Backwards and Forwards with Separation Logic

The work

AuthorsCallum Bannister; Peter Höfner; Gerwin Klein
Editors
Typeinproceedings
Year2018
Citekeybannister2018backwards

Where it appeared

Published in9th International Conference on Interactive Theorem Proving (ITP)
PublisherSpringer
SeriesLecture Notes in Computer Science
Volume10895
Pages68--87

Identifiers

DOI10.1007/978-3-319-94821-8_5
ISBN978-3-319-94820-1

Abstract

The use of Hoare logic in combination with weakest pre- conditions and strongest postconditions is a standard tool for program verification, known as backward and forward reasoning. In this paper we 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 en- able automation with several interactive proof tactics.

A copy is held

pdf, 224.1 kB. Not published — it may be under copyright. The facts and links here are.

How it got here

How it got hereagent via bibtex
Added2026-08-05 00:00 UTC
Approved bya person 2026-08-17 08:38 UTC

Filed under

gerwinklein lncs separation-logic the-copy-is-not-the-work

Cite it as

@inproceedings{bannister2018backwards,
  title        = {Backwards and Forwards with Separation Logic},
  author       = {Callum Bannister and Peter Höfner and Gerwin Klein},
  year         = {2018},
  booktitle    = {9th International Conference on Interactive Theorem Proving (ITP)},
  publisher    = {Springer},
  series       = {Lecture Notes in Computer Science},
  volume       = {10895},
  pages        = {68--87},
  isbn         = {978-3-319-94820-1},
  doi          = {10.1007/978-3-319-94821-8_5},
}

This record lives at https://refs.drheap.org/bannister2018backwards/ and will keep doing so.