Towards SMT Model Checking of Array-Based Systems

Silvio Ghilardi; Enrica Nicolini; Silvio Ranise; Daniele Zucchelli

doi:10.1007/978-3-540-71070-7_6

Towards SMT Model Checking of Array-Based Systems

Silvio Ghilardi ¹ Enrica Nicolini ² Silvio Ranise ^{1, 2} Daniele Zucchelli ¹

1 Dipartimento di Scienze dell'Informazione [Milano]

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 Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications

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.

Type de document :

Communication dans un congrès

Alessandro Armando and Peter Baumgartner and Gilles Dowek. Automated Reasoning, 4th International Joint Conference, IJCAR 2008, Aug 2008, Sydney, Australia. Springer, 5195, pp.67-82, 2008, Lecture Notes in Computer Science. 〈10.1007/978-3-540-71070-7_6〉

Domaine :

Informatique [cs] / Logique en informatique [cs.LO]

Liste complète des métadonnées

https://hal.inria.fr/inria-00576600
Contributeur : Christophe Ringeissen <>
Soumis le : lundi 14 mars 2011 - 17:37:25
Dernière modification le : vendredi 6 juillet 2018 - 15:06:10

Towards SMT Model Checking of Array-Based Systems

Lien texte intégral

Identifiants

Collections

Citation

Exporter

Métriques

92

Contact

Towards SMT Model Checking of Array-Based Systems

Lien texte intégral

Identifiants

Collections

Citation

Exporter

Partager

Métriques

92

Contact