Computer-Aided Verification (Fall 2020)

ECEN 5139, CSCI 5135

About the course

Instructor Fabio Somenzi
Lectures Tue, Th 2:20-3.35pm
Office hours Check on Canvas


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.