Home | Search | Help  
Home Page Università di Genova

Seminar Details


Date 3-6-2009
Time 14:30
Room/Location Sala Conferenze
Title Model-Checking Modulo Theories: Declarative Framework and Pragmatic Issues
Speaker Prof. Silvio Ghilardi e Dott. Silvio Ranise
Affiliation Universita' degli studi di Milano
Link https://www.disi.unige.it/index.php?eventsandseminars/seminars
Abstract 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.
Back to Seminars