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.
Three hours of lecture per week. This course will be cross-listed with E&CE
Algebraic and logical preliminaries: partial orders, lattices, lambda-calculus. Classical logic. Automata. Formal modelling and specification.
Linear and branching-time temporal logic. Explicit state and symbolic state model checking. State space reduction. Abstraction. Compositional reasoning.
Decision procedures for propositional logic. Decidable subsets of first-order logic.
Interactive proof. Automated reasoning. Combining proof tools.
Chosen by the instructor: invariant generation, infinite state systems, non-classical logics, abstract interpretation.