Deductive Model Checking (DMC)
Constraint-based Verification
Giorgio Delzanno, and
Andreas
Podelski
DMC (Deductive Model Checking) is a prototype symbolic model checker
implemented in SICStsus Prolog
for infinite-state systems with integer and real data variables. The symbolic
representation of the state-space is given through a collection (disjunction)
of linear arithmetic constraints. Constraints are stored in the
internal database of SICStus Prolog as constrained facts (i.e. unit facts
with constraints in the body). Constraints are manipulated using the internal
real-solver of SICStus (Holzbaur's clp(Q,R) library). Safety and liveness
properties are verified using a possibly non terminating fixpoint computation.
A set of acceleration rules (defined in the rule-based style typical of
Prolog) are used to speed-up (and sometimes enforce termination of) the
computation. With DMC, we managed to prove properties of concurrent systems
like mutual exclusion algorithms (Bakery, Ticket, Producer-Consumers),
parameterized cache coherence protocols (Illinois, Berkeley, Dragon, Firefly)
and abstractions of C-programs for array bounds checking. We describe next
how to load and experiment using the current prototype version and the
cache coherence protocols in the directory `examples'.
Note: since Sept, 2000 I am not maintaining the code anymore
Links
Download
the DMC user guide.
Download
the DMC SICStus Prolog source code.
You need SICStus Prolog to run
DMC.
SICStus
Prolog user guide.
References
[DP99] G. Delzanno and A. Podelski
Model
Checking in CLP.
In Proc. of 6th Int'l Conf. on
Tools and Algorithms for the Construction and Analysis of Systems,
TACAS 99, LNCS 1579, pages 223--239. Springer, 1999.
[DP99] G. Delzanno and A. Podelski
Constraint-based
Deductive Model Checking (Draft)
Accepted for publication in the journal
Software Tools for Technology Transfer,
February 2000.
[Del00] G. Delzanno
Automatic
Verification of Parameterized Cache Coherence Protocols
Technical Report DISI-1-00,
University of Genova, January 2000.