Temporal logic model checking allows us to decide whether a property stated in a temporal logic holds in a model. With its emphasis on partial verification using fully automated techniques, model checking has become a practical tool for reasoning about hardware and software. This course is aimed to serve as an introduction to the state of the art model checking algorithms and technology. Topics include symbolic, automata-theoretic, bounded and game-theoretic approaches to model checking; query-checking; abstraction and refinement; techniques for model checking software. The course will also give students hands-on experience with current model-checking tools.

• Fall, 2003
• Fall, 2001
• Fall, 2000

• Marsha Chechik