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!):
- 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.
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.
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:
- Time your presentation for 15 minutes.
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. Hard deadline: TBD at midnight. Submit on bCourses.
- Recommended length: 5-10 pages, use at least 11 pt font
- Topics to cover:
- Introduction & Problem Definition
- Outline of your Approach and how it compares to related work
- Formal Model and Algorithms Devised
- Major Technical Challenges in the Design/Implementation and how you tackled them
- Summary of Results -- what worked, what didn't, why, ideas for future work
- A one-paragraph narrative on the roles each team member played in the project
- How the project applied one or more of the course topics.
- 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!