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:
http://www.cs.bham.ac.uk/research/lics/
- [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