Department of Computer Science
CPSC 538D: Verification of Mixed Hardware-Software Systems (96W)

Link to Readings, Projects, Schedule, etc.

Instructor: Alan Hu, CICSR 325, A J H at C S dot U B C dot C A

Overview:

This course will be a graduate-level survey of several automatic formal verification methods and paradigms that are rapidly gaining industrial importance. Ideally, I'd like this course to serve two purposes: (1) provide a broad, solid foundation for further research in this area, and (2) give students practical, general exposure so they will be better equipped to understand, evaluate, and use these techniques in the future, even if they don't pursue research in this area.

Main topics to be covered will likely include BDDs and associated algorithms, CTL model checking, LTL and the tableaux procedure, symbolic trajectory evaluation, partial order and symmetry reductions, and omega automata. The theoretical topics will be motivated by practical applications such as comparing logic circuits, checking multiprocessor cache coherence protocols, and verifying correctness of pipelined processors.

Evaluation:

Assignments will consist of pencil-and-paper homework to understand the theory, and several small projects to gain hands-on experience with the verification tools. There will be no final exam.

Textbook:

There is no textbook for the course. Readings will come from the original research papers.

Prerequisites:

Graduate standing or consent of instructor. I intend to make the course fairly self-contained, but familiarity with finite automata, basic digital logic, and some computer architecture will be helpful.