EECS 219C: Formal Methods: Specification, Verification, and Synthesis

Spring 2018


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

General Information

Scribed course notes from a previous year are available here (PDF). Please email the instructor if you have any feedback on these notes or find typos.

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 combining machine learning and formal methods, formal methods for safe and high assurance artificial intelligence (AI) and robotics, formal methods for building secure systems, formal methods for human-robot (human-CPS) systems, formal methods for education, etc.

The course material has applications to several areas in EECS and beyond including computer security, software engineering, embedded/cyber-physical systems, artificial intelligence, 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!):

Note: This course was formerly called "Computer-Aided Verification". The title was changed in 2017-18 to more accurately reflect the broad content in formal methods covered in the course.

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:
  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
    Publisher: MIT Press
    Year: 2016
  4. Author: Gerard Holzmann
    Title: The SPIN Model Checker: Primer and Reference Manual
    Publisher: Addison-Wesley
    Year: September 2003
  5. Author: Rajeev Alur
    Title: Principles of Cyber-Physical Systems
    Publisher: MIT Press
    Year: 2015
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 formal methods, or a new formal 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.

Suggested project topics will be posted here.

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; (~20 %)
4. Project presentation and possibly demo. (~15 %)

Guidelines for Project Presentations:

Guidelines for Project Reports:

Course Topics and Schedule (Tentative: Subject to change!)

The tentative course schedule is posted below. Lecture slides will be posted alongside where available; note however that most lectures will done on the whiteboard. Scribed notes and readings will be posted on bCourses/this webpage.

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/synthesis tools: Timed / Hybrid systems verification / synthesis tools:
Copyright 2005-18 Sanjit A. Seshia
Last modified: Mon Jan 16 12:39:01 PDT 2018