| 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. |
