Resources, Concurrency and Local Reasoning

By Peter W. O'Hearn. International Conference on Concurrency Theory, 2004

801 citations recorded by the source corpus.

Subfields: Artificial Intelligence, Computational Theory and Mathematics, Computer Networks and Communications

View Paper: https://www.semanticscholar.org/paper/9651bfd271e42b77f259828dc39920042731584b

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 Computer Networks and Communications

Citations in the corpus

A Local Shape Analysis Based on Separation Logic (2006, methodology): “This example is motivated by the treatment of a concurrent queue in [11].”
Towards a program logic for JavaScript (2012, background): “separation logic with sharing [9, 20, 31], but they all seem to take a different approach to our t∗ connective.”
VCC: A Practical System for Verifying Concurrent C (2009, background): “In contrast to rely/guarantee, concurrent separation logic exploits that large portions of the program state may be operated on mutually exclusive [20, 21].”
Local Action and Abstract Separation Logic (2007, background): “The need for precision of these predicates (the lock invariants) can be seen from the Reynolds counterexample for concurrent separation logic [ 22 , 12].”
A Marriage of Rely/Guarantee and Separation Logic (2007, methodology): “’ On the other hand, the recent development of separation logic [19, 15] suggests that greater modularity is possible.”
Separation logic and abstraction (2005, background): “3 Permissions reading O’Hearn [21] has recently given separation logic an ownersh ip, or permissions, interpretation: E 7→ E is the permission to read, write and dispose the cell at location E.”
A type and effect system for deterministic parallel Java (2009, background): “Subarrays and partitioning provide a natural object-oriented way to encode disjoint segments of arrays, in contrast to lower-level mechanisms like separation logic [35] that specify array index ranges directly.”
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”
A Formally Verified Compiler Back-end (2009, background): “A powerful way to characterize such programs is concurrent separation logic [79].”
Compositional shape analysis by means of bi-abduction (2009, background): “Based on concurrent separation logic [O’Hearn 2007], one might expect that the results of a sequential analysis could in some circumstances be sound in a concurrent model [Berdine et al.”
A Semantics for Concurrent Separation Logic (2004, methodology): “Similar restrictions are made in O’Hearn’s paper [31].”