Semantics and Verification of Software

News

  • 2015-06-30: exam dates are scheduled
  • 2015-06-16: due to the RWTH Sports Day there will be no exercise class on June 24th
  • 2015-04-09: to avoid a time clash, the Thursday lecture is shifted from 11:15 to 11:45
  • 2015-02-19: we are online!

Schedule

Type Day Time Hall Start Lecturer
Lecture Tue 14:15 – 15:45 AH 2 14 Apr Noll
Thu 11:45 – 13:15 AH 2 9 Apr Noll
Exercise Wed 15:00 – 16:30 AH 6 22 Apr Matheja/Olmedo

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 Subject Slides Handout Exercises Solutions
1 9 Apr Introduction l1 l1
2 14 Apr Operational Semantics of WHILE I
(Evaluation of Expressions)		 l2 l2 e1
3 16 Apr Operational Semantics of WHILE II
(Execution of Statements)		 l3 l3
4 21 Apr Operational Semantics of WHILE III
(Summary & Application to Compiler Correctness)		 l4 l4 e2 s2
5 23 Apr Operational Semantics of WHILE IV
(The Compiler & Its Correctness)		 l5 l5
6 28 Apr Denotational Semantics of WHILE I
(The Approach)		 l6 l6 e3 s3
7 30 Apr Denotational Semantics of WHILE II
(CCPOs and Continuous Functions)		 l7 l7
8 05 May Denotational Semantics of WHILE III
(Fixpoint & Coincidence Theorem)		 l8 l8 e4 s4
9 07 May Axiomatic Semantics of WHILE I
(Hoare Logic)		 l9 l9
10 12 May Axiomatic Semantics of WHILE II
(Soundness & Completeness)		 l10 l10 e5 s5
11 19 May Axiomatic Semantics of WHILE III
(Total Correctness)		 l11 l11 e6 s6
12 21 May Axiomatic Semantics of WHILE IV
(Axiomatic Equivalence)		 l12 l12
13 02 Jun Extension by Blocks and Procedures I
(Operational Semantics)		 l13 l13 e7 s7
14 11 Jun Extension by Blocks and Procedures II
(Denotational Semantics)		 l14 l14 e8 s8
15 16 Jun Nondeterminism and Parallelism I
(Shared-Variables Communication)		 l15 l15
16 18 Jun Nondeterminism and Parallelism II
(Channel Communication)		 l16 l16 e9 s9
17 25 Jun Axiomatic Semantics of WHILE V
(Correctness Properties for Execution Time)		 l17 l17
18 30 Jun Axiomatic Semantics of WHILE VI
(Proving Timed Correctness)		 l18 l18 e10 s10
19 07 Jul Wrap-Up l19 l19

Exam

  • The exam will take place in oral form.
  • The following dates are offered:
    • Thu 23 July
    • Wed 26 August
    • Thu 24 September
  • Participants should indicate their date(s) of preference by 20 July via this foodle poll.
  • Previous registration is necessary via this Campus page.
  • Students who intend to take an advanced master exam (“vorgezogene Masterprüfung”) need to register in person at ZPA in the beginning of July. More information is available here.
  • Exams take place in Thomas Noll’s office (E1, 2nd floor, room 4211) according to the following schedule:
    Date Time Student
    Thu 23 July 10:00-10:30 Jan-Erik Rediger
    10:30-11:00 Frederick Prinz
    11:00-11:30 Thomas Mertens
    Wed 26 August 09:00-09:30 Houman Biglari
    09:30-10:00 Yannick Deuster
    10:00-10:30 –
    10:30-11:00 Christopher Spinrath
    11:00-11:30 Manuel Krebber
    Tue 8 September 10:00-10:30 Tobias Schürg
    Thu 17 September 14:00-14:30 Frank Emrich
    Thu 24 September 10:00-10:30 Kevin Jahns
    10:30-11:00 Thomas Henn

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