Trustworthy Systems

Backwards and forwards with separation logic

Authors

Callum Bannister, Peter Hoefner and Gerwin Klein

DATA61

UNSW Sydney

Australian National University

Abstract

The use of Hoare logic in combination with weakest preconditions 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 operator. We implement our framework in the interactive theorem prover Isabelle/HOL, and enable automation with several interactive proof tactics.

BibTeX Entry

  @inproceedings{Bannister_HK_18,
    address          = {Oxford},
    author           = {Bannister, Callum and H\"{o}fner, Peter and Klein, Gerwin},
    booktitle        = {International Conference on Interactive Theorem Proving},
    date             = {2018-7-9},
    doi              = {https://doi.org/10.1007/978-3-319-94821-8\_5},
    month            = jul,
    pages            = {68--87},
    paperurl         = {https://trustworthy.systems/publications/full_text/Bannister_HK_18.pdf},
    publisher        = {Lecture Notes in Computer Science},
    title            = {Backwards and Forwards with Separation Logic},
    volume           = {10895},
    year             = {2018}
  }

Download