Fakultätskolloquium

Veranstalter: M. Mendler

Prof. Dr. Peter Höfner (CSIRO & The University of New South Wales Sydney, Australia):
Backwards and Forwards in Separation Logic.
The use of Hoare logic in combination with weakest pre- and strongest post-conditions is a standard tool for program verification, known as backward and forward reasoning. In this talk I extend these techniques to allow backward and forward reasoning for separation logic. While the former is derived directly from the standard operators of separation logic, the latter uses a new one. We implement our framework in the interactive proof assistant Isabelle/HOL, and enable automation with several interactive proof tactics.

Kontakt:

Lüttgen, Gerald Lehrstuhl für Praktische Informatik, insbesondere Softwaretechnik und Programmiersprachen Telefon +49 (0)951 863-3850, Fax +49 (0)951 863-3855, E-Mail: gerald.luettgen@uni-bamberg.de