EECS 219C: Computer-Aided Verification

(Algorithmic Formal Methods for System Design, Verification, and Dependability)

Spring 2011


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

General Information

Course Description

The evolution of computer systems is seeing two trends: increasing ubiquity (thus we depend more and more on them) and growing complexity (so they are harder to get right). We face a major challenge to ensure that as computing becomes more ubiquitous, it is also dependable and secure. The challenge is to develop and maintain large, complex software systems on top of increasingly unreliable computing substrates under stringent resource constraints such as energy usage. We need to advance the science of building correct and robust systems at all levels of abstraction, from algorithms, through software, to circuits.

This course covers fundamental algorithms and concepts that find widespread use in ensuring that systems are dependable and secure. In particular, we will cover algorithmic techniques for formal verification and synthesis, 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 and software systems. We will also cover other cutting-edge research topics such as quantitative and probabilistic verification, combining statistical learning and deductive reasoning, and formal methods for fault tolerance and robust system design.

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

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

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

(tentative)

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

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

Homeworks/Project Milestones

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

Tools

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: Thu May 5 21:46:56 PDT 2011