Semantics and Verification of Software

News

  • 2019-06-06: due to the CS Summer Party, the exercise class on June 7 is moved from room 5056 to the seminar room of i2
  • 2018-12-18: we are online!

Schedule (TBA)

Type Day Time Room Start Lecturer
Lecture Mon 14:30 – 16:00 AH 6 15 Apr Noll
Lecture Thu 10:30 – 12:00 5056 4 Apr Noll
Exercise Fri 10:30 – 12:00 5056 26 Apr Batz, Matheja

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, parallelism, …

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

Slides & Exercises

No. Date Topic Slides Handout Exercises Solutions
1 4 Apr Introduction l01 l01    
2 12 Apr, 5056 Operational Semantics of WHILE I (Evaluation of Expressions) l02 l02    
3 15 Apr Operational Semantics of WHILE II (Execution of Statements) l03 l03    
4 18 Apr Operational Semantics of WHILE III (Summary & Application to Compiler Correctness) l04 l04 ex-01  
5 25 Apr Operational Semantics of WHILE IV (The Compiler & Its Correctness) l05 l05 ex-02  
6 2 May Denotational Semantics of WHILE I (The Approach) l06 l06 ex-03  
7 6 May Denotational Semantics of WHILE II (Algebraic Foundations) l07 l07    
8 9 May Denotational Semantics of WHILE III (Fixpoint & Coincidence Theorem) l08 l08 ex-04  
9 20 May Axiomatic Semantics of WHILE I (Hoare Logic) l09 l09    
10 23 May Axiomatic Semantics of WHILE II (Soundness of Hoare Logic) l10 l10 ex-05  
11 27 May Axiomatic Semantics of WHILE III (Completeness & Total Correctness) l11 l11 ex-06  
12 3 Jun Axiomatic Semantics of WHILE IV (Total Correctness & Axiomatic Equivalence) l12 l12 ex-07  
13 6 Jun Axiomatic Semantics of WHILE V (Correctness Properties for Execution Time) l13 l13    
14 17 Jun Extension by Blocks and Procedures I (Operational Semantics) l14 l14 ex-08  
15 24 Jun Extension by Blocks and Procedures II (Denotational Semantics) l15 l15    
16 27 Jun Extension by Blocks and Procedures III (Axiomatic Semantics) l16 l16 ex-09  
17 1 Jul Separation Logic I (Introduction) l17 l17    
18 4 Jul Separation Logic II (Recursive Data Structures and Partial Correctness Properties) l18 l18 ex-10  
19 8 Jul Separation Logic III (Soundness) & Wrap-Up l19 l19    

Exam

  • There will be oral exams offered during the following two weeks:
    • Week 31 (July 29 – August 2)
    • Week 38 (September 16 – 20)
  • Registration is possible via RWTHonline until June 14, 2019.
  • Admission requires to achieve 50% of the points in the exercises.
  • Please register for a date via this Foodle poll.

Evaluation results

  • Lecture (TBA)
  • Exercises (TBA)

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