Local Reasoning about Programs that Alter Data Structures

By Peter W. O'Hearn, John C. Reynolds, Hongseok Yang. 2001

883 citations recorded by the source corpus.

Subfields: Artificial Intelligence, Computational Theory and Mathematics, Natural Language Processing, 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 Computational Theory and Mathematics

In Natural Language Processing

In Program Analysis & Verification

Citations in the corpus

Gated Graph Sequence Neural Networks (2015, methodology): “For all tasks GG-NN achieves perfect test accuracy using only 50 training examples, while the RNN/LSTM baselines either use more training examples (Task 4) or fail to solve the tasks (Task 15, 16 and 18).”
Permission accounting in separation logic (2005, methodology): “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.”
Towards a program logic for JavaScript (2012, methodology): “Using the separating conjunction ∗ [19], the assertion ((l, x) 7→ v) ∗ ((l, y) 7→ w) declares that a heap contains an object l which must have two separate fields x, y with the appropriate values.”
The verifying compiler: A grand challenge for computing research (2003, background): “Theories relevant for the correctness of concurrency are well established [40-42]; and theories for object orientation and pointer manipulation are under development [43,44].”
A Local Shape Analysis Based on Separation Logic (2006, background): “Early on in separation logic there was an emphasis on what was referred to as “local reasoning”: reasoning concentrates on the cells accessed during computation [12].”
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.”
Smallfoot: Modular Automatic Assertion Checking with Separation Logic (2005, methodology): “For a full understanding of exactly how Smallfoot works familiarity with [32, 35, 31, 5] is essential.”
Separation logic: a logic for shared mutable data structures (2002, methodology): “More recently, I generalized the logic to permit reasoning about unrestricted address arithmetic, by regarding addresses a s integers which refer to individual fields [24, 30, 29].”
Iris from the ground up: A modular foundation for higher-order concurrent separation logic (2018, neutral): “Around the turn of the millennium, Peter O’Hearn, John Reynolds, Hongseok Yang, and collaborators proposed separation logic, a derivative of Hoare logic geared toward reasoning more modularly and scalably about pointer-manipulating programs (O’Hearn et al., 2001; Reynolds, 2002).”
Resources, Concurrency and Local Reasoning (2004, background): “Local reasoning [6] is possible in such a situation because dynamic, non scope-based, uses of semaphores to protect resources are matched by the dynamic, non scope-based, approach to resource separation provided by separation logic.”
Local Action and Abstract Separation Logic (2007, methodology): “Neither did we explicitly include the Hoare logic rule for introducing existentials [23]; it, semantically, just boils down to the disjunction rule.”
Separation logic and abstraction (2005, methodology): “We choose to build upon the recent formalism of separation lo gic, which facilitates local reasoning about code [23].”
Symbolic Execution with Separation Logic (2005, background): “Separation Logic allows specifications to be kept small because it avoids the need to state frame axioms, which describe the portions of the heap not altered by a command [10].”
Formal methods: Practice and experience (2009, background): “There has been a move beyond the theory for veri.cation of well-structured subsets of a programming language, to deal with the more potentially undisciplined aspects of programming; for example, pointer swinging [O Hearn et al. 2001] and concurrency [Vafeiadis and Parkinson 2007].”
A Marriage of Rely/Guarantee and Separation Logic (2007, methodology): “We adopt all of the small axioms for local state from separation logic (not presented) [14].”