Model-Checking Modulo Theories: Declarative Framework and Pragmatic Issues
Staff - Faculty of Informatics
Start date: 22 February 2010
End date: 23 February 2010
The Faculty of Informatics is pleased to announce a seminar given by Silvio Ghilardi and Silvio Ranise
DATE: Monday, February 22nd, 2010
PLACE: USI Università della Svizzera italiana, room SI-15, Informatics building (Via G. Buffi 13)
TIME: 11.00
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.
BIO:
Silvio Ghilardi graduated in Philosophy and then got a PhD in Mathematics at the Università degli Studi di Milano. He was research assistant in Algebra and Geometry, then Associate Professor and currently Full Professor in Logic at the Computer Science Department of the Università degli Studi di Milano. His research interests range from modal logic, to algebraic and categorical logic, to automated reasoning and formal methods. Recently, he was involved in the development of the SMT based model checker MCMT.
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)."
HOST: Prof. Natasha Sharygina
