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, 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〉
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 : jeudi 15 février 2018 - 08:48:09

Lien texte intégral

Identifiants

Citation

Silvio Ghilardi, Enrica Nicolini, Silvio Ranise, Daniele Zucchelli. Towards SMT Model Checking of Array-Based Systems. 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〉. 〈inria-00576600〉

Partager

Métriques

Consultations de la notice

74