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.


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


Menu:ShowHide