Calendar Description

Objectives

This course introduces the theory and practice of computer-aided verification for the design and analysis of digital systems (i.e., hardware and software systems). It emphasizes formal methods techniques, i.e., techniques based on logical reasoning and mathematical modelling, which are gradually being incorporated into CASE and CAD tools. These techniques have been used to find subtle, critical logic and safety errors in industrial hardware and software systems.

References

Course notes.

Schedule

Three hours of lecture per week. This course will be cross-listed with ECE 725.

Outline

Theory and Modelling (10 hrs)
Algebraic and logical preliminaries: partial orders, lattices, lambda-calculus. Classical logic. Automata. Formal modelling and specification.

Temporal Logic and Model Checking (8 hours)
Linear and branching-time temporal logic. Explicit state and symbolic state model checking. State space reduction. Abstraction. Compositional reasoning.

Decision Procedures (5 hours)
Decision procedures for propositional logic. Decidable subsets of first-order logic.

Mechanized theorem proving (5 hours)
Interactive proof. Automated reasoning. Combining proof tools.

Advanced Topics (8 hours)
Chosen by the instructor. e.g., Invariant generation, Infinite state systems, Non-classical logics, Abstract interpretation.