Computer-Aided Verification (Fall 2017)

ECEN 5139, CSCI 5135

About the course

Instructor Pavol Cerny
Lectures Tue, Th 2-3.15pm in ECEE 265
Office hours Th 3.30-4.30pm in ECEE 120, and by appointment


Everything is on the course Moodle site.


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.