News
- 08.07.2010: The evaluation results of the lectures and exercise classes are available.
- 20.05.2010: Master students have to register by May 28 for the exam (see below).
- 23.04.2010: Starting in week 18, the Wednesday lecture (10:00 at AH 6) will be moved to Friday (13:45 at AH 1).
- 20.04.2010: In week 17, exercise class and Friday lecture will be switched (see below)
- 11.03.2010: We are online!
Schedule
Type | Day | Time | Place | Start | Lecturer |
V4 | Thu | 15:00-16:30 | AH 5 | April 15 | |
Fri | 13:45-15:15 | AH 1 | May 7 | ||
Ü2 | Mo | 10:00-11:30 | AH 2 | Apr. 26 |
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
- Dataflow analysis
- Extensions: procedures and dynamic data structures
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 | April 15 | Introduction |  | |
2 | April 21 | Operational Semantics of WHILE I
(Evaluation of Expressions) | | |
3 | April 22 | Operational Semantics of WHILE II
(Execution of Statements) | | |
4 | April 26 | Operational Semantics of WHILE III
(Properties of Execution Relation) | | |
5 | April 29 | Operational/Denotational Semantics of WHILE | | |
6 | May 6 | Denotational Semantics of WHILE I
(Fixpoint Semantics of WHILE Loop) | | |
7 | May 7 | Denotational Semantics of WHILE II
(Chain-Complete Partial Orders) | | |
8 | May 14 | Denotational Semantics of WHILE III
(Continuous Functions and Fixpoint Theorem) | | |
9 | May 20 | Equivalence of Operational and Denotational Semantics | | |
10 | May 21 | Axiomatic Semantics of WHILE I
(Introduction) | | |
11 | June 4 | Axiomatic Semantics of WHILE II
(Hoare Logic) | | |
12 | June 10 | Axiomatic Semantics of WHILE III
(Correctness of Hoare Logic) | | |
13 | June 11
(AH 3) | Axiomatic Semantics of WHILE IV
(Relative Completeness and Total Correctness Properties) | | |
14 | June 17 | Axiomatic Semantics of WHILE V
(Total Correctness and Semantic Equivalence) | | |
15 | June 24 | Semantics of Blocks and Procedures | | |
16 | June 25 | Provably Correct Implementation I
(Abstract Machine & Compiler) | | |
17 | July 1 | Provably Correct Implementation II
(Correctness of Compiler) | | |
18 | July 2 | Dataflow Analysis I
(Introduction & Available Expressions Analysis) | | |
19 | July 8 | Dataflow Analysis II
(Live Variables Analysis) | | |
20 | July 15 | Dataflow Analysis III
(The Framework) | | |
21 | July 16 | Dataflow Analysis IV
(Solving Dataflow Equation Systems) | | |
22 | July 22 | Dataflow Analysis V
(The MOP Solution) | | |
23 | July 23 | Dataflow Analysis VI
(MOP vs. Fixpoint Solution & Wrap-Up) | | |
Exercises
Exercise sheets will be made available on Mondays. The deadline for handing in your solution is on Mondays, before
No. | Online | Hand in | Exercise Sheet | Solution |
|---|---|---|---|---|
1 | April 19 | April 30 | Friday, April 30th | |
2 | April 26 | May 3 | Monday, May 3rd | |
3 | May 3 | May 10 | Monday, May 10th | |
4 | May 10 | May 17 | Exercise 4 updated! | Monday, May 17th |
5 | May 17 | May 31 | Monday, May 31st | |
6 | May 31 | June 7 | Monday, June 7th | |
7 | June 7 | June 14 | Monday, June 14th | |
8 | June 14 | June 21 | Monday, June 21st | |
9 | June 21 | June 28 | Monday, June 28th | |
10 | June 28 | July 5 | Monday, July 5th | |
11 | July 5 | July 12 | Exercise 11 updated! | Monday, July 12th |
12 | July 12 | July 19 | Monday, July 19th | |
13 | July 19 | July 26 (optional) | Exercise 13 (optional) |
Exam
The exam will be organized in oral form. Dates are scheduled by appointment with Dr. Noll (preferably via e-mail), either in the second half of July or between beginning of September and mid-October. 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 by May 28 via the CampusOffice registration procedure on the corresponding Campus web page.
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
- Flemming Nielson, Hanne R. Nielson, Chris Hankin: Principles of Program Analysis, 2nd ed., Springer, 2005
