Computer-Aided Verification (Fall 2014)

ECEN 5139, CSCI 5135

Instructor Fabio Somenzi
Lectures Tue, Th 2:00 pm-3:15 pm in ECEE 1B32
Office hours MW 9:00-10:30 am, Th 5:00-6:00 pm, or by appointment

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

Virtual machine for ECEN5139/CSCI 5135