Course Description
This course covers fundamental algorithms and modeling techniques
for formal verification and synthesis of systems.
In particular, we will cover topics such as model
checking, 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) automated symbolic modeling and reasoning,
(ii) exploration-driven generalization, and
(iii) the interplay between inductive inference (learning from examples)
and deductive reasoning (logical inference and constraint solving).
We will also cover other
cutting-edge research topics such as quantitative and probabilistic
verification, combining statistical learning and formal methods,
specification inference, error localization and explanation,
and the use of crowdsourcing in verification.
The course material has applications to several EECS areas including
computer security, software engineering, embedded/cyber-physical systems,
control systems, and CAD for integrated circuits and biological 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: 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.
- 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, error localization and explanation,
specification inference, crowdsourcing in verification, 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: Friday, May 13 at midnight. Submit on bSpace.
- 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!