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

Spring 2024

General Information

Instructor: Sanjit A. Seshia (office: Cory 566)
Class Hours and Location:
Monday and Wednesday, 1-2:30 pm, 299 Cory.
Office Hours:
Monday and Wednesday 2:30-3 pm and by appointment (566 Cory)
Credits: 3 units
Check the bCourses site for this course regularly.

Scribed course notes from a previous year are available here (PDF). An updated set of notes will also be posted on bCourses. 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!):

SAT & BDDs: Complexity, phase transitions, modern DPLL SAT solvers: backjumping, 2-literal watching, conflict-driven learning, etc., proof generation, incremental SAT, circuit SAT. Binary Decision Diagrams, BDD representation and manipulation algorithms, applications.
SMT and Synthesis: Survey of logical theories (uninterpreted functions, linear arithmetic, arrays/memories, bit-vectors, etc.), decision procedures, combination of theories, eager and lazy encoding to SAT, generalized DPLL, syntax-guided synthesis.
Model Checking: Modeling with finite automata, Kripke structures and extended finite automata. Temporal logic. Explicit-state model checking, partial-order reduction. Basic fixpoint theory, symbolic model checking, abstraction, bounded model checking, interpolation and its variants, symmetry reduction, assume-guarantee reasoning, learning finite automata, checking simulation and bisimulation, infinite-state model checking.
Advanced Topics: Formal methods for synthesis from specifications, combining inductive (machine) learning and deduction, formal methods for safe AI, specification inference, emerging applications, etc.

Note: This course was formerly called "Computer-Aided Verification". The title was changed in 2017-18 to more accurately reflect the revisions made in recent years and 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:

Authors: Edmund M. Clarke, Jr., Orna Grumberg, and Doron A. Peled
Title: Model Checking
Publisher: MIT Press
Year: January 2000

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)

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
Author: Gerard Holzmann
Title: The SPIN Model Checker: Primer and Reference Manual
Publisher: Addison-Wesley
Year: September 2003
Author: Rajeev Alur
Title: Principles of Cyber-Physical Systems
Publisher: MIT Press
Year: 2015
Authors: Daniel Kroening and Ofer Strichman
Title: Decision Procedures: An Algorithmic Point of View
Publisher: Springer
Year: 2016

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)

Project: (~60%) The course project is the most important component of this class. It can be a theoretical and/or experimental investigation related to topics covered in class. A list of project topics will be announced in the first three weeks of the semester. You are also encouraged to pick topics of your own, after consulting with the instructor. 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 a few homeworks during the semester get you familiar with basic tools and concepts. The homeworks will be lightly graded. Late homeworks, in general, will not be permitted or will be assessed a penalty. It is more important to attempt the homework fully than to get everything right. Collaboration is permitted, but each person must write up their homework independently, and you must write the names of your collaborators on your homework.
Class Participation and Paper Discussions: (10%) Students will be graded on their participation in class discussions and on discussions of research papers on advanced topics.

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; (~7.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. (~20 %)

Guidelines for Project Presentations:

Time your presentation for 15 minutes (+5 min for questions). It's very important to finish on time. Practise your presentation several times.
Topics to cover:

Motivation, Problem definition, and your approach
Related work and what is new about your work
Your solution. Describe the main technical challenges and how you tackled them.
Hardware/software platform and tools used
Demo (optional) -- could be interleaved with the presentation or performed right after
Finish with a 1-slide summary: what did you achieve, what more can be done?

Guidelines for Project Reports:

One report per team. Deadline: May 9, midnight. Submit on bCourses.
Recommended length: 5-10 pages, use at least 11 pt font
Topics to cover:
1. Introduction & Problem Definition
2. Outline of your Approach and how it compares to related work
3. Formal Model and Algorithms Devised
4. Major Technical Challenges in the Design/Implementation and how you tackled them
5. Summary of Results -- what worked, what didn't, why, ideas for future work
6. A one-paragraph narrative on the roles each team member played in the project
7. How the project applied one or more of the course topics.
8. Feedback: List of topics covered in class that came in handy; any topics that weren't covered that would have been useful
Illustrate algorithms and models with diagrams, and results with graphs, screenshots, pictures of your hardware, etc.
Keep the report short and precise; avoid lengthy and verbose descriptions!

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.

1/17 -- Introduction and Course Overview (slides); Additional viewing: 2007 Turing Award video and 2013 Turing Award video
1/22 - SAT Solving Part I (slides)
1/24 - SAT Solving Part II (In addition to above slides, see: Example 1, Example 2, BCP Intro. BCP Example )
1/29 - SAT Solving (end); Binary Decision Diagrams (BDDs) (slides)
1/31 - Binary Decision Diagrams (BDDs) (slides)
2/5 - Satisfiability Modulo Theories (SMT) - Part I: Modeling (Examples used in class)
2/7 - Satisfiability Modulo Theories (SMT) - Part II: Theories and Theory Solvers (Examples used in class)
2/12 - Satisfiability Modulo Theories (SMT) - Part III: Eager SMT Solving (Eager SMT (see slides 26-66))
2/14 - Satisfiability Modulo Theories (SMT) - Part IV: Lazy SMT Solving (Lazy SMT Examples)
2/19 - President's Day: No class
2/21 - Syntax-Guided Synthesis (SyGuS) (Slides used in class)
2/26 - Modeling for Verification (Example used in class)
2/28 - Invariants, Inductive Invariant Checking, Intro to UCLID5
3/4 - Formal Specification, Temporal Logic (Examples used in class)
3/6 - Explicit-State Model Checking (Extra Slides)
3/11 - Reachability Analysis, Bounded Model Checking, k-Induction
3/13 - Abstraction, CEGAR, Verification by Reduction to Synthesis, UCLID5 Tutorial
3/18 - Simulation and Bisimulation; Compositional Reasoning
3/20 - Project mini-updates
3/25 - Spring break: no class
3/27 - Spring break: no class
4/1 - Hyperproperties: Specification and Verification
4/3 - Interpolation and IC3/PDR
4/8 - Verification by Reduction to Synthesis; Formal Inductive Synthesis; Oracle-Guided Inductive Synthesis (Slides)
4/10 - Specification and Modeling of AI/ML based Autonomy
4/15 - Project Mini-Updates
4/17 - Verification of AI/ML Systems (Simulation, Probabilistic Verification)
4/22 - Run-Time Verification and Assurance (Slides)
4/24 - Conclusion
4/29 - Final Project Presentations (1-2:30 pm in class)
5/1 - Final Project Presentations (1-2:30 pm in class)

Tools

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

SAT solvers/BDD packages:

Finite-State Model checking tools:

SMT solvers and SMT-based verification/synthesis tools:

Cyber-Physical / Timed / Hybrid systems verification / synthesis tools: