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. © 2008 Springer-Verlag Berlin Heidelberg.
Towards SMT model checking of array-based systems / Ghilardi, S.; Nicolini, E.; Ranise, S.; Zucchelli, D.. - 5195:(2008), pp. 67-82. (Intervento presentato al convegno 4th International Joint Conference on Automated Reasoning, IJCAR 2008 tenutosi a Sydney, NSW, aus nel 2008) [10.1007/978-3-540-71070-7_6].
Towards SMT model checking of array-based systems
Ranise S.;
2008-01-01
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. © 2008 Springer-Verlag Berlin Heidelberg.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione
