Program Verification Using Change Information

Prof. Bernhard Beckert (University of Koblenz)

CSL SEMINAR SERIES

DATE: 2003-10-21
TIME: 16:00:00 - 17:00:00
LOCATION: RSISE Seminar Room, ground floor, building 115, cnr. North and Daley Roads, ANU
CONTACT: JavaScript must be enabled to display this email address.

ABSTRACT:
In this talk, I propose an extension of the design-by-contract approach. In addition to preconditions, postconditions, and invariants as the basis for proving properties of a program, also information should be provided on which parts of the state are not changed by running the program. This is done in the form of modifier sets. I present a precise semantics of modifier sets and theorems on how to use them in program-correctness proofs.

This technique has been implemented as part of the KeY system, and I will give a short overview of the KeY project and a demo.
BIO:
Prof. Beckert got an M.Sc. (1993) and a Ph.D. (1998) in Computer Science from the University of Karlsruhe, where he held a post-doc position (Assistent) until this year. Since September 2003, he is an Assistant Professor (Juniorprofessor) at the University of Koblenz.

Prof. Beckert's research interests include: - Formal Methods in Software Engineering - Program Verification - Automated Deduction in Classical and Non-classical Logics