Time: Mondays, 10:30-12:00 and Tuesdays, 14:30-16:00
Location: Stong College, room 221 (Mondays) and TEL Building, room 0004 (Tuesdays)
Instructor: Franck van Breugel, franck@cse.yorku.ca
Office Hours: Lassonde Building, room 3046

Time: Thursdays, 14:30-15:30
Location: Lassonde Building, lab 1004
Teaching Assistant: Qiyi Tang, qiyitang@cse.yorku.ca

This course is a sequel to System Specification (EECS3342) which is an introduction to mathematical modeling and refinement of systems using deductive methods.

This course provides students with a deeper understanding of both deductive and algorithmic methods and tools for ensuring the safety and correctness of mission critical systems (e.g. medical devices such as pacemakers, nuclear reactors and train control systems). In addition to deductive techniques, the course treats algorithmic methods such as model-checking tools, specification languages such as temporal logic, table based specification methods, and the nature of software certification.

The textbook for this course is

• Christel Baier and Joost-Pieter Katoen. Principles of Model Checking. The MIT Press. 2008.

Additional reading material will be provided on this course wiki.

Students can view their marks using the ePost system.