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.
2022
International Symposium on Automated Technology for Verification and Analysis
Cham, Svizzera
Springer
978-3-031-19991-2
978-3-031-19992-9
Cimatti, A.; Griggio, A.; Redondi, G.
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].
File in questo prodotto:
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

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11572/362302
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 2
  • ???jsp.display-item.citation.isi??? ND
social impact