Tags:artifact system, covers, model completeness, quantifier elimination, superposition calculus and verification of data-aware processes
Abstract:
In ESOP 2008, Gulwani and Musuvathi introduced a notion of cover and exploited it to attack infinite-state model checking problems. Motivated by applications to the verification of data-aware processes, we show how covers are strictly related to model completions, a well-known topic in classical model theory. We also investigate the computation of covers within the Superposition Calculus, by adopting a constrained version of the calculus, equipped with appropriate settings and reduction strategies.