Formal Methods in Software Development (WS 2023/24)
Section outline
-
326.013, Friday 8:30-11:00, Room: S2 053 (November 24: HS 2), Start: October 6, 2023
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 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 6: introduction and organization, the language of logic.
- October 13: the RISC Algorithm Language, specifying and verifying (part 1).
- October 20: specifying and verifying (part 1).
- October 27: specifying and verifying (part 1).
- November 3: the art of proving, the RISC ProofNavigator.
- November 10: specifying and verifying (part 2), the RISC ProgramExplorer.
- November 17: the Java Modeling Language (part 1).
- November 24: the extended static checking of Java programs with ESC/Java2.
- December 1: verifying Java programs with KeY.
- December 15: the Java Modeling Language (part 2).
- January 12: modeling concurrent systems, specifying in temporal logic.
- January 19: specifying in temporal logic, the Spin model checker.
- January 26: automatic model checking, proving system invariants.
- October 6: introduction and organization, the language of logic.
-
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)
- 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 (not any more available from original site)
- Local copy (works with Java 5)
- Documentation
- OpenJML (use V0.8.59, not the newer alpha versions, works with Java 8)
- Extended Static Checking for Java (ESC/Java 2) (not any more available from original site)
- Local copy (works with Java 5)
- Documentation
- 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).
-
-
-
-
-
-
-
-
-
Extra Assignment (March 11)Due: Monday, 11 March 2024, 11:59 PM
-
-
The final exam must be passed positively; it accounts for 50% of the course grade.
- 2nd Exam: Wednesday, March 20, 2024, 17:15-18:45, MT 127
- Registration in KUSSS is required till Monday, March 18, 2024, 12:00.
- The exam is open book: all written/printed (non-electronic) materials are allowed.
- 2nd Exam: Wednesday, March 20, 2024, 17:15-18:45, MT 127
