Formal Methods in Software Development (WS 2024/25)
Section outline
-
326.013, Friday 8:30-11:00, Start: October 4, 2024, MT 226
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 4: introduction and organization, the language of logic.
- October 11: the RISC Algorithm Language, specifying and verifying.
- October 18: specifying and verifying.
- October 25: specifying and verifying.
- November 8: the art of proving, the RISC Theorem Proving Interface.
- November 15: specifying and verifying.
- November 22: the Java Modeling Language (part 1).
- November 29: extended static checking of Java programs with ESC/Java2.
- December 6: verifying Java programs with KeY.
- December 13: the Java Modeling Language (part 2).
- December 20: modeling concurrent systems.
- January 10: specifying in temporal logic, verifying safety properties.
- January 17: the Spin model checker, automatic model checking.
- January 24: (no lecture)
- January 31: 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 31, 2025, 8:30-10:00, HS 18
- If you submitted the assignments in the current semester, no registration is needed (otherwise, send me an email 1-2 weeks before the exam).
- The exam is open book: all written/printed (non-electronic) materials are allowed.
- There will be another exam at the end of March 2025.
- If you submitted the assignments in the current semester, no registration is needed (otherwise, send me an email 1-2 weeks before the exam).
- Exam: Friday, January 31, 2025, 8:30-10:00, HS 18
