# CS 745 Computer-Aided Verification

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