Formal methods describe methods for system-design or system analysis and implementations techniques described by mathematical precision. The goal is to construct systems, which behave according to their specification with a high reliability. This course introduces, both theoretically and practically, the two most important types of formal methods for the analysis of programs: software model checking and deductive verification.
The course addresses the following topics:
Design by Contract with JML
Runtime Assertion Checking
Software Model Checking
First-Order and Dynamic Logic
Construction of Programs Correct-by-Construction
You will be able to download the lecture materials in Stud.IP.