Trustworthy Systems

False failure: Creating failure models for separation logic

Authors

Callum Bannister and Peter Hoefner

DATA61

UNSW Sydney

Australian National University

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.

BibTeX Entry

  @inproceedings{Bannister_Hoefner_18,
    address          = {Groningen},
    author           = {Bannister, Callum and H\"{o}fner, Peter},
    booktitle        = {17th International Conference on Relational and Algebraic Methods in Computer Science},
    date             = {2018-10-29},
    doi              = {https://doi.org/10.1007/978-3-030-02149-8\_16},
    editor           = {{Stef Joosten, Jules Desharnais, Walter Guttmann}},
    keywords         = {separation logic; generalised correctness; forward reasoning},
    month            = oct,
    pages            = {263-279},
    paperurl         = {https://trustworthy.systems/publications/full_text/Bannister_Hoefner_18.pdf},
    publisher        = {Springer},
    series           = {Lecture Notes in Computer Science},
    title            = {False Failure: Creating Failure Models for Separation Logic},
    volume           = {11194},
    year             = {2018}
  }

Download