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!):
- 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 Beyond: 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,
quantitative verification, probabilistic verification,
combining inductive learning and deduction,
specification inference, emerging applications, etc.