**Speaker:**
Giorgio Delzanno
**Title:**
Deductive Model Checking

**Abstract.**
Automated verification methods can today be applied to practical
systems. One reason for this success is that implicit
representations of *finite* sets of states through Boolean
formulas can be handled efficiently via BDD's.
The finiteness is an inherent restriction here.
Many systems, however, operate on data values from an infinite
domain and are intrinsically *infinite-state*; i.e., one cannot
produce a finite-state model without abstracting away crucial
properties.
One important research goal is to find appropriate data
structures for implicit representations of infinite sets of states, and
design model checking algorithms that perform well on practical
examples.
The metaphor of *constraints* seems useful (unavoidable?) for the
implicit representation of sets of states.
The question is whether and how the systems for programming over constraints
as first-class data structures can be used for the verification of
infinite-state systems.
In our work we propose *Constraint Logic Programming (CLP)*
as a conceptual basis and as a practical implementation platform for
model checking.
Specifically, we exhibit a connection bewteen temporal properties (CTL)
and CLP program semantics.
This connection allows us to integrate algorithmic techniques developed
in Computer Aided Verification with deductive methods developed, e.g.,
in Constraint Databases.

Joint work with Andreas Podelski, *Max-Planck-Institut für
Informatik, Saarbrücken.*