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.
Towards SMT Model-Checking of Array-based Systems / S. Ghilardi, E. Nicolini, S. Ranise, D. Zucchelli - In: Automated Reasoning : 4th International Joint Conference, IJCAR 2008, Sydney, Australia, August 12-15, 2008 : Proceedings / [a cura di] A. Armando, P. Baumgartner, G. Dowek. - Berlin : Springer, 2008. - ISBN 9783540710691. - pp. 67-82 (( Intervento presentato al 4. convegno International Joint Conference on Automated Reasoning (IJCAR 08) tenutosi a Sydney nel 2008 [10.1007/978-3-540-71070-7_6].
Towards SMT Model-Checking of Array-based Systems
S. GhilardiPrimo
;E. NicoliniSecondo
;D. ZucchelliUltimo
2008
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.
Pubblicazioni consigliate
I metadati presenti in AIR sono rilasciati con licenza CCO mentre i file delle pubblicazioni sono rilasciati con licenza CC BY-SA, salvo diversa indicazione. In caso di violazione di copyright, contattare l'assistenza di AIR
