Instructor |
Pavol Cerny |

Lectures |
Tue, Th 3:30pm-4.45pm in ECCR 150 |

Office hours |
Th 2-3pm in ECEE 120, and by appointment |

# Course description

Hardware and software systems are very hard to design correctly. (In)famous errors in systems include bugs in a Pentium processor and in the Ariane V rocket. More recently, software bugs are a common cause of car recalls. Companies from Intel to Airbus make full use of formal verification. We will see:- How to specify correctness of your system: assertions, pre-post conditions, temporal logic.
- Algorithms for verification of systems: model checking and abstract interpretation.
- Little engines of proof: constraint solvers, decision procedures.

# Schedule

- Introduction: Models of Systems, Invariant Verification.
- August 26: Introduction to Computer-Aided Verification
- August 28: Models of systems: Reactive Modules (part 1). HW1 posted, due September 11.
- Sept 2, 4: Models of systems: Reactive Modules (part 2). Parallel composition. Semantics.
- Sept 9, 11: Invariant verification. Algorithms, computational complexity; compositional reasoning.

- Temporal logics, model checking
- Sept 16: Temporal logics. Computational Tree Logic (CTL). HW2 posted, due September 30.
- Sept 18: Verification at Xilinx. Guest lecture by Graham Schelle.
- Sept 23: Computational Tree Logic (CTL). CTL model checking.
- Sept 25: Invariance and Termination in Probabilistic Programs. Lecture by Sriram Sankaranarayanan.
- Sept 30: CTL model checking (part II). Expressiveness of CTL.
- Oct 2: Linear temporal logic (LTL).
- Oct 7: Automata on finite words (review). Automata on infinite words.
- Oct 9: LTL model checking.
- Oct 14: Midterm 1.
- Oct 16: LTL model checking (part II). HW 3 posted. Due October 30.

- "Little engines of proof"
- Oct 21: Propositional logic. Introduction to SAT (satisfiability) solving.
- Oct 23, 28: Resolution; DPLL algorithm for SAT.
- Oct 30: CDCL algorithm for SAT. HW 4 posted. Due November 13.
- Nov 4: Satisfiability-based model checking: BMC, Interpolation.

- Program verification
- Nov 6, 11: Operational Semantics, Hoare Logic.
- Nov 13: Proving Termination.
- Nov 18: Verification condition generation. HW5 posted, due Dec 2.
- Nov 20, Dec 2: Abstract Interpretation.
- December 4: Midterm 2.

- Course projects
- December 9, December 11: Project presentations

# Course project

The goal of your project is to perform a substantial verification case study in the domain of your choice, ideally related to your research. Alternatively, you can implement an optimization to an open-source verification tool. Project deadlines:- October 7: project proposal, two pages
- November 18: checkpoint (project works on motivating examples), three-page description
- December 8: project submission deadline (submit source code, examples, six-page project report)
- December 9,11: project presentations, demos

# Relevant links

- Lecture notes: Formal Verification of VLSI systems by Fabio Somenzi. Available on Moodle.
- Book: Computer-Aided Verification by Rajeev Alur and Thomas Henzinger. Available here and on Moodle.
- Book: The Calculus of Computation by Aaron Bradley and Zohar Manna. Required.
- Model checker Spin.
- Model checker NuSMV.
- Software verifier Dafny.