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

Canvas

Everything is on the course Canvas site.

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 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.