CSIL Courses

Lecture overview. Overview of course

  • 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