326.506-Formal Specification and Verification

Lecturer: Dr. Heinrich Rolletschek

Time and place: Wednesday, 12:00-13:30, T 857.

Contents: Informally, we say that a program P is correct, if it solves the problem it is supposed to solve for any given input. Such an assertion can be given in a rigorous form by a specification of the form {p} P {q}, were p and q are formulas; it means: if p holds before the execution of P, then q holds afterwards. This course deals with the problem of program verification, that is, how to prove correctness in a rigorous fashion.

Literature: Lecture notes will be given out.

Distributed so far:

• Introduction and chapter 1 (originally pp. 1-20)
• Corrected pages 15-21 (replace original pages 15-20)
• Chapter 2 (pp. 23-32)
• Chapter 3 (pp. 33-43)
• Chapter 4, sections 4.1-4.3 (pp. 45-58)
• Rest of Chapter 4 (section 4.4, pp. 59-65)
• Chapter 5, sections 5.1, 5.2 (pp. 67-75)
• Chapter 5, sections 5.3, 5.4 (pp. 75-86, new p. 75 replaces old one)