EECS 219C: Computer-Aided Verification

(Model Checking and Computational Logic)

Spring 2007

General Information

Instructor: Sanjit A. Seshia (office: Cory 568)
Class Hours and Location:
Monday & Wednesday, 10:30 am - 12 noon, in 531 Cory
Office Hours:
Mon. 2 - 3 pm, Wed. 1 - 2 pm, in 568 Cory
Credits: 3 units

Authors: Edmund M. Clarke, Jr., Orna Grumberg, and Doron A. Peled
Title: Model Checking
Publisher: MIT Press
Year: January 2000
Acronym: MC
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:-

Author: Gerard Holzmann
Title: The SPIN Model Checker: Primer and Reference Manual
Publisher: Addison-Wesley
Year: September 2003
Acronym: SPIN

If you lack background in one of the areas mentioned under "pre-requisites" above, please see here for a list of suggested books.

Grading

Project: (50%) The course project is the most important component of this class. It must be a theoretical and/or experimental investigation into the use of model checking or other techniques in computational logic into problems in verification, synthesis, planning, etc. Potential project topics will be announced in the first two weeks of the semester. It is expected that students team up in groups of 2 or 3 for their project. Projects will culminate in a final paper, presentation, and possibly a demo.
Homeworks: (30%) There will be 3 homework assignments on the first half of the course, weighted equally. Assignments will include both theoretical problems and experimentation with verification tools. Homeworks will be due at the beginning of class.
Teamwork: Students may collaborate on homeworks, but each student must individually write up his or her solutions and be prepared to present it in class on the due date. Indicate on your homework the names of those you have collaborated with and on which problems.
Class Presentation: (15%) The latter half of the course will be on current research topics. Students will be required to sign up to present a topic in class based on a few assigned papers. Depending on the ratio of class size to number of topics, this could be done in teams of 2 people. (The list of papers will be up by the second week of class.)
Class Participation: (5%) Ask questions and participate in class discussions!

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: