Towards SMT Model Checking of Array-Based Systems

Abstract. We introduce the notion of array-based system as a suittraction 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. c SpringerVerlag 2008

• Type: Conference
• Year: 2008
• Where: CADE
• Authors: Silvio Ghilardi, Enrica Nicolini, Silvio Ranise, Daniele Zucchelli
• Keywords: Automated Reasoning, CADE 2008, Infinite State Systems, Quantified-first Order Formulae, Satisfiability Modulo Theories