Fall 2022: Formal Verification of Systems Software
Fall 2022: Formal Verification of Systems Software
Course No:
EECS 498-008
Credit Hours:
4 credits
Instructor:
Manos Kapritsos
Prerequisites:
EECS 491
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.
More info (pdf)