News

  • 30.01.09 - The evaluation results for the lectures and the exercises are available.
  • 04.11.08 - We have decided to put the solutions online. Feel free to use them.
  • 29.10.08 - Now! every exercise contains the number of points. The golden rule: you need to accumulate >= 50% of the total number of points in order to be eligible for the SVS exam.
  • 29.10.08 - There is no lecture on 30.10.08
  • 29.10.08 - The time of the exercise class remains the same. The solutions of the exercises will not be published online.


Schedule

Type

Day

Time

Place

Start

Lecturer

V4

Mon

11:45-13:15

AH 2

Oct. 20

Noll

Thu

13:30-15:00

AH 1

Oct. 16

Noll

Ü2

Mon

13:30-15:00

AH 2

Oct. 27

Mereacre / Han


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 software verificatio

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. Dataflow analysis
  7. 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

Oct. 16

Introduction

Here

Here

2

Oct. 20

Operational Semantics of WHILE I

(Evaluation of Expressions)

Here

Here

3

Oct. 23

Operational Semantics of WHILE II

(Execution of Statements)

Here

Here

4

Oct. 27

Operational and Denotational Semantics

Here

Here

5

Nov. 3

Denotational Semantics of WHILE I

(Fixpoint Semantics of WHILE Loop)

Here

Here

6

Nov. 6

Denotational Semantics of WHILE II

(Chain-Complete Partial Orders)

Here

Here

7

Nov. 10

Denotational Semantics of WHILE III

(Continuous Functions and Fixpoint Theorem)

Here

Here

8

Nov. 13

Operational/Denotational/Axiomatic Semantics of WHILE

Here

Here

9

Nov. 17

Axiomatic Semantics of WHILE I

(Hoare Logic)

Here

Here

10

Nov. 20

Axiomatic Semantics of WHILE II

(Soundness of Hoare Logic)

Here

Here

11

Nov. 24

Axiomatic Semantics of WHILE III

(Completeness and Equivalence)

Here

Here

12

Dec. 1

Axiomatic Semantics of WHILE IV

(Total Correctness)

Here

Here

13

Dec. 4

Semantics of Blocks and Procedures

Here

Here

14

Dec. 8

Dataflow Analysis I (Introduction)

Here

Here

15

Dec. 11

Dataflow Analysis II

(Available Expressions & Live Variables)

Here

Here

16

Dec. 15

Dataflow Analysis III (The Framework)

Here

Here

17

Dec. 18

Dataflow Analysis IV (Equation Solving)

Here

Here

18

Jan. 5

Dataflow Analysis V

(Efficient Fixpoint Computation)

Here

Here

19

Jan. 8

Dataflow Analysis VI (MOP Solution)

Here

Here

20

Jan. 12

Dataflow Analysis VII (MOP vs. Fixpoint Solution)

Here

Here

21

Jan. 15

Dataflow Analysis VIII

(Interprocedural MVP Solution)

Here

Here

22

Jan. 19

Dataflow Analysis IX

(Interprocedural Fixpoint Solution)

Here

Here

23

Jan. 22

Dataflow Analysis X

(Interprocedural Fixpoint Solution & Wrap-Up)

Here

Here

24

Jan. 26

Provably Correct Implementation I

(Abstract Machine & Compiler)

Here

Here

25

Jan. 29

Provably Correct Implementation II

(Compiler Correctness)

 

Here

Here

26

Feb. 2

Wrap-Up

Here

Here


Literature