Skip to Main content Skip to Navigation
Conference papers

Towards SMT Model Checking of Array-Based Systems

Silvio Ghilardi 1 Enrica Nicolini 2 Silvio Ranise 1, 2 Daniele Zucchelli 1 
2 CASSIS - Combination of approaches to the security of infinite states systems
FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174), Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : We introduce the notion of array-based system as a suitable abstraction of infinite state systems such as broadcast protocols or sorting programs. By using a class of quantified-first order formulae to symbolically represent array-based systems, we propose methods to check safety (invariance) and liveness (recurrence) properties on top of Satisfiability Modulo Theories solvers. We find hypotheses under which the verification procedures for such properties can be fully mechanized.
Document type :
Conference papers
Complete list of metadata

https://hal.inria.fr/inria-00576600
Contributor : Christophe Ringeissen Connect in order to contact the contributor
Submitted on : Monday, March 14, 2011 - 5:37:25 PM
Last modification on : Friday, January 21, 2022 - 3:09:03 AM

Links full text

Identifiers

Citation

Silvio Ghilardi, Enrica Nicolini, Silvio Ranise, Daniele Zucchelli. Towards SMT Model Checking of Array-Based Systems. Automated Reasoning, 4th International Joint Conference, IJCAR 2008, Aug 2008, Sydney, Australia. pp.67-82, ⟨10.1007/978-3-540-71070-7_6⟩. ⟨inria-00576600⟩

Share

Metrics

Record views

63