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 1-2pm 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
    • Models of Systems: Reactive modules.
    • Invariant verification.
    • Invariant verification - computational complexity; compositional reasoning.
  • Temporal logic, model checking
    • Temporal logics - Linear temporal logic (LTL); Computational Tree Logic (CTL).
    • CTL model checking.
    • Automata on finite words (review). Automata on infinite words.
    • LTL model checking.
  • "Little engines of proof"
    • Propositional logic. Introduction to SAT (satisfiability) solving.
    • Resolution; DPLL algorithm for SAT.
    • CDCL algorithm for SAT.
    • SMT (satisfiability modulo theories).
    • Satisfiability-based model checking: BMC.
    • Satisfiability-based model checking: Interpolation.
  • Program verification
    • Operational Semantics.
    • Hoare logic.
    • Proving Termination.
    • Weakest (liberal) precondition.
    • Verification condition generation.
    • Abstract Interpretation.

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 6: project proposal
  • November 11: checkpoint (project works on motivating examples)
  • December 10: project submission deadline (submit source code, examples, 4-page project report)
  • December 10,12: project presentations, demos

Relevant links

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

Grading

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.