EECS 219C: Computer-Aided Verification

(Model Checking and Computational Logic)

Spring 2007


Short-cuts: [   Description   |   Prerequisites   |   Books   |   Grading   |   Projects   |   Schedule   |   Tools   ]

General Information

Course Description

The evolution of computer systems is seeing two trends: growing complexity (so they are harder to get right) and increasing ubiquity (thus we depend more and more on them). The dependability of complex computer systems can no longer be sufficiently evaluated and controlled only by the traditional approaches of testing and simulation. Model checking is a collection of algorithmic methods based on state space exploration used to verify the correctness of systems. Computational logic concerns the use of mathematical logic to reason about computation. In this course, students will be introduced to the theory and practice of model checking and related topics in computational logic. Application areas discussed will include topics in both Electrical Engineering and Computer Science, including hardware and software verification, analysis of real-time, embedded, and hybrid systems, computer security, planning in AI, hardware and software synthesis, and constraint solving.

Prerequisites

Familiarity with propositional logic, finite automata, basic computational complexity classes (P, NP, PSPACE), and basic graph algorithms is assumed. An undergraduate course in algorithms such as CS 170 is highly recommended, but is not mandatory. EE 219A, EE 219B, and CS 172 are NOT needed. If you are unsure whether you have sufficient background for the course, please meet the instructor.

Reference Books

There is no required textbook for this course. Readings will be listed on the schedule below or handed out in class. The following books are highly recommended (copies are on reserve at the Engineering library):
  1. Authors: Edmund M. Clarke, Jr., Orna Grumberg, and Doron A. Peled
    Title: Model Checking
    Publisher: MIT Press
    Year: January 2000
    Acronym: MC
  2. Authors: Michael Huth and Mark Ryan
    Title: Logic in Computer Science: Modelling and Reasoning about Systems
    Publisher: Cambridge Univ. Press
    Year: June 2004 (2nd edition)
    Acronym: LICS
Additional reference books:- If you lack background in one of the areas mentioned under "pre-requisites" above, please see
here for a list of suggested books.

Grading

Projects

