326.506-Formal Specification and Verification

Lecturer: Dr. Heinrich Rolletschek

Time and place: Thursday, 10:15-11: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.

Final Exam:Friday, October 4, 8:30-10: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.