15-414 Handouts
Date Day Lecture Slides Additional Readings and Notes
8/28Tues Model checking overview (pdf)  
8/30Thurs Propositional Logic (pdf) (ps)  
9/04Tues Propositional Logic (pdf) (ps)  
9/06Thurs Propositional Logic (pdf) (ps)  
9/11Tues GRASP (pdf) (ps) (ppt) GRASP technical report (pdf) (ps)
9/13Thurs GRASP (pdf) (ps) (ppt)  
9/18Tues Example of GRASP (pdf) (compacted ps) An Overview of Backtrack Search Satisfiability Algorithms (pdf)
9/20Thurs Chaff (pdf) (ppt) Chaff: Engineering an Efficient SAT Solver (pdf)
The Quest for Efficient Boolean Satisfiability Solvers (pdf)
Efficient Conflict Driven Learning in a Boolean Satisfiability Solver (pdf)
9/25Tues Encoding Sudoku (pdf) (ppt)  
9/27Thurs Optimized Sudoku Encoding (pdf) (ppt)
MiniSat (pdf) (ppt)
10/02Tues CBMC (pdf) (ppt) solution to lecture problem by Arie Gurfinkel
10/04Thurs CBMC (pdf) (ppt) solution to lecture problem by Arie Gurfinkel
10/09Tues BDDs (pdf) (ps) Graph-Based Algorithms for Boolean Function Manipulation (pdf)
10/11Thurs BDDs (pdf) (ps)  
10/16Tues CTL (pdf)  
10/18Thurs CTL (pdf) and midterm review NuSMV information
10/22Tues Midterm (in class) Last year's midterm (pdf)
10/25Thurs CTL and midterm results More examples of CTL (pdf) (ppt)
10/30Tues CTL Examples Additional examples of CTL (zip) (tar.gz)
11/01Thurs Computation Tree Logics (pdf) Covered LTL
11/06Tues Model Checking (pdf); BDDs in Detail (pdf) Covered the design of model checkers
11/08Thurs Traffic (pdf) (ppt) Himanshu Jain covered a SVM model of a traffic light controller. See the SVM files.
11/13Tues Symbolic Model Checking (pdf) (ps) Introduced symbolic model checking using BDDs
11/15Thurs Fixed-Points for Symbolic Model Checking (pdf) (ps) Covered the fixed-point representation of properties needed to perform symbolic model checking
11/20Tues Java Pathfinder, Part 1 (pdf) by Sagar Chaki
11/22Thurs No Class Thanksgiving Holiday
11/27Tues Java Pathfinder, Part 2 (pdf) by Sagar Chaki. Covered choice points, partial order reduction, and the exercises.
JPF examples (tar.gz) from class.

You might need to VPN to access some papers. Some lecture slides do not work with gv. acroread should be used instead.

15-414 Textbooks

We will be following this textbook for most of the course:

Logic in Computer Science: Modeling and reasoning about systems
Michael R A Huth and Mark D Ryan
Cambridge University Press
The following book is more technical in nature and provides a thorough treatment of model checking:
Model Checking
Edmund M. Clarke, Orna Grumberg, and Doron Peled
MIT Press