 |
 |
||
|
|
|
|
 |
 |
|
|
|
|
|
 |
 |
|
|
|
|
|
 |
||
|
|
||
15-414 Handouts
| Date | Day | Lecture Slides | Additional Readings and Notes |
| 8/28 | Tues | Model checking overview (pdf) | |
| 8/30 | Thurs | Propositional Logic (pdf) (ps) | |
| 9/04 | Tues | Propositional Logic (pdf) (ps) | |
| 9/06 | Thurs | Propositional Logic (pdf) (ps) | |
| 9/11 | Tues | GRASP (pdf) (ps) (ppt) | GRASP technical report (pdf) (ps) |
| 9/13 | Thurs | GRASP (pdf) (ps) (ppt) | |
| 9/18 | Tues | Example of GRASP (pdf) (compacted ps) | An Overview of Backtrack Search Satisfiability Algorithms (pdf) |
| 9/20 | Thurs | 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/25 | Tues | Encoding Sudoku (pdf) (ppt) | |
| 9/27 | Thurs | Optimized Sudoku Encoding (pdf) (ppt) MiniSat (pdf) (ppt) |
|
| 10/02 | Tues | CBMC (pdf) (ppt) solution to lecture problem | by Arie Gurfinkel |
| 10/04 | Thurs | CBMC (pdf) (ppt) solution to lecture problem | by Arie Gurfinkel |
| 10/09 | Tues | BDDs (pdf) (ps) | Graph-Based Algorithms for Boolean Function Manipulation (pdf) |
| 10/11 | Thurs | BDDs (pdf) (ps) | |
| 10/16 | Tues | CTL (pdf) | |
| 10/18 | Thurs | CTL (pdf) and midterm review | NuSMV information |
| 10/22 | Tues | Midterm (in class) | Last year's midterm (pdf) |
| 10/25 | Thurs | CTL and midterm results | More examples of CTL (pdf) (ppt) | 10/30 | Tues | CTL Examples | Additional examples of CTL (zip) (tar.gz) |
| 11/01 | Thurs | Computation Tree Logics (pdf) | Covered LTL |
| 11/06 | Tues | Model Checking (pdf); BDDs in Detail (pdf) | Covered the design of model checkers |
| 11/08 | Thurs | Traffic (pdf) (ppt) | Himanshu Jain covered a SVM model of a traffic light controller. See the SVM files. |
| 11/13 | Tues | Symbolic Model Checking (pdf) (ps) | Introduced symbolic model checking using BDDs |
| 11/15 | Thurs | Fixed-Points for Symbolic Model Checking (pdf) (ps) | Covered the fixed-point representation of properties needed to perform symbolic model checking |
| 11/20 | Tues | Java Pathfinder, Part 1 (pdf) | by Sagar Chaki |
| 11/22 | Thurs | No Class | Thanksgiving Holiday |
| 11/27 | Tues | Java Pathfinder, Part 2 (pdf) | by Sagar Chaki. Covered choice points, partial order reduction, and the exercises.
JPF examples (tar.gz) from class. |
| 11/29 | Thurs | ||
| 12/04 | Tues | ||
| 12/06 | Thurs |
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 systemsThe following book is more technical in nature and provides a thorough treatment of model checking:
Michael R A Huth and Mark D Ryan
Cambridge University Press
Model Checking
Edmund M. Clarke, Orna Grumberg, and Doron Peled
MIT Press