Separation logics and modalities: a survey

The work

AuthorsStéphane Demri; Morgan Deters
Editors
Typearticle
Year2015
Citekeydemri2015separation

Where it appeared

Published inJournal of Applied Non-Classical Logics
Volume25
Issue1
Pages50--99

Abstract

Like modal logic, temporal logic, or description logic, separation logic has become a popular class of logical formalisms in computer science, conceived as assertion languages for Hoare-style proof systems with the goal to perform automatic program analysis. In a broad sense, separation logic is often understood as a programming language, an assertion language and a family of rules involving Hoare triples. In this survey, we present similarities between separation logic as an assertion language and modal and temporal logics. Moreover, we propose a selection of landmark results about decidability, complexity and expressive power.

A copy is held

pdf, 560.8 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-21 22:06 UTC

Cite it as

@article{demri2015separation,
  title        = {Separation logics and modalities: a survey},
  author       = {Stéphane Demri and Morgan Deters},
  year         = {2015},
  journal      = {Journal of Applied Non-Classical Logics},
  volume       = {25},
  number       = {1},
  pages        = {50--99},
  doi          = {10.1080/11663081.2015.1018801},
}

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