Computer Laboratory

Technical reports

Combining model checking and theorem proving

Hasan Amjad

September 2004, 131 pages

This technical report is based on a dissertation submitted March 2004 by the author for the degree of Doctor of Philosophy to the University of Cambridge, Trinity College.


We implement a model checker for the modal mu-calculus as a derived rule in a fully expansive mechanical theorem prover, without causing an unacceptable performance penalty.

We use a restricted form of a higher order logic representation calculus for binary decision diagrams (BDDs) to interface the model checker to a high-performance BDD engine. This is used with a formalised theory of the modal mu-calculus (which we also develop) for model checking in which all steps of the algorithm are justified by fully expansive proof. This provides a fine-grained integration of model checking and theorem proving using a mathematically rigourous interface. The generality of our theories allows us to perform much of the proof offline, in contrast with earlier work. This substantially reduces the inevitable performance penalty of doing model checking by proof.

To demonstrate the feasibility of our approach, optimisations to the model checking algorithm are added. We add naive caching and also perform advanced caching for nested non-alternating fixed-point computations.

Finally, the usefulness of the work is demonstrated. We leverage our theory by proving translations to simpler logics that are in more widespread use. We then implement an executable theory for counterexample-guided abstraction refinement that also uses a SAT solver. We verify properties of a bus architecture in use in industry as well as a pedagogical arithmetic and logic unit. The benchmarks show an acceptable performance penalty, and the results are correct by construction.

Full text

PDF (0.9 MB)

BibTeX record

  author =	 {Amjad, Hasan},
  title = 	 {{Combining model checking and theorem proving}},
  year = 	 2004,
  month = 	 sep,
  url = 	 {},
  institution =  {University of Cambridge, Computer Laboratory},
  number = 	 {UCAM-CL-TR-601}