News
- 21.12.2011: Evaluation results are online
- 18.11.2011: Updated (corrected) exercise sheet!
- 09.11.2011: Due to the "Fachschaftsvollversammlung" the exercise class presenting the solution of exercise 2 will take place at the lecture date and location (10:00 - 11:30 a.m. in AH 2). Therefore you can hand in your solution for Exercise 1 until Wednesday, before 10 o'clock!
- 17.10.2011: There will be no exercise class on Tuesday, October 18th. The first exercise class will take place on Tuesday, October 25th.
- 22.09.2011: We are online!
Schedule
Type | Day | Time | Place | Start | Lecturer |
V3 | Wed | 10:00-11:30 | AH 2 | Oct 12 | |
Thu | 13:30-15:00 | AH 1 | Oct 13 | ||
Ü2 | Tue | 11:45-13:15 | AH 6 | Oct 25 |
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:
- The imperative model language WHILE
- Operational semantics of WHILE
- Denotational semantics of WHILE
- Equivalence of operational and denotational semantics
- Axiomatic semantics of WHILE
- Extensions: procedures and dynamic data structures
- Compiler correctness
Prerequisites
Basic knowledge in the following areas is expected:
- Essential concepts of imperative programming languages
- Formal languages and automata theory
- Mathematical logic
Lectures
No. | Date | Topic | Overlays | Handout |
|---|---|---|---|---|
1 | Oct 12 | Introduction |  |  |
2 | Oct 13 | Operational Semantics of WHILE I
(Evaluation of Expressions) | | |
3 | Oct 26 | Operational Semantics of WHILE II
(Execution of Statements) | | |
4 | Nov 10 | Operational Semantics of WHILE III
(Properties of Execution Relation) | | |
5 | Nov 16 | Denotational Semantics of WHILE I
(Fixpoint Semantics) | | |
6 | Nov 17 | Denotational Semantics of WHILE II
(Chain-Complete Partial Orders) | | |
7 | Nov 23 | Denotational Semantics of WHILE III
(Continuous Functions and Fixpoint Theorem) | | |
8 | Nov 24 | Denotational Semantics of WHILE IV
(Equivalence with Operational Semantics) | | |
9 | Nov 30 | Axiomatic Semantics of WHILE I
(Introduction) | | |
10 | Dec 7 | Axiomatic Semantics of WHILE II
(Hoare Logic) | | |
11 | Dec 8 | Axiomatic Semantics of WHILE III
(Correctness of Hoare Logic) | | |
12 | Dec 14 | Axiomatic Semantics of WHILE IV
(Total Correctness Properties) | | |
13 | Dec 15 | Axiomatic Semantics of WHILE V
(Semantic Equivalence) | | |
14 | Dec 21 | Extension by Blocks and Procedures I
(Operational Semantics) | | |
15 | Jan 11 | Extension by Blocks and Procedures II
(Denotational Semantics) | | |
16 | Jan 18 | Provably Correct Implementation I
(Abstract Machine) | | |
17 | Jan 19 | Provably Correct Implementation II
(Compiler & Its Correctness) | | |
18 | Jan 25 | Nondeterminism and Parallelism I (Shared-Variables and Channel Communication) | | |
19 | Jan 26 | Nondeterminism and Parallelism II
(Communicating Sequential Processes) | | |
20 | Feb 1 | Nondeterminism and Parallelism III
(Calculus of Communicating Systems) | | |
21 | Feb 2 | Nondeterminism and Parallelism IV
(Equivalence of CCS Processes) | | |
Exercises
The exercise sheets will be available on Tuesdays. Please hand your solution in before the beginning of the exercise classes, i.e. on tuesday before 11:45 am.
Examination admission requires at least 50 % of the points in the exercises.
- Exercise 0 (hand in until October, 25th)
- Exercise 1 (hand in until November, 8th)
- Exercise 2 (hand in until November, 15th)
- Exercise 3 (hand in until November, 22nd)
- Exercise 4 (hand in until November, 29nd)
- Exercise 5( hand in until December, 6th)
- Exercise 6 (hand in until December, 13th)
- Exercise 7 (hand in until December, 20th)
- Exercise 8 (hand in until January, 10th) Solution: Ex. 4
- Exercise 9 (hand in until January, 17th)
- Exercise 10 (hand in until January, 24th)
- Exercise 11 (hand in until January, 31st) Solution: Ex. 2 + 3
Exam
The exam will be organized in oral form. Dates are scheduled by appointment with Dr. Noll (preferably via e-mail), between February and April. Regarding registration, the following rules apply:
- Students enrolled in Diplomstudiengang Informatik have to register via (V)ZPA.
- Students enrolled in Masterstudiengang Informatik have to register via the CampusOffice registration procedure on the corresponding Campus web page.
Evaluation results
- Lecture
- w.r.t. lectures
- w.r.t. instructor
- Exercises
- w.r.t. exercises
- w.r.t. instructors
Literature
- Glynn Winskel: The Formal Semantics of Programming Languages, The MIT Press, 1996
- Hanne R. Nielson, Flemming Nielson: Semantics with Applications: A Formal Introduction, Wiley, 1992
