Semantics and Verification of Software


  • 2017-09-15: we are online!


Type Day Time Hall Start Lecturer
Lecture Tue 10:15 – 11:45 AH 1 10 Oct Noll
  Thu 10:15 – 11:45 AH 6 12 Oct Noll
Exercise Wed 12:00 – 13:30 AH 3 25 Oct Kaminski/Matheja


The analysis and verification of software systems is an important issue. In particular, safety-critical systems are ones in which errors can be disastrous: loss of life, major financial losses, etc. Techniques to safeguard against such scenarios are essential for such systems. Testing can identify problems, especially if done in a rigorous fashion, but is generally not sufficient to guarantee a satisfactory level of quality. Formal methods, on the other hand, offer techniques ranging from the description of requirements in a formal notation to allow for rigorous reasoning about them, to techniques for automatic verification of software.
The goal of this course is to provide an introduction to the field of formal semantics for programming languages, with particular emphasis on software verification. The following topics will be covered:
  1. The imperative model language WHILE
  2. Operational semantics of WHILE
  3. Denotational semantics of WHILE
  4. Equivalence of operational and denotational semantics
  5. Axiomatic semantics of WHILE
  6. Compiler correctness
  7. Extensions: procedures, parallelism, …


Basic knowledge of the following relevant undergraduate courses is expected:
  • Programming (essential concepts of imperative and object-oriented programming languages and elementary programming techniques)
  • Formal Languages and Automata Theory (regular and context-free languages, finite and pushdown automata)
  • Mathematical Logic

Slides & Exercises

No. Date Subject Slides Handout Exercises Solutions
1 10 Oct Introduction        
2 12 Oct          
3 19 Oct          
4 24 Oct          
5 26 Oct          
6 07 Nov          
7 14 Nov          
8 16 Nov          
9 21 Nov          
10 23 Nov          
11 28 Nov          
12 30 Nov          
13 05 Dec          
14 07 Dec          
15 12 Dec          
16 14 Dec          
17 19 Dec          
18 21 Dec          
19 09 Jan          
20 11 Jan          
21 16 Jan          
22 18 Jan          


  • Depending on the number of participants, the exam will take place in written or oral form.

Further information

  • The lectures will be given in German or English, depending on the language proficiency of the audience.
  • The slides and other course material will be in English. There are no lecture notes (yet); the course material will consist of slides.

Background Literature