Lecture 1 -- Tue, Jan 18 -- Introduction, motivation, review of research
Lecture 2 -- Thu, Jan 20 -- Modeling using FSMs, EFSMs, communicating FSMs (contains Homework 1)
Lectures 3 and 4 -- Tue, Jan 25 and Thu, Jan 27:
Solving two-player games on finite graphs;
solving emptiness of pushdown automata using games;
regularity of reachable configurations of a PDA.
Lecture 3
Lecture 4
Lectures 5 and 6-- Tue, Feb 1 and Thu, Feb 3 --- Binary decision diagrams
Hint for Problem 1.
Hint for Problem 2.
Lecture 7 -- Tue, Feb 8--- CTL and bisimulations
Lecture 8 -- Tue, Feb 10--- Model checking CTL using BDDs; fixpoints; mu-calculus
Lecture 9 and Lecture 10--- Tue, Feb 15 and Thu, Feb 17--- Predicate abstraction
See Construction of abstract state graphs with PVS, Graf and Saidi, CAV'97
Lecture 11--- Tue, Feb 22 -- Predicate abstraction in SLAM
See Automatic Predicate Abstraction of C Programs by Ball, Majumdar, Millstein, Rajamani and
Boolean and Cartesian Abstraction for Model Checking C Programs by Ball Podelski, Rajamani.
See SLAM talk by Ball and Rajamani, POPL'02.
Thu, Feb 24 -- Discussion
Tue, Mar 1 -- Linear-time temporal logic (LTL) -- Syntax/semantics; Buchi automata
Thu, Mar 3 -- LTL -> Buchi automata -- Vardi-Wolper construction.
Here are some lecture notes that give the construction and proof of
correctness in detail; relevant section is Sec 3.1 (earlier sections are
good to read as well for basic definitions of LTL and omega-automata:
Linear-time
temporal logic and Buchi automata -- Madhavan Mukund.
Tue, Mar 8 -- Emptiness of Buchi automata, on-the-fly model checking,
nested DFS, expressive power of LTL and FOL, MSO.
Homework! - Due on 17/18 March
Thu, Mar 10 -- No lecture -- Larry Wos lecture instead.
See list of seminar papers
Tue, Mar 15 -- Bounded model checking using SAT.
See Bounded Model Checking Using Satisfiability Solving
by Clarke, Biere, Raimi and Zhu, FMSD 2001.
Thu, Mar 17 -- Solving SAT -- the high level algorithm in a modern
SAT solver
See talk:
A Quest for Efficient SAT Solvers
See the papers:
The Quest for Efficient Boolean Satisfiability Solvers
and see Section 2 in Applying SAT Methods in Unbounded Symbolic Model Checking
by McMillan.
Tue, Mar 22; Thu Mar 24: Spring break
Tue, Mar 29; Thu Mar 31:
Shape Analysis -- analyzing dynamic data with pointers -- Reps, Sagiv, Wilhelm
See the papers:
Static Program Analysis via 3-valued logic CAV'04 invited talk
Parametric
Shape Analysis via a 3-valued logic,
TOPLAS'02 (has all details)
See talk:
Static Program Analysis via 3-valued logic, CAV'04 invited talk.
Tue, Apr 05: Speaker: Ayesha Yasmeen
Interpolation and SAT-based Model Checking, by K. McMillan.
Thu, Apr 07: Speaker: Mike Rosulek
A BDD-based Model Checker for Recursive Programs, by J. Esparza, S. Schwoon, by Esparza and Schwoon.
Tue, Apr 12: Speaker: Jared Mowery
Discovering Affine Equalities Using Random Interpretation, by Gulwani and Necula, Proc. of Principles of Programming Languages (POPL), 2003.
Thu, Apr 14: Speaker: Shan Lu
Scalable Error Detection using Boolean Satisfiability, by Y. Xie, A. Aiken, Proc. of Principles of Programming Languages (POPL), 2005.
Tue, Apr 19: Speaker: Dinakar Dhurjati
Analyzing Memory Accesses in x86 Executables, by G. Balakrishnan and T. Reps,
13th Int'l Conf on Compiler Construction (CC), ETAPS'04.
Thu, Apr 21: Speaker: Joseph Tucek
Summarizing Procedures in Concurrent Programs,, by S. Quadeer, S. Rajamani, J. Rehof,
Proc. of Principles of Programming Languages (POPL), 2004.
Tue, Apr 26: Speaker: Allen Chang
CVC Lite.
Also the paper Simplification by Cooperating Decision Procedures, by Nelson and Oppen.
Thu, Apr 28: Speaker: Raman Sharykin
Timed Automata, by R. Alur and D. Dill,
Journal of Theoretical Comp. Sc., 1994.
Tue, May 2:
Overview of course
