Rationale for Introduction of this Course

• Reliability and safety of software in critical applications is a major concern in security, medical applications, telecommunication industry etc. Formal verification is among the most promising techniques for addressing this concern. Formal verification is everyday practice in hardware design, and major software companies are actively pursuing this direction.

• Similar courses (with the same textbook) is taught in dozens if not hundreds of universities around the world including Princeton, CMU, Cambridge, McGill and Toronto.

• The course is useful for all students -- it introduces a rigorous approach to software engineering.

• It is a natural addition to our software engineering program -- it's about building correct and reliable systems.

• The course provides a connection with research interests of several faculty members in the department. Through this course, a few very good students were attracted to our graduate program.

• Students really like this course. They learn a formal, mathematically transparent theory, and immediately see how it works in practice by designing and verifying their own systems.

Will this be a required or elective course in the curriculum?

Elective for now. I intend to propose it as a required course for the software engineering stream in the future. It would increase the proportion of courses with formal content in this stream, which is currently quite low.

Probable enrollment when offered? Around 30