Lecturer: Prof. Dr. Ina Schaefer
Assistant: Tabea Bordis, M.Sc.
Module number: INF-SSE-38
Lecture number: INF-SSE-050 / INF-SSE-051
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:
The lecture Software Quality 2 will be held completely online this semester. You will be able to download the lecture materials in Stud.IP. Please enroll yourself in the Stud.IP course and the tutorial Software Quality 2. You are not allowed to publicly release any of the given material.
For the lecture, we will upload slides and video casts of the lecture.
For the tutorial, we will upload exercise sheets with exercises for a distinct topic of the lecture. Some of the exercises, can only be solved on a computer. If tools are required for any exercise, you will find all the information on the exercise sheet.
There will be live-sessions in StudIP for every lecture and tutorial on the dates mentioned earlier. In these live-sessions, the students can ask questions and the solutions for the exercise sheets of the tutorial will be presented. We encourage active participation in these sessions. We are not allowed to record and upload the live-sessions afterwards!
| Day | Date | Type | Topic |
|---|---|---|---|
| Friday | 23.10.20 | 1. Lecture | Introduction |
| Donnerstag | 29.10.20 | 1. Exercise | Introduction |
| Friday | 30.10.20 | 2. Lecture | Design-by-Contract mit JML |
| Thursday | 05.11.20 | 2. Exercise | Design-by-Contract mit JML |
| Friday | 06.11.20 | 3. Lecture | Advanced Specification with JML |
| Thursday | 12.11.20 | 3. Exercise | Advanced Specification with JML |
| Friday | 13.11.20 | 4. Lecture | Testing with JML |
| Thursday | 19.11.20 | 4. Exercise | Testing with JML |
| Friday | 20.11.20 | 5. Lecture | Software Model Checking with JPF |
| Thursday | 26.11.20 | 5. Exercise | Software Model Checking with JPF |
| Friday | 27.11.20 | 6. Lecture | First-Order Logic |
| Thursday | 03.12.20 | 6. Exercise | First-Order Logic |
| Friday | 04.12.20 | 7. Lecture | Sequent Calculus |
| Thursday | 10.12.20 | 7. Exercise | Sequent Calculus |
| Friday | 11.12.20 | 8. Lecture | Dynamic Logic |
| Thursday | 17.12.20 | 8. Exercise | Dynamic Logic |
| Friday | 15.01.21 | 9. Lecture | Deductive Verification with KeY |
| Thursday | 21.01.21 | 9. Exercise | Deductive Verification with KeY |
| Friday | 22.01.21 | 10. Lecture | Loops, Method Calls, and Inheritance |
| Thursday | 28.01.21 | 10. Exercise | Loops, Method Calls, and Inheritance |
| Friday | 29.01.21 | 11. Lecture | Correctness-by-Construction |
| Thursday | 04.02.21 | 11. Exercise | Correctness-by-Construction |
| Thursday | 11.02.21 | 12. Exercise | Experiment: Correctness-by-Construction |
| Friday | 12.02.21 | 12. Lecture | Zusammenfassung |