Formal Methods in Software Development (WS 2025/26)
Abschnittsübersicht
-
326.013, Friday 8:30-11:00, Start: October 10, 2025
This course is offered simultaneously for the master program "Computer Science" and for the master program "Computational Mathematics". It gives a survey on the use of formal methods for the development of reliable software. More specifically, we deal with
- specifying sequential programs and concurrent systems,
- computer-supported verification,
- extended static checking,
- model checking.
The course consists of two parts:
- a lecture part where the fundamental issues of the field are taught, and
- an exercise part where practical skills are trained using freely available software tools.
The grading of the course will be based on a couple of exercises and a final exam.
You have to create an account in this Moodle instance (using your students.jku.at email address) and self-register as a course participant (link "Enrol me in this course" at the top). You are then able to submit your assignments; furthermore, you receive per email all messages posted in the "Announcements" forum and may yourself post messages in the "Questions and Answers" forum.
-
As an extra service, it is intended to live-stream and record the course via the following Zoom session:https://jku.zoom.us/j/93538736451?pwd=OTdnTVNXOVJhcURDMmd4bG1DQTVRQT09
Meeting ID: 935 3873 6451 Password: formalHowever, no guarantee is given with respect to completeness and quality of the stream/recordings. The basic course format is on-site, not hybrid. -
The following is a preliminary schedule of the lecture:
- October 10: introduction and organization, the language of logic.
- October 17: the RISC Algorithm Language, specifying and verifying.
- October 24: specifying and verifying.
- October 31: specifying and verifying.
- November 7: the art of proving, the RISC Theorem Proving Interface.
- November 14: specifying and verifying.
- November 21: the Java Modeling Language (part 1).
- November 28: extended static checking of Java programs with ESC/Java2.
- December 5: verifying Java programs with KeY.
- December 12: the Java Modeling Language (part 2).
- December 19: modeling concurrent systems.
- January 9: specifying in temporal logic, verifying safety properties.
- January 16: the Spin model checker, automatic model checking.
- January 23: (no lecture)
- January 30: exam
-
Exercises and Software RISCAL Software and Models - Computer Programs/Systems as Subject of Formal Reasoning
- Introduction (4 on 1)
- Fehler im System: der Traum von Software ohne Bugs (restricted)
- Retrospective: Hoare: An Axiomatic Basis for Computer Programming (restricted)
- Formal Methods: Practice and Experience (local copy)
- Formally Verified Software in the Real World (restricted)
- Formal Methods in Dependable Systems Engineering (local copy)
- The Development and Deployment of Formal Methods in the UK (local copy)
- A manifesto for applicable formal methods (local copy)
- Demonstration Examples
- Logic, Checking, and Proving (4 on 1)
- Introduction (4 on 1)
- Specifying and Verifying Sequential Programs
- Specifying and Verifying Java Programs
- The Java Modeling Language: Part 1 (4 on 1)
- Behavioral Interface Specification Languages (restricted)
- Specification and Verification: The Spec# Experience (restricted)
- The Frama-C Software Analysis Platform (restricted)
- Demonstration Examples
- Extended Static Checking with ESC/Java 2 (4 on 1)
- Verifying Java Programs with KeY (4 on 1)
- The Java Modeling Language: Part 2 (4 on 1)
- The Java Modeling Language: Part 1 (4 on 1)
- Specifying and Verifying Concurrent Systems
The password to this area is handed out by a forum message.
- Computer Programs/Systems as Subject of Formal Reasoning
-
The following software is used in this course (how to use the software):
- RISC Algorithm Language (RISCAL)
- RISC Theorem Proving Interface (RISCTP)
- Java Modeling Language (JML) (original tools not any more available)
- Local copy of original tools (works with Java 5)
- OpenJML (latest release V0.8.59 works with Java 8, there is also an alpha release V0.21.0 for Java 21)
- Extended Static Checking for Java (ESC/Java 2)
- Local copy (works with Java 5)
- KeY Verification Environment
- Tutorial (local copy), More Tutorials and Examples
- Spin Model Checker
-
8 exercises are handed out. From these, the best 7 are used for grading (in total 350 points have to be earned).
-
-
The final exam must be passed positively; it accounts for 50% of the course grade.
- Exam: Friday, January 30, 2026, 8:30-10:00
- No registration is needed if the assignments have been submitted in the current semester (otherwise send me an email 1-2 weeks before the exam).
- The exam is open book: all written/printed (non-electronic) materials are allowed.
- No registration is needed if the assignments have been submitted in the current semester (otherwise send me an email 1-2 weeks before the exam).
- Exam: Friday, January 30, 2026, 8:30-10:00
