Looking for a book that derives and constructs a model checking application

Question

I am teaching myself program verification and am currently learning proof assistants. I have the book Handbook of Practical Logic and Automated Reasoning which gives the proofs necessary for the understanding of such a system, but more importantly for me it also gives an implementation of the necessary algorithms as OCAML source.

I know that some of the tools listed in Wikipedia: Model Checking tools and YAHODA: Verifications Tools Database are open source, but I also prefer it when the theory, proofs, algorithms and source code are presented at the same time reinforcing each other, and in a progression building up to a final application.

Is there such a book for model checking?

EDIT

I may have found what I am looking for in Mathematical Logic for Computer Science with Prolog source. As I don't have the book, does anyone know if this book fits the requirement?

Answer 1

John Harrison's book is an exception in going all the way from theory to practice and making all the source code available. I think you will find it difficult to find an equivalent book for model checking, but there are a few that achieve a close approximation.

• Principles of Model Checking by Baier and Katoen contains a lot of examples and pretty detailed algorithmic description.
• The SPIN Model Checker by Gerard Holzmann is a very different treatment from the author of one of the earliest model checkers. He has maintained the tool for about thirty years and has a "programmatic" approach.

A better bet may be to follow the course notes and lab assignments of some courses available online. At least you will find the theory, practice and examples, even though they are not organised in a book.

• Edmund Clarke's course in CMU has a reading list which includes tutorials for a few different model checkers.
• Joost-Pieter Katoen's software verification course and the followup on Practical Model Checking and Advanced Model Checking cover a lot of ground.

Finally, this is not entirely what you asked for, but since you have been studying logic and now model checking, you will invariably run into references to abstract interpretation, which is the basis of static program analysis and is intimately connected to model checking (though this connection is not always explicit in the model checking literature).

• Patrick Cousot's MIT Course is a tour de force covering everything from lattice theoretic foundations to the complete implementation of a static analyzer for a simple language. His course material includes all the code and exercises.