FakultätskolloquiumVeranstalter: M. Mendler Donnerstag, 14.2.2019: 16:00 - 18:00 Uhr; WE5/04.004Prof. 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.
|