News       Library       Links       Sitemap       Search  
 Formale Spezifikation und Verifikation

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)
Final Exam: July 4, 8:30-10:00, BA 9912. One A4-page with handwritten notes may be used.
    This page is maintained by Heinrich Rolletschek . Last updated on June 27, 2001