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.
Cite
CITATION STYLE
Ghilardi, S., Nicolini, E., Ranise, S., & Zucchelli, D. (2008). Towards SMT model checking of array-based systems. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5195 LNAI, pp. 67–82). https://doi.org/10.1007/978-3-540-71070-7_6
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
