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