Winter 2024: Formal Verification of Systems Software

Winter 2024: Formal Verification of Systems Software

Course No:
EECS 498-009
Credit Hours:
4 credits
Instructor:
Manos Kapritsos
Prerequisites:
None

During this course, you will learn how to formally specify a system’s behavior, how to prove that the high-level design of the system meets that specification and finally how to show that the system’s low-level implementation retains those properties. The course does not assume any prior knowledge in formal verification. We will start from the basics of the Dafny language and build from there. In the end, you should be able to design and prove correct a complex system. The experience of doing so will make you a more careful and effective programmer, even when you don’t write formally verified code.

More info (pdf)