False Failure: Creating Failure Models for Separation Logic

C. Bannister, P. Höfner

Abstract: Separation logic, an extension of Floyd-Hoare logic, finds countless applications in areas of program verification, but does not allow forward reasoning in the setting of total or generalised correctness. To support forward reasoning, separation logic needs to be equiped with a failure element. We present several ways on how to add such an element. We show that none of the `obvious' extensions preserve all the algebraic properties desired. We develop more complicated models, satisfying the desired properties, and discuss their use for forward reasoning.

Paper: pdf


This page contains provisional data about the above paper. In particular is provides links to our Isabelle/HOL files. Currently the files are still unorganised; we are polishing as we speak — sorry for any inconvenience.
After the files are better organised and polished we will make them avaible at a more permanent place (e.g. GitHub or AFP).

(Abstract) Algebraic Theorems about Quantales (following the models discussed in the paper)
    File 1
    File 2

Forward and Backward Reasoning in Separation Logic
We develop techniques to allow backward and forward reasoning for separation logic and implement our framework in the interactive theorem prover Isabelle/HOL.
Details about our development can be found in the paper
[BHK18]  Bannister, C., Höfner, P., Klein, G.:Backwards and Forwards with Separation Logic. In: Interactive Theorem Proving (ITP 2018). Lecture Notes in Computer Science 10895, pp.68-87, Springer, 2018. doi: 10.1007/978-3-319-94821-8_5  
Our framework can be accessed via https://github.com/sel4proj/Jormungand


Contact: Peter Höfner: peter.hoefner <at> data61.csiro.au

Last update: Sep. 01, 2018