||Tue, Th 3:30pm-4.45pm in ECCR 150
||Th 2-3pm in ECEE 120, and by appointment
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
- Little engines of proof: constraint
solvers, decision procedures.
Introduction: Models of
Systems, Invariant Verification.
- August 26: Introduction to Computer-Aided
- 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
- Sept 23: Computational Tree Logic (CTL). CTL
- 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
- 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,
- 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.
- December 9, December 11: Project presentations
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.
- 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
- Lecture notes: Formal Verification of VLSI systems by Fabio
- Book: Computer-Aided Verification by Rajeev Alur and
Henzinger. Available here
and on Moodle.
The Calculus of Computation
by Aaron Bradley and Zohar Manna. Required.
- Model checker NuSMV.
The course will be graded based on a course project (30% of
the course grade), homework (30%), exams (30%), and in-class
A statement of class policies is