The key point about the course project is that there should be some new research in it: either a new application of existing verification technology, or a new verification technique, or both. (Note: it doesn't have to be wholly about verification -- e.g., it could be an application of "verification technology" such as SAT solving to synthesis.) Projects that are simply surveys of existing papers without any input of new ideas will not be acceptable.

The main deliverables (in chronological order) will be:
1. 1-2 page proposal, with precise problem definition, literature survey, and timeline; (5 % towards final grade)
2. 1-2 page preliminary report, describing progress on the timeline; (5 %)
3. 4-6 page final report: This should read like a conference paper, must use at least 10 pt font; (~20 %)
4. Project presentation and possibly demo. (~20 %)

Here is a list of suggested projects (Berkeley campus access only).

Course Topics and Schedule (subject to change)

Lec. Date Topics Suggested Readings Homeworks & Milestones
1 1/17 Introduction (PDF)
  • 25 years of model checking -- history, opportunities, and challenges
   
Part I: Computational Engines
2 1/22 Boolean Satisfiability - Part I (PDF)
  • Terminology
  • Some motivating applications
  • Complexity, special cases, phase transition behavior
  • Survey of SAT algorithms, with focus on DPLL-based
L. Zhang thesis (Ch. 2)  
3 1/24 Boolean Satisfiability - Part II ( PDF of Main Lecture, Example 1, Example 2, BCP Intro. BCP Example )
  • Recent techniques: Non-chronological backtracking, 2-literal watching, conflict-driven learning, decision heuristics, ...
  • Incremental SAT solving
  • Proof generation
L. Zhang thesis (Ch. 3, 4)  
4 1/29 Binary Decision Diagrams ( PDF )
  • Definitions and Basic Properties
  • Constructing BDDs
  • Variable ordering
  • Bounds on BDD size
  • BDD variants
R. E. Bryant's 1992 Computing Surveys paper, MC Sec. 5.1  
Part II: Foundations of Model Checking -- Systems with Boolean State
5 1/31 Models and Properties ( PDF )
  • Finite-state machines, Kripke structures, etc.
  • Synchronous vs. asynchronous systems
  • System behaviors as traces
MC Ch. 2 HW 1 out, Project topics announced
  2/5 Class cancelled (grad admissions meeting); will be rescheduled -- Decide on your project topics!    
6 2/7 Finite-State Model Checking -- Introduction ( PDF )
  • Temporal logic - LTL, CTL, CTL*
MC Ch. 3  
7 2/12 Explicit-State Model Checking ( PDF )
  • Recap of models & properties, temporal logic & automata
  • Invariant verification as graph reachability
  • Search: depth-first, breadth-first
  • The SPIN model checker
MC Ch. 9: 9.1, 9.2; SPIN Ch. 6, 8  
8 2/14 More Explicit-State Model Checking ( PDF )
  • Verifying liveness properties
  • Optimizations -- partial-order reduction, etc.
SPIN Ch. 8, 9; MC Ch. 10 HW 1 due;
HW 2 out
  2/19 President's Day Holiday    
9 2/21 Symbolic Model Checking with BDDs ( PDF )
  • Basics of symbolic representation
  • Quantified Boolean Formulas
  • Fixpoint theory
  • CTL model checking algorithms, the SMV model checker
MC Ch. 5, Ch. 6: 6.1, 6.2 Project proposal due
10 2/23 More Symbolic Model Checking and Abstraction
(Make-up lecture, 540 Cory 11 - 12:30) ( PDF )
  • Counterexample generation
  • Fairness
  • Optimizations
  • Basics of abstraction
MC. Ch. 6: 6.3, 6.4, 6.6, Ch. 13: 13.1  
11 2/26 Abstraction (contd.) and Symbolic Model Checking without BDDs ( PDF )
  • Counterexample-guided abstraction refinement
  • Bounded model checking
  • Proof-based abstraction
   
12 2/28 More Abstraction; Notions of Simulation and Language Equivalence ( PDF )
  • Interpolation-based model checking
  • Language equivalence, containment, similarity, bisimilarity
  • Algorithm for simulation checking
[McMillan 2003],
[McMillan 2005],
Ch. 11
HW 2 due;
HW 3 out
13 3/5 Compositional Reasoning and Symmetry; Mu-Calculus ( PDF )
  • Symmetry reduction
  • Assume-guarantee reasoning
  • Mu-Calculus
MC Ch. 14, 12, 7  
14 3/7 Pushdown Model Checking ( PDF )
  • Symbolic representation
  • Reachability analysis - backward and forward
  • LTL model checking
S. Schwoon's thesis (Sec. 2.1 - 2.3, Ch. 3)  
15 3/12 Games and Verification ( PDF )
  • Modeling open systems
  • Controller synthesis as a game
  • Solving safety games
F. Mang's thesis  
16 3/14 Model Generation from Traces ( PDF )
  • Motivation and problem setup
  • Angluin's DFA learning algorithm
  HW 3 due
Part III: Research Frontiers
17 3/19 Satisfiability Modulo Theories ( PDF )
  • Focus on finite-precision bit-vector arithmetic & arrays/memories
[Barrett et al. 1998];
[Bryant et al. 2007]
 
18 3/21 No regular class. Instead, attend Prof. Ranjit Jhala's lecture on software model checking on 3/22, from 11:30 am - 1 pm, in 405 Soda    
  3/26 Spring recess    
  3/28 Spring recess    
19 4/2 No regular class. Instead, attend paper presentation on Runtime Monitoring in Prof. Sen's CS 294-5 class on 4/3, 11:30 am - 1 pm in 405 Soda    
20 4/4 Learning Algorithms in Model Checking: Abstraction and Assume-Guarantee Reasoning
(Guest lecture by Dr. Anubhav Gupta, Cadence Berkeley Labs) ( PDF )
  Project preliminary report due by e-mail to Sanjit on 4/6
21 4/9 Coverage Metrics for Formal Verification (Wenchao Li) ( PDF ) [Hoskote et al. 1999];
[Chockler et al. 2006]
 
  4/11 Class rescheduled to Friday (Sanjit at SRC review)    
22 4/13 Error Localization and System Repair [11 am - 12:30 pm, in 540 Cory]
(Shyam Rajagopalan) ( PDF )
  • Links to optimization and games
[Groce et al. 2005];
[Griesmayer et al. 2006]
 
23 4/16 Parallelism in Verification (Rhishikesh Limaye) ( PDF )
  • Parallel and distributed algorithms for SAT and model checking
[Melatti et al. 2006];
[Feldman et al. 2004]
 
  4/18 Class cancelled (Sanjit away at DATE conference)    
24 4/23 Combining Multiple Tools and Techniques (Sungmin Cho) ( PDF )
  • Formal & semi-formal, static & dynamic, etc.
  • Focus on algorithms, for both hardware and software
[Ho et al., 2000]
[Gulavani et al., 2006]
 
25 4/25 Model Checking Hybrid Systems (Jia Zou) ( PDF ) [Alur et al., 1995]
[Agrawal and Thiagarajan, 2005]
 
26 4/30 Computational Logic and Security (Susmit Jha) ( PDF )
  • Temporal logic for privacy
  • Verifying secrecy
[Blanchet 2006]
[Barth et al., 2006]
 
27 5/2 Specifications: Choice of logic, and synthesis (Narayanan Sundaram) ( PDF )
  • LTL vs CTL
[Vardi 2001]
 
  5/7 Project presentations (9:30 am to 12 noon in 540 Cory)   Final project report due

Tools

Some homeworks will involve experimentation with the following tools:

Copyright 2005-07 Sanjit A. Seshia
Last modified: Wed Feb 14 19:29:01 PST 2007