Part I. Hoare Logic and Deductive Verification
1. Code Annotation: The Java Modelling Language
2. Automated Static Assertion Checking: Weakest Preconditions
3. The Correctness-by-Construction Approach to Programming
4. Ghost State and Control-flow Abstraction
5. Model State and Data Abstraction
6. The Back-end: Automated Theorem Proving
Part II. Temporal Logic and Model Checking
7. Kripke Structures and System Modelling
8. Temporal Logic and Model Checking: LTL and CTL
9. Software Model Checking
The overall aim of the course is to provide a working familiarity with the main methods and tools in the formal methods area, in theory as well as in practice.
After passing the course, the students should be able to:
1. Independently select a suitable modeling approach for some given simple problem;
2. Argue informally and formally for the soundness and limitations of the chosen approach;
3. Identify, specify and verify important system properties using suitable automated or semi-automated tools;
4. Correctly interpret and evaluate the results of the analysis.
For passing the course, a student has to demonstrate the ability to apply the methods discussed in the course; for the highest grade he/she has also to be proficient in the theoretical foundations of these methods.