(The lecture will be given in English)
The correctness of software is a key factor in many application domains: malfunctioning embedded systems may directly cause accidents and the operating system's reliability is crucial to the availability of any server software running on the system.
The lecture gives an overview of the concepts and techniques on which correctness proofs are founded. We use the interactive theorem prover Isabelle to explain and to demonstrate the reasoning steps in detail, and to verify typical example programs. The lab exercises offer hands-on experience with a down-sized, pedagogical verification environment for a C-like language within the Isabelle framework.
Beyond the formal techniques, the lecture seeks to highlight the connection to a practioner's perspective on the issue of "program correctness": a precise understanding of the specifications and invariants of code is in any case a prerequisite to produce reliable software, whether it will be formally verified or not.
The topics cover the different layers of argumentation. First, it is necessary to understand and to define in detail the meaning of the used programming language. We use an embedding (a translation) of a C-dialect SimplC to Schirmer's Simpl language. Next, a Hoare logic (for Simpl) generates verification conditions whose proof establishes the program's correctness. Finally, we verify typical examples to demonstrate the reasoning strategies and -patterns involved. Since heap-manipulating programs pose particular challenges, they receive broader attention, based on the classical Burstall (components-as-arrays) memory model and on recent developments in separation logic.
The lecture on Tue, 14.5. is cancelled due to
the Studentische Vollversammlung.
Accordingly,
the exercises on Wed, 15.5. will not take place.
j-i by j-1 in program 2)
(Solution)