6
$\begingroup$

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?

$\endgroup$
8
$\begingroup$

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.

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.
$\endgroup$
  • 2
    $\begingroup$ I ordered Principles of Model Checking yesterday. Can you give some links to the online courses you mention? $\endgroup$ – Guy Coder Jul 28 '12 at 0:38
  • $\begingroup$ Done. I wish I had remembered the Spin book earlier. Hope the courses are useful. $\endgroup$ – Vijay D Jul 29 '12 at 2:08
  • $\begingroup$ I mark this as the accepted answer to award the points; please don't take this to mean that there is a book meeting the requirements. The information here is still very valuable for someone just starting out with model checking. $\endgroup$ – Guy Coder Jul 29 '12 at 21:54
  • $\begingroup$ Thanks for accepting. I assume the comment below is not addressed to me. I agree (and said in my reply) that there probably isn't a book meeting your requirements. $\endgroup$ – Vijay D Aug 3 '12 at 21:56
  • $\begingroup$ No the comment is not addressed at you. It is for others who are seeking the same type of info as myself and may read this in the future. $\endgroup$ – Guy Coder Aug 4 '12 at 14:33

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.