Separation logic: a logic for shared mutable data structures

By John C. Reynolds. 2002

2,727 citations recorded by the source corpus.

Subfields: Artificial Intelligence, Computer Networks and Communications, Hardware and Architecture, Program Analysis & Verification

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Computer Networks and Communications

In Hardware and Architecture

In Program Analysis & Verification

Citations in the corpus

Gated Graph Sequence Neural Networks (2015, methodology): “The results for this task are given in Reynolds, 2002), which uses inductive predicates to describe abstract data structures.”
Permission accounting in separation logic (2005, background): “Reynolds, O’Hearn and Yang [20, 19, 14] and others developed the logic to describe mutation of the heap based on a notion of separate locations.”
Separation logic and abstraction (2005, methodology): “The interested reader can read further de tails and references in a survey paper by Reynolds [29].”
RustBelt: securing the foundations of the rust programming language (2017, background): “By virtue of being a separation logic [O’Hearn 2007; Reynolds 2002], Iris comes with built-in support for reasoning modularly about ownership.”
Iris (2015, background): “This goal has sparked a long line of work, especially in recent years, during which a synthesis of rely-guarantee reasoning [21] and separation logic [31, 28] has led to a series of increasingly advanced program logics for concurrency: RGSep [37], SAGL [13], LRG [12], CAP [10], HLRG [15], CaReSL [34”
Checking Interference with Fractional Permissions (2003, methodology): “Reynolds and O’Hearn have continued analysis of mutable data structures using the logic of “bunched implications” [10] and “separation logic” [12].”
A type and effect system for deterministic parallel Java (2009, background): “First, SL is a low-level specification language: it generally treats memory as a single array of words, on which notions of objects and linked data structures must be defined using SL predicates [40, 35].”
Symbolic Execution with Separation Logic (2005, methodology): “Separation Logic has provided an approach to reasoning about programs with pointers that often leads to simpler specifications and program proofs than previous formalisms [12].”
Local Action and Abstract Separation Logic (2007, methodology): “Separation logic is an extension of Hoare's logic which has been used to attack the old problem of reasoning about the mutation of data structures in memory [33] [17] [23] [34].”
A Semantics for Concurrent Separation Logic (2004, methodology): “Separation logic [17] provides a class of formulas for specifying properties of stores and heaps.”
Learning Shape Analysis (2017, methodology): “Separation logic [33, 36] has often been used in automatic reasoning about such programs, as its frame rule favors compositional reasoning and thus promises scalable verification tools.”
Resources, Concurrency and Local Reasoning (2004, methodology): “The purpose of this work is to revisit these issues, using the recent formalism of separation logic [11].”