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

  • Download the DMC user guide.
  • Download the DMC SICStus Prolog source code.
  • You need SICStus Prolog to run DMC.
  • SICStus Prolog user guide.

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