Semantics and Verification of Software, Summer Term 2007
Type | Time | Place | Start | Lecturer |
V2 | Tue 11:45--13:15 | AH III | 10. April 2007 | |
V2 | Fri 08:15--09:45 | AH II | 13. April 2007 | |
Ü2 | Wed 13:30--15:00 | AH III | 18. April 2007 | Willems |
News
- You can pick up your exercise solutions at the office (room 4213).
- The evaluation reports for the course and the exercise class are available.
- The exercise course on 4 June is canceled.
- Exercises should be worked on in groups of three and have to be handed in before the exercise lesson on wednesday.
- The exercise course will start 18 April instead of 11 April as announced at first.
Contents
In order to guarantee the correctness and reliability of software systems, testing is not sufficient. Instead, a formal verification of programs is required. The goal of this course is to provide an introduction to the field of formal software verification.
The following topics will be covered:
- The imperative model language WHILE
- Operational, denotational and axiomatic semantics of WHILE and their equivalence
- Dataflow analysis
Slides
No. | Date | Topic | Overlays | Handout |
1 | 10.04.2007 | Introduction | ||
2 | 13.04.2007 | Operational Semantics I (Evaluation of Expressions) | ||
3 | 17.04.2007 | Operational Semantics II (Execution of Statements) | ||
4 | 20.04.2007 | Operational and Denotational Semantics | ||
5 | 24.04.2007 | Basic Fixpoint Theory I (Partial Orders) | ||
6 | 27.04.2007 | Basic Fixpoint Theory II (Continuous Functions) | ||
7 | 04.05.2007 | Denotational Semantics | ||
8 | 11.05.2007 | Axiomatic Semantics I (Partial Correctness Properties) | ||
9 | 15.05.2007 | Axiomatic Semantics II (Hoare Logic) | ||
10 | 18.05.2007 | Axiomatic Semantics III (Soundness & Completeness) | ||
11 | 22.05.2007 | Axiomatic Semantics IV (Equivalence & Total Correctness) | ||
12 | 25.05.2007 | Blocks and Procedures I (Operational Semantics) | ||
13 | 05.06.2007 | Blocks and Procedures II (Denotational Semantics) | ||
14 | 08.06.2007 | Dataflow Analysis I (Introduction) | ||
15 | 12.06.2007 | Dataflow Analysis II (Available Expressions & Live Variables) | ||
16 | 15.06.2007 | Dataflow Analysis III (The Framework) | ||
17 | 19.06.2007 | Dataflow Analysis IV (Equation Solving) | ||
18 | 22.06.2007 | Dataflow Analysis V (Worklist Algorithm) | ||
19 | 26.06.2007 | Dataflow Analysis VI (MOP Solution) | ||
20 | 29.06.2007 | Dataflow Analysis VII (MOP vs. Fixpoint Solution) | ||
21 | 03.07.2007 | Dataflow Analysis VIII (Interprocedural MVP Solution) | ||
22 | 06.07.2007 | Dataflow Analysis VIIII (Interprocedural Fixpoint Solution) | ||
23 | 10.07.2007 | Wrap-Up |
Exercise sheets
Language
The lecture will be given in German or English, depending on the audience.
Literature
- Glynn Winskel: The Formal Semantics of Programming Languages, The MIT Press, 1996
- Flemming Nielson, Hanne R. Nielson, Chris Hankin: Principles of Program Analysis, 2nd ed., Springer, 2005
- Daniel Jackson: Software Abstractions: Logic, Language, and Analysis, The MIT Press, 2006
Prerequisites
Basic knowledge in the following areas is expected:
- Essential concepts of imperative and object-oriented programming languages
- Formal languages and automata theory
- Mathematical logic
