EECS 219C: Computer-Aided Verification

Fall 2012

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

General Information

Course Description

This course covers fundamental algorithms and modeling techniques for formal verification and synthesis of systems. In particular, we will cover topics such as model checking, satisfiability (SAT) solving and satisfiability modulo theories (SMT). These techniques have become essential tools for the design and analysis of hardware, software, and cyber-physical systems. Central themes of the course this year will include (i) automated symbolic modeling and reasoning, (ii) exploration-driven generalization, and (iii) the interplay between inductive inference (learning from examples) and deductive reasoning (logical inference and constraint solving). We will also cover other cutting-edge research topics such as quantitative and probabilistic verification, combining statistical learning and formal methods, specification inference, error localization and explanation, and the use of crowdsourcing in verification.

The course material has applications to several EECS areas including computer security, software engineering, embedded/cyber-physical systems, control systems, and CAD for integrated circuits and biological systems.

A tentative list of topics to be covered: (subject to change!):


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 posted on bSpace; you should come prepared to take notes. The following books will be used in selected parts of the course (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
  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)
  3. Authors: Edward A. Lee and Sanjit A. Seshia
    Title: Introduction to Embedded Systems: A Cyber-Physical Systems Approach
    Year: 2011
  4. Author: Gerard Holzmann
    Title: The SPIN Model Checker: Primer and Reference Manual
    Publisher: Addison-Wesley
    Year: September 2003
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. Projects that are simply surveys of existing papers without any input of new ideas will not be acceptable.

In each of the past offerings, more than 50% of the projects have resulted in published conference papers. You are highly encouraged to work towards publishable results.

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. Mini-update presentations, describing progress on the timeline; (~5 % each)
3. 5-10 page final report: This should read like a conference paper, must use at least 11 pt font; (~25 %)
4. Project presentation and possibly demo. (~20 %)

Guidelines for Project Presentations:

Guidelines for Project Reports:

Course Topics and Schedule (subject to change)

The tentative course schedule is given below. Lecture slides will be posted alongside; readings will be posted on bSpace.

Homeworks/Project Milestones

Homeworks are posted on bSpace. Project milestones as announced in class.


Some homeworks will involve experimentation with the following tools:
Links to more tools will be added here as needed.
Copyright 2005-11 Sanjit A. Seshia
Last modified: Fri Nov 30 17:53:49 PST 2012