We consider the problem of invariant checking for transition systems using SMT and quantified variables ranging over finite but unbounded domains. We propose a general approach, obtained by combining two ingredients: exploration of a finite instance, to obtain candidate inductive invariants, and instantiation-based techniques to discharge quantified queries. A thorough experimental evaluation on a wide range of benchmarks demonstrates the generality and effectiveness of our approach. Our algorithm is the first capable of approaching in a uniform way such a large variety of models.
Verification of SMT Systems with Quantifiers / Cimatti, A.; Griggio, A.; Redondi, G.. - ELETTRONICO. - 13505:(2022), pp. 154-170. (Intervento presentato al convegno ATVA tenutosi a Virtual nel 25-28 october, 2022) [10.1007/978-3-031-19992-9_10].
Verification of SMT Systems with Quantifiers
Cimatti A.;Griggio A.;Redondi G.
2022-01-01
Abstract
We consider the problem of invariant checking for transition systems using SMT and quantified variables ranging over finite but unbounded domains. We propose a general approach, obtained by combining two ingredients: exploration of a finite instance, to obtain candidate inductive invariants, and instantiation-based techniques to discharge quantified queries. A thorough experimental evaluation on a wide range of benchmarks demonstrates the generality and effectiveness of our approach. Our algorithm is the first capable of approaching in a uniform way such a large variety of models.File | Dimensione | Formato | |
---|---|---|---|
main.pdf
Open Access dal 22/10/2023
Tipologia:
Post-print referato (Refereed author’s manuscript)
Licenza:
Tutti i diritti riservati (All rights reserved)
Dimensione
569.39 kB
Formato
Adobe PDF
|
569.39 kB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione