EECS 219C: Computer-Aided Verification

Spring 2015


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

General Information

Course Description

This course is an introduction to the theory and applications of formal methods, a field of computer science and engineering concerned with the rigorous mathematical specification, design, and verification of systems. At its core, formal methods is about proof: formulating specifications that form proof obligations, designing systems to meet those obligations, and verifying, via algorithmic proof search, that the systems indeed meet their specifications. In particular, the course will cover topics such as model checking, Boolean 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) the close connections between verification and synthesis, and (ii) the interplay between inductive inference (learning from examples) and deductive reasoning (logical inference and constraint solving). Based on time and interests, we will also cover other current research topics such as quantitative and probabilistic verification, combining machine learning and formal methods, specification inference, and emerging application areas such as computer networking, robotics, and education.

The course material has applications to several areas in EECS and beyond including computer security, software engineering, embedded/cyber-physical systems, control systems, robotics, networking and distributed systems, education, systems and synthetic biology, and CAD for integrated circuits. We will therefore focus on fundamental theory and techniques that apply broadly to many 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 posted on bCourses; you should come prepared to take notes. The following books may be used in selected parts of the course (copies will be 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
    Website:
    LeeSeshia.org
    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.

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.

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.

Here are some suggested project topics.

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 will be posted below. Lecture slides will be posted alongside where available; note however that most lectures will have scribed notes and these notes and readings will be posted on bCourses.

Tools

Here is an incomplete list of tools that could be useful in your projects.

SAT solvers:

Finite-State Model checking tools:

SMT solvers and SMT-based verification tools: Timed / Hybrid systems verification / synthesis tools:
Copyright 2005-15 Sanjit A. Seshia
Last modified: Wed Mar 4 17:18:49 PST 2015