Model-Checking Modulo Theories: Declarative Framework and Pragmatic Issues

Опубликовано 7 сентября 2016, 17:29

We discuss the notion of array-based system as a suitable abstraction of infinite state systems such as parametrised systems 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) properties on top of Satisfiability Modulo Theories (SMT) solvers. We identify hypotheses under which such verification technique becomes a decision procedure for invariance properties of array-based systems and discuss the difficulties to make the approach viable in practice. In this respect, the use of quantified first-order formulae to describe sets of states makes checking for fix-point and unsafety extremely expensive. Thus, we focus on (static and dynamic) techniques for instance reduction and illustrate some experimental results of our implementation of the framework in the MCMT model-checker.