Computer-Aided Verification (Fall 2018)

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 ECOT 349, and by appointment


Everything is on the course Canvas 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 through Airbus to Facebook develop and use computer-aided 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.