Skip to content. Skip to navigation
McGill Home SOCS Home
Personal tools
You are here: Home Academic Courses Course Profile


Course Summary

Model checking is an automated technique for proving that a system (described as a transition system) satisfies a specification written in some formal language. In this class we develop the logic background, especially temporal logic and show how model checking works. We study binary decision diagrams which have allowed industrial strength systems to be verified in practice. We end with special topics like Buchi automata and real-time systems.

McGill Course Description (Click Here)