Semantics and Verification of Software

News

  • 2018-01-16: Assignment of slots for the oral exam is handled via this foodle poll. Please register (for as many slots as possible) by beginning of February.
  • 2018-01-31: There will be no sample solution for exercise 10.
  • 2017-12-18: During the first lectures candidates have been informed that admission to the exam requires a certain percentage of points to be obtained in the exercises. However, this requirement is not fixed in the corresponding module specification and thus invalid. For this reason, every registered participant is automatically admitted. Therefore, if people are not intending to attend the exam they should de-register via Campus Office in order to avoid a “not passed” due to not showing up. Although the exercises are no longer mandatory for the exam admission, we will continue to correct them and discuss them in the exercise classes. We firmly believe that actively solving the exercises is truly important so as to pass the exam.
  • 2017-12-05: There is, unfortunately, a typo in exercise sheet 6, task 3b. Of course you should define the strongst postcondition instead of the strongest precondition.
  • 2017-10-26: Due to a public holiday there will be no exercise class on November 1st. The deadline for the second exercise sheet has been extended accordingly to November 8th.
  • 2017-09-15: we are online!

Schedule

Type Day Time Hall Start Lecturer
Lecture Tue 10:15 – 11:45 9U10 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

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 10 Oct Introduction l1 l1    
2 12 Oct Operational Semantics of WHILE I (Evaluation of Expressions) l2 l2    
3 19 Oct Operational Semantics of WHILE II (Execution of Statements) l3 l3 ex-01   sol01
4 24 Oct Operational Semantics of WHILE III (Summary & Application to Compiler Correctness) l4  l4    
5 26 Oct Operational Semantics of WHILE IV (The Compiler & Its Correctness)  l5 l5 ex-02   sol02
6 07 Nov Denotational Semantics of WHILE I (The Approach)  l6 l6 ex-03 sol03 
7 14 Nov Denotational Semantics of WHILE II (Fixpoint Theory)  l7 l7    
8 16 Nov Denotational Semantics of WHILE III (Fixpoint & Coincidence Theorem)  l8  l8 ex-04  sol04 
9 21 Nov Axiomatic Semantics of WHILE I (Hoare Logic) l9  l9    
10 23 Nov Axiomatic Semantics of WHILE II (Soundness & Completeness) l10 l10 ex-05 sol05 
11 28 Nov Axiomatic Semantics of WHILE III (Total Correctness & Axiomatic Equivalence) l11 l11    
12 30 Nov Axiomatic Semantics of WHILE IV (Axiomatic Equivalence & Timed Correctness Properties) l12 l12  ex-06  sol06 
13 05 Dec Axiomatic Semantics of WHILE V (Proving Timed Correctness) l13 l13    
14 07 Dec Extension by Blocks and Procedures I (Operational Semantics) l14 l14 ex-07  sol07 
15 12 Dec Extension by Blocks and Procedures II (Denotational Semantics) l15 l15 ex-08   
16 14 Dec Nondeterminism and Parallelism I (Shared-Variables Communication) l16 l16 ex-09  sol09
17 19 Dec Nondeterminism and Parallelism II (Channel Communication) l17 l17    
18 09 Jan Fairness in CSP & Type Systems l18 l18 ex-10   
19 11 Jan Security Type Systems l19 l19    
20 16 Jan Wrap-Up l20 l20    

Exam

  • There will be an oral exam. Please use this foodle poll by beginning of February for getting a date assigned (and choose as many slots as possible).
  • Registration was possible via this web page.
  • Admission requires to achieve 50% of the points in the exercises.

Evaluation results

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