326.506Formal Specification and Verification Lecturer: Dr. Heinrich Rolletschek Time and place: Wednesday, 12:0013: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. 120)
 Corrected pages 1521 (replace original pages 1520)
 Chapter 2 (pp. 2332)
 Chapter 3 (pp. 3343)
 Chapter 4, sections 4.14.3 (pp. 4558)
 Rest of Chapter 4 (section 4.4, pp. 5965)
 Chapter 5, sections 5.1, 5.2 (pp. 6775)
 Chapter 5, sections 5.3, 5.4 (pp. 7586, new p. 75 replaces old one)
Final Exam: July 4, 8:3010:00, BA 9912. One A4page with handwritten notes may be used.
