Computer-Aided Verification (Fall 2014)

ECEN 5139, CSCI 5135

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.


  • 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.


The course will be graded based on a course project (30% of the course grade), homework (30%), exams (30%), and in-class participation (10%).

Syllabus statement

A statement of class policies is available here.