In ESOP 2008, Gulwani and Musuvathi introduced a notion of cover and exploited it to handle 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 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.
Model Completeness, Covers and Superposition / D. Calvanese, S. Ghilardi, A. Gianola, M. Montali, A. Rivkin (LECTURE NOTES IN ARTIFICIAL INTELLIGENCE). - In: Automated Deduction – CADE 27 / [a cura di] P. Fontaine. - [s.l] : Springer, 2019 Aug. - ISBN 9783030294359. - pp. 142-160 (( Intervento presentato al 27. convegno International Conference on Automated Deduction tenutosi a Natal nel 2019.
Model Completeness, Covers and Superposition
S. Ghilardi;
2019
Abstract
In ESOP 2008, Gulwani and Musuvathi introduced a notion of cover and exploited it to handle 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 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.
| File | Dimensione | Formato | |
|---|---|---|---|
|
CADE-19.pdf
accesso riservato
Tipologia:
Pre-print (manoscritto inviato all'editore)
Dimensione
218.19 kB
Formato
Adobe PDF
|
218.19 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
|
Calvanese2019_Chapter_ModelCompletenessCoversAndSupe.pdf
accesso riservato
Tipologia:
Publisher's version/PDF
Dimensione
448.15 kB
Formato
Adobe PDF
|
448.15 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
