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 documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
