Temporal Logic and Model Checking
The books and papers listed here provide
background reading that is often more advanced than the material in
Logic in Computer Science: Modelling and Reasoning about Systems
- Michael Huth, Mark Ryan
- Cambridge University Press, Second Edition 2004. ISBN: 0 521 54310.
- Web page:
- [Buy this if you buy anything -- also good for the course Hoare Logic]
- Model Checking
- Edmund M Clarke, jr., Orna Grumberg, and Doron Peled,
MIT Press, 1999.
Symbolic Model Checking,
- Kenneth L McMillan,
Kluwer Academic Publishers, 1993.
- Software model checking
- Ranjit Jhala and Rupak Majumdar, ACM Computing Surveys, Vol. 41, No. 4, October 2009
Branching vs. Linear Time: Final Showdown
- Moshe Vardi, Rice
Formal Hardware Verification with BDDs: An Introduction,
- Alan J. Hu,
Department of Computer Science, University of British Columbia.
An Introduction to Binary Decision Diagrams,
- Henrik Reif Andersen,
Professor at the IT University of Copenhagen.
introduction to model Checking
- (Invited tutorial given
at the Summer School on Formal Methods in Performance Analysis - Nijmegen,
- Piere Wolper
Four Lectures on Model Checking
- Thomas Henzinger, UCB
Logic and Verification
- (slides for a Spring 2003 course at NYU, especially Lecture 5)
- Clark Barrett
Property Specification Language Reference Manual
- (Version PSL 1.1 of the language selected by the
Accellera Formal Verification Technical Committee as the future standard).
The Designer's Guide To PSL
- (short PSL introduction from Doulos).
Property Specification: The key to an Assertion-Based Verification Platform
- C. Michael Chang and Harry D. Foster,