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〉
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
