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. Ghilardi
Primo
;
E. Nicolini
Secondo
;
D. Zucchelli
Ultimo
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.
model checking ; satisfiability modulo theory
Settore M-FIL/02 - Logica e Filosofia della Scienza
2008
Book Part (author)
File in questo prodotto:
Non ci sono file associati a questo prodotto.
Pubblicazioni consigliate

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/2434/53456
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 45
  • ???jsp.display-item.citation.isi??? 30
social impact