Computer-Aided Verification (Fall 2019)

ECEN 5139, CSCI 5135

About the course

Instructor Fabio Somenzi
Lectures Tue, Th 2-3.15pm in ECEE 265
Office hours Th 3.30-5.00pm in ECOT 348, 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.