Model-Checking Modulo Theories: Declarative Framework and Pragmatic Issues

  • Silvio Ranise | INRIA

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.

Speaker Details

Silvio Ranise has a permanent research position at INRIA from September 2002, in the LORIA laboratory common to CNRS, INRIA and the Universities of Nancy. He is now on-leave to work in the European project AVANTSSAR (at the University of Verona) aimed at the verification of Software Oriented Architectures. He got his PhD in January 2002 from the University of Genova (Italy) and the University of Nancy 1 (France) under a joint PhD program. His research interests are model checking, web service and program verification, automated deduction, decision procedures. He has initiated the workshop series “Pragmatics of Decision Procedures in Automated Deduction (PDPAR)” (now called SMT workshop) and the “Satisfiability Modulo Theory Library (SMT-LIB).”

Watch Next