EECS 219C: Computer-Aided Verification

(Model Checking and Computational Logic)

Spring 2006

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 concerns the use of algorithmic methods in verifying the dependability and performance of computer systems, both software and hardware. 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.


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 would be useful, 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.



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).

Here is the project schedule.

Anticipated Topics and Schedule

Lec. Date Topics Suggested Readings Homeworks & Milestones
1 1/18 Introduction (PDF)
  • Overview of model checking
Part I: Foundations -- Systems with Boolean State
2 1/23 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/25 Boolean Satisfiability - Part II ( PDF of Main Lecture, Example 1, Example 2, BCP Intro. )
  • Recent techniques: Non-chronological backtracking, 2-literal watching, conflict-driven learning, decision heuristics, ...
  • Incremental SAT solving
  • Proof generation
L. Zhang thesis (Ch. 3, 4)  
  1/30 Class cancelled -- make-up class on 2/17 from 12:30 - 2pm in Cory 299   HW 1 out, Project topics announced
4 2/1 Binary Decision Diagrams ( PDF of Main Lecture, BCP Example )
  • 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  
5 2/6 Models and Properties ( PDF )
  • Finite-state machines, Kripke structures, etc.
  • Synchronous vs. asynchronous systems
  • System behaviors as traces
MC Ch. 2 HW 1 due
6 2/8 Finite-State Model Checking -- Introduction ( PDF )
  • Temporal logic - LTL, CTL, CTL*
MC Ch. 3 HW 2 out
7 2/13 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/15 More Explicit-State Model Checking ( PDF )
  • Verifying liveness properties
  • Optimizations -- partial-order reduction, etc.
SPIN Ch. 8, 9; MC Ch. 10  
9 2/17 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 HW 2 due
  2/20 President's Day Holiday    
10 2/22 More Symbolic Model Checking and Abstraction ( PDF )
  • Counterexample generation
  • Fairness
  • Optimizations
  • Basics of abstraction
MC. Ch. 6: 6.3, 6.4, 6.6, Ch. 13: 13.1 Project proposal due
11 2/27 Abstraction (contd.) and Symbolic Model Checking without BDDs ( PDF )
  • Counterexample-guided abstraction refinement
  • Bounded model checking
  • Proof-based abstraction
12 3/1 More Abstraction; Notions of Simulation and Language Equivalence ( PDF )
  • Interpolation-based model checking
  • Language equivalence, containment, similarity, bisimilarity
  • Algorithm for simulation checking
McMillan paper, Ch. 11 HW 3 out
13 3/6 Compositional Reasoning and Symmetry; Mu-Calculus ( PDF )
  • Symmetry reduction
  • Assume-guarantee reasoning
  • Mu-Calculus
MC Ch. 14, 12, 7  
14 3/8 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) HW 3 due
15 3/13 Games and Verification ( PDF )
  • Modeling open systems
  • Controller synthesis as a game
  • Solving safety games
F. Mang's thesis HW 4 out
  3/15 Class rescheduled to 3/17 from 12:30 - 2pm in Cory 299    
16 3/17 Model Generation from Traces ( PDF )
  • Motivation and problem setup
  • Angluin's DFA learning algorithm
Part II: Systems with Non-Boolean State and Applications
17 3/20 First-order logic and SAT-Based Automated Theorem Proving ( PDF-1, PDF-2 )
  • Terminology
  • Modeling with first-order logic
  • Classification of SAT-Based Approaches
  • UCLID: Eager Encoding to SAT
S. Seshia thesis  
18 3/22 More SAT-Based Automated Theorem Proving ( PDF )
  • The Lazy Encoding Approach: Verifun, CVC-Lite, ICS, MathSAT, etc.
  HW 4 due; HW 5 out
  3/27 Spring recess    
  3/29 Spring recess Part II required readings below  
19 4/3 Interface Automata: Theory and Applications. Guest lecture by Arindam Chakrabarti. ( PDF ) [dAH01]  
20 4/5 Software Verification I: Abstraction-based Model Checking. Guest lecture by Prof. Rupak Majumdar. ( PDF )
  • Predicate abstraction
  • The Blast model checking project (& comparison with SLAM)
SLAM (pdf), Bebop (pdf), Blast. HW 5 and Project preliminary report due
21 4/10 Software Verification II: Execution-based Model Checking
  • Execution-based and explicit-state approaches: Verisoft, CMC, etc.
VeriSoft (ps), CMC (pdf)  
22 4/12 Software Verification III: Reasoning about Concurrency
  • Compositional Reasoning; the Zing model checker
Zing overview (pdf), [QRR04] (pdf), [FQ03] (ps) HW 6 out
23 4/17 Model Checking Real-Time Systems
  • Discrete real-time
  • Dense real-time
[Alur97] (gzipped ps)  
  4/19 Class cancelled (Sanjit travelling)    
24 4/24 Model Checking Hybrid Systems [ACH+95] HW 6 due
25 4/26 Hardware and System-Level Verification
  • Processor verification
  • Arithmetic circuit verification
  • Bounded model checking of software
[BD94] (pdf), [CB95] (pdf), CBMC (pdf)  
26 5/1 Computational Logic and Security
  • Cryptographic protocol analysis
Course wrap-up
[CJM00] (pdf, can skip Sec. 4.2, 4.3), [MMS97] (ps, can skip Sec. 4)  
  5/3 Project presentations - I   Final project report due May 7th, 5 pm.
  5/8 Project presentations - II    


Some homeworks will involve experimentation with the following tools:

Copyright 2005-06 Sanjit A. Seshia
Last modified: Sun Aug 27 13:49:51 PDT 2006