326.506Formal Specification and Verification Lecturer: Dr. Heinrich Rolletschek Time and place: Thursday, 10:1511:45, K 009D. 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. The main topics are:  Basic verification rules.
 A formal mathematical bases for the verification rules.
 Some applications.
 Dealing with structured data types.
 Dealing with functions and procedures.
Literature: Lecture notes.Final Exam:Friday, October 4, 8:3010:00, K 012 D I intend to give another written exam on November 29, but this is not yet fixed. Please let me know if you
intend to participate, and perhaps at which times you cannot. If this date is too early or too late for you,
then an oral exam can also be arranged.
