Aarhus University Seal / Aarhus Universitets segl

Fictional Separation Logic

Research output: Contribution to book/anthology/report/proceedingArticle in proceedingsResearchpeer-review

Separation logic formalizes the idea of local reasoning for heap-manipulating programs via the frame rule and the separating conjunction P * Q, which describes states that can be split into \emph{separate} parts, with one satisfying P and the other satisfying Q. In standard separation logic, separation means physical separation. In this paper, we introduce \emph{fictional separation logic}, which includes more general forms of fictional separating conjunctions P * Q, where "*" does not require physical separation, but may also be used in situations where the memory resources described by P and Q overlap. We demonstrate, via a range of examples, how fictional separation logic can be used to reason locally and modularly about mutable abstract data types, possibly implemented using sophisticated sharing. Fictional separation logic is defined on top of standard separation logic, and both the meta-theory and the application of the logic is much simpler than earlier related approaches.
Original languageEnglish
Title of host publicationLecture Notes in Computer Science : 21st European Symposium on Programming, ESOP 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 - April 1, 2012. Proceedings
EditorsHelmut Seidl
Number of pages20
Volume7211
PublisherSpringer
Publication year2012
Pages377-396
ISBN (print)978-3-642-28868-5
ISBN (Electronic)978-3-642-28869-2
Publication statusPublished - 2012
Externally publishedYes

See relations at Aarhus University Citationformats

ID: 73743362