|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)
Covered resolution. Started discussion on GRASP SAT solver.
Here are the slides.
|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).|
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/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)).|
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).|
Discussed one posssible solution to the traffic light example
version 3), (A
solution). Please report alternative solutions or bugs in our
solution. We will make them available to the
Kwon described how to solve various games using Model Checking.
|11/14/06||Tuesday||Semantics of CTL (ps),(pdf).|
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.|
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
Edmund M. Clarke, Orna Grumberg, Doron Peled