Formale Methoden der Softwareentwicklung
Time and Place
| Mi | 14:15 – 15:45 (Lecture) | 00.131-128 |
| Fr | 16:15 – 17:45 (Tutorials) | 01.255-128 |
The first meeting is on Wednesday, November 4th. For now, all meetings (lectures and tutorials) will be conducted online. Please subscribe to the StudOn course (see below).
A general description
In the first part of the course, we will engage in the formal verification of reactive systems. Students learn the syntax and semantics of the temporal logics LTL, CTL, and CTL* and their application in the specification of e.g. safety and liveness properties of systems. Simple models of systems are designed and verified using model checkers and dedicated frameworks for asynchronous and synchronous reactive systems, and the algorithms working in the background are explained.
The second part of the course focuses on functional correctness of programs; more precisely, we discuss the theory of pre- and postconditions, Hoare triples, loop invariants, and weakest (liberal) preconditions, in order to introduce automatised correctness proofs using the Hoare calculus.
Furthermore, unlike SemProg we focus on push-button tools rather than approaches based on proof assistants.
-
For the second part of the material we are planning to work with the functional programming language FStar.
Subscription, administration and more
Please subscribe via the StudOn course. We will use that course for all administrative tasks.
Please also fill in the poll about your preferred online meeting tools that you will find there.