Handouts
Date Day Title
08/29/06  Tuesday Model checking overview (pdf)
08/31/06  Thursday Propositional logic (ps) (pdf)
09/05/06  Tuesday Conversion of propositional formulas to CNF and DNF. Introduction of new variables for converting a formula to CNF. A handout was given. Section 1.5 of Huth and Ryan gives a program for converting formulas to Normal forms.
09/07/06  Thursday We reviewed how to convert a given formula to CNF by adding new variables. Then we discussed the Davis-Putnam rules. A handout describing these rules was given.
09/12/06  Tuesday Reviewed Davis Putnam rules. A handout illustrating these rules was given. We discussed HW1 related doubts and solved some related problems. A handout describing the principle of structural induction was given.(pdf)
We assigned the following paper for reading. GRASP technical report (ps) (pdf)
09/14/06  Thursday Covered resolution. Started discussion on GRASP SAT solver. Here are the slides. (ps) (pdf) (ppt)
09/19/06  Tuesday Explained implication graphs and conflict induced clauses in GRASP.
09/21/06  Thursday GRASP discussion continued, non-chronological backtracking in GRASP. Chaff paper assigned for reading (pdf). A more verbose account of Chaff can be found in Lintao Zhang's Ph.D. thesis (chapters 2,3).
09/26/06  Tuesday CNF encodings for Sudoku puzzle. (ppt)
09/28/06  Thursday Described the features of ZChaff SAT solver (ppt).
10/03/06 Tuesday Spent about 15 minutes on new ideas in Minisat such as compression of clauses. (ppt).
Started Binary Decision Diagrams (ps) (pdf).
Here is a link to the original BDD paper by Randy Bryant (pdf).
10/05/06 Thursday Finished the set of slides on BDDs from previous class.
10/10/06 Tuesday Representing sets and relations as BDDs, Quantified boolean formulas, computing the relational product efficiently. (ps) (pdf) Material covered in the last three lectures can be found in Model checking book Chapter 5, Huth and Ryan Sections 6.1-6.2.2 and 6.3.1-6.3.2.
10/12/06 Thursday Reviwed the algorithm for computing relational product. Described a non-clausal SAT solver based on General Matings. Slides and a related paper are: slides, paper (pdf)
10/17/06 Tuesday Midterm
10/19/06 Thursday Completed the General Matings based SAT solver started in previous class. Started CTL model checking (ps),(pdf).
10/24/06 Tuesday Continued CTL model checking. We ran Cadence SMV on small examples.
10/26/06 Thursday More SMV examples (slides(ppt)).
10/31/06 Tuesday Discussed a mutual exlusion protocol and specifications in SMV.
(Using TRANS statement and CTL specification)
(Using processes and CTL specification)
(Using processes and LTL specification). Provided by Ken McMillan. This version uses Cadence SMV syntax.
11/2/06 Thursday Finished the mutual exlusion example from previous class.
11/7/06 Tuesday Traffic light controller example in SMV. We want a solution that satisfies mutual exlusion, guarantees liveness for each light, is non-blocking, and there should not be strict sequencing of lights. (Buggy version 1), (Buggy version 2).
11/9/06 Thursday Discussed one posssible solution to the traffic light example (Buggy version 3), (A solution). Please report alternative solutions or bugs in our solution. We will make them available to the class.
Kwon described how to solve various games using Model Checking.
11/14/06 Tuesday Semantics of CTL (ps),(pdf).
11/14/06 Tuesday Explicit state model checking (ps),(pdf).
Symbolic model checking (ps),(pdf).
11/16/06 Tuesday Kwon's lecture on how to solve various puzzles using model checking. (pdf)
12/05/06, 12/07/06 Tuesday, Thursday Fixpoint characterization of CTL(ps),(pdf). Bounded Model Checking.
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, Doron Peled
            MIT Press