Sciweavers

Share
CADE
2008
Springer

Towards SMT Model Checking of Array-Based Systems

9 years 2 months ago
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
Silvio Ghilardi, Enrica Nicolini, Silvio Ranise, D
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2008
Where CADE
Authors Silvio Ghilardi, Enrica Nicolini, Silvio Ranise, Daniele Zucchelli
Comments (0)
books