CS 745 Computer-Aided Verification


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.


Course notes.


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


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.

Campaign Waterloo

David R. Cheriton School of Computer Science
University of Waterloo
Waterloo, Ontario, Canada N2L 3G1

Tel: 519-888-4567 x33293
Fax: 519-885-1208

Contact | Feedback: cs-webmaster@cs.uwaterloo.ca | David R. Cheriton School of Computer Science | Faculty of Mathematics

Valid HTML 4.01!Valid CSS! Last modified: Friday, 01-Jun-2012 11:00:32 EDT