The evolution of computer systems is seeing two trends: increasing ubiquity
(thus we depend more and more on them) and growing complexity (so they
are harder to get right). We face a major challenge to ensure that as
computing becomes more ubiquitous, it is also dependable and secure. The challenge
is to develop and maintain large, complex software systems on top of increasingly
unreliable computing substrates under stringent resource constraints such as
energy usage. We need to advance the science of building correct and robust systems at all
levels of abstraction, from algorithms, through software, to circuits.
This course covers fundamental algorithms and concepts that find widespread use
in ensuring that systems are dependable and secure. In particular, we will
cover algorithmic techniques for formal verification and synthesis, 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 and software systems. We will also cover other
cutting-edge research topics such as quantitative and probabilistic
verification, combining statistical learning and deductive reasoning,
and formal methods for fault tolerance and robust system design.
The course material has applications to several EECS areas including
CAD for integrated circuits, computer security, software engineering,
embedded/cyber-physical systems, control systems, 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,
temporal logic, explicit-state model checking, partial-order reduction,
basic fixpoint theory, symbolic model checking,
abstraction, bounded model checking, interpolation, symmetry reduction,
assume-guarantee reasoning, checking simulation and bisimulation.
- Advanced Topics: Formal methods for synthesis from specifications, Quantitative verification, probabilistic verification,
verifying infinite-state systems, combining learning and deduction, coverage computation,
verifying fault tolerance and robustness, etc.
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.
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!