(The lecture will be given in English)

- Lecturer: Dr. Holger Gast, Exercises: Lars Noschinski
- 2 lecture and 2 tutorial hours per week
- 5 ECTS
- Times: Lecture Tue, 8:30-9:55; Exercises: Wed, 8:30-9:55 (in 01.09.014)
- Module: IN3350
- Introduction to the theorem prover Isabelle
- Semantics of a C-like imperative language SimplC
- Simpl: language, semantics, Hoare logic
- Embedding SimplC to Simpl
- Heap-manipulating programs: Burstall's memory model
- Symbolic execution in separation logic
- Introduction and Motivation (with Demo01.thy)
- Basics of Isabelle (with Demo02.thy and BinTree.thy)
- Tail Recursion and More on Induction Demo03.thy
- Semantics of Simpl Demo05.thy
- Hoare Logic of Simpl Demo06.thy
- Emedding SimplC to Simpl and verification examples Demo07.thy
- Abstraction predicates and separation lemmas Demo08.thy
- Burstall's Heap Model Demo09.thy
- Heap Manipulations & Ghost State Demo10.thy
- Introduction to Separation Logic Demo11.thy
- Symbolic Execution in Separation Logic Demo12.thy
- Examples of Symbolic Execution Demo13.thy
- Exercise Sheet 1 (Theory Template, Solution)
- Exercise Sheet 2 (Theory Template, Solution)
- Exercise Sheet 3 (Theory Template, Solution)
- Exercise Sheet 4 (Theory Template, Solution UPDATED)
- SimplC.zip
- Exercise Sheet 5
- Exercise Sheet 6 (UPDATED VERSION, replaced
`j-i`

by`j-1`

in program 2) (Solution) - Exercise Sheet 7 (Theory Template, Solution)
- Exercise Sheet 8 UPDATED (Theory Template UPDATED, Solution)
- Exercise Sheet 9 (Theory Template, Solution)
- Exercise Sheet 10 (Theory Template, )

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.