Formal Methods in Software Development (WS 2022/23)
Abschnittsübersicht
-
326.013, Friday 8:30-11:00, Room: S2 053, Start: October 7, 2022
To take part in the course, you have to enrol in the KUSSS system. This course is offered simultaneously for the master program "Computer Science" and for the master program "Computer Mathematics".
This course 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 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 7: introduction and organization, the language of logic.
- October 14: the RISC Algorithm Language, specifying and verifying (part 1).
- October 21: specifying and verifying (part 1).
- October 28: specifying and verifying (part 1).
- November 4: the art of proving, the RISC ProofNavigator.
- November 11: specifying and verifying (part 2), the RISC ProgramExplorer.
- November 18: the Java Modeling Language (part 1).
- November 25: the extended static checking of Java programs with ESC/Java2.
- December 2: verifying Java programs with KeY.
- December 9: The Java Modeling Language (part 2),
- December 16: modeling concurrent systems.
- January 13: specifying in temporal logic.
- January 20: the Spin model checker, automatic model checking.
- January 27: automatic model checking, verifying safety properties by proving.
- October 7: introduction and organization, the language of logic.
-
Chapter 8: Computer Programs (teaser pages only)
- 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)
- Demonstration Examples
- Logic, Checking, and Proving (4 on 1)
- Specifying and Verifying Sequential Programs
- Specifying and Verifying Programs: Part 1 (4 on 1)
- Assigning Meaning to Programs (restricted)
- An Axiomatic Basis for Computer Programming (restricted)
- summation.txt, linsearch2.txt, linsearch3.zip
- Specifying and Verifying Programs: Part 2 (4 on 1)
- 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)
- 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)
- Specifying and Verifying Concurrent Systems
The password to this area is handed out in class.
-
The following software is used in this course (how to use the software):
- RISC Algorithm Language
- RISC ProofNavigator
- RISC ProgramExplorer
- Java Modeling Language (JML) tools
- Use the stable release 5.5 from the archive (not the newer release candidates); also note that the JML tools need an installation of Java 1.4.2.
- Local copy
- Documentation
- OpenJML
- Extended Static Checking for Java (ESC/Java 2)
- 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.
- 2nd Exam: Thursday, March 30, 2023, 17:15-18:45, S2 044
- Registration in KUSSS is required till Monday, March 27, 12:00.
- The exam is open book: all written (non-electronic) materials are allowed.
- Registration in KUSSS is required till Monday, March 27, 12:00.
- 2nd Exam: Thursday, March 30, 2023, 17:15-18:45, S2 044