Some Fomal Verification Related Books

(that I read recently.)


  • Logic in computer science: modeling and reasoning about systems / Michael Huth and Mark Ryan. Cambridge University Press, 2000.
    • The logic part includes propositional logic, predicate logic and modal logic, and is relatively easy to read. The verification part includes program verification (theorem proving) and symbolic model checking.
  • Model checking / E. Clarke, O. Grumberg and D. Peled. MIT Press, 1999. 
    • This book covers most (if not all) of the research topics in model checking. 
  • Introduction to formal hardware verification / Thomas Kropf.  Springer-Verlag, 1999.
    • It is mainly on symbolic model checking, and also includes an introduction on higher-order logic.
  • Algorithms and data structures in VLSI Design. C. Meinel and T. Theobald. Springer-Verlag, 1998.
    • This book covers BDDs and many variants and extensions of BDDs. It also has BDD-based symbolic image computation and a brief introduction to CTL model checking.
  • Binary Decision Diagrams: theory and implication. R. Drechsler and B. Becker. Kluwer Academic Publishers, 1998.
    • It is mainly on the various minimization methods for BDDs, and also includes a case study on using BDDs in two-level logic minimization.
  • "Bounded Model Checking," A. Biere, A. Cimatti, E. M. Clarke, O. Strichman and Y. Zhu. Vol. 58 of Advances in Computers, 2003. Academic Press (pre-print)
    • As a relatively new technique (since 1999), bounded model checking has sparked a lot of research. Check Biere's website for this pre-print.