[Please remove <h1>]

---

Objectives

This course introduces the theory and practice of computer-aided verification for the design 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 E&CE 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 hrs)

Linear and branching-time temporal logic. Explicit state and symbolic state model checking. State space reduction. Abstraction. Compositional reasoning.

Decision Procedures (5 hrs)

Decision procedures for propositional logic. Decidable subsets of first-order logic.

Mechanized Theorem Proving (5 hrs)

Interactive proof. Automated reasoning. Combining proof tools.

Advanced Topics (8 hrs)

Chosen by the instructor: invariant generation, infinite state systems, non-classical logics, abstract interpretation.