Reading List

Reading List
Temporal Logic and Model Checking

The books and papers listed here provide background reading that is often more advanced than the material in the course.

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.
 Sometimes can be found online using Google.]
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, Sometime Professor at the IT University of Copenhagen.
An introduction to model Checking 
(Invited tutorial given at the Summer School on Formal Methods in Performance Analysis - Nijmegen, July 2000)
Piere Wolper
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).
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, Verplex systems