Semantics and Verification of Software

Master course in Winter 2024/25

Schedule

TypeDayTimeRoomStartLecturer
LectureMon12:30-14:00AH 27 OctNoll
 Tue12:30-14:00AH 28 OctNoll
ExerciseThu16:30-18:00AH 324 OctAhrens, Haase

Detailed information is available through the associated RWTHmoodle classroom.

Contents

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, pointers (separation logic), …

Prerequisites

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

Background Literature