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.