zbMATH — the first resource for mathematics

Towards SMT model checking of array-based systems. (English) Zbl 1165.68406
Armando, Alessandro (ed.) et al., Automated reasoning. 4th international joint conference, IJCAR 2008, Sydney, Australia, August 12–15, 2008 Proceedings. Berlin: Springer (ISBN 978-3-540-71069-1/pbk). Lecture Notes in Computer Science 5195. Lecture Notes in Artificial Intelligence, 67-82 (2008).
Summary: 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.
For the entire collection see [Zbl 1149.68003].

68Q60 Specification and verification (program logics, model checking, etc.)
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
PDF BibTeX Cite
Full Text: DOI