Peter W. O'Hearn

17 references under this name, matched as it is written. Somebody else may write under it too, and the same person may appear here spelled another way.

This description was written by a machine and published without a person checking it. It is what the agent made of this grouping, and not a statement anybody has stood behind.

Peter W. O'Hearn

Separation logic, from the connective to the tool: the logic of bunched implications supplies a conjunction that splits without a modality, BI becomes an assertion language for mutable data structures and then a program logic for local reasoning, and resources, concurrency and local reasoning extends it to concurrent programs. The corpus holds the analysers that followed -- Smallfoot, shape analysis, and compositional analysis by bi-abduction -- together with his own account of the path from categorical logic to a tool run against a production codebase. The most recent record argues the other way round: incorrectness logic reasons about what a program does wrong rather than what it does right. dblp: https://dblp.org/pid/o/PeterWOHearn

Incorrectness logic
Peter W. O'Hearn (2020) · Proceedings of the ACM on Programming Languages · Association for Computing Machinery
Separation logic
Peter W. O'Hearn (2019) · Communications of the ACM
Why Separation Logic Works
David Pym and others (2019) · Philosophy & Technology · Springer
Concurrent separation logic
Stephen Brookes and others (2016) · ACM SIGLOG News
A Primer on Separation Logic (and Automatic Program Verification and Analysis)
Peter W. O'Hearn (2012) · Software Safety and Security: Tools for Analysis and Verification · IOS Press
Compositional Shape Analysis by Means of Bi-Abduction
Cristiano Calcagno and others (2011) · Journal of the ACM · Association for Computing Machinery
Local Action and Abstract Separation Logic
Cristiano Calcagno and others (2007) · 22nd Annual IEEE Symposium on Logic in Computer Science (LICS 2007) · IEEE
Resources, concurrency, and local reasoning
Peter W. O'Hearn (2007) · Theoretical Computer Science · Elsevier
Smallfoot: Modular Automatic Assertion Checking with Separation Logic
Josh Berdine and others (2006) · Formal Methods for Components and Objects · Springer Berlin Heidelberg
A Local Shape Analysis Based on Separation Logic
Dino Distefano and others (2006) · Tools and Algorithms for the Construction and Analysis of Systems · Springer
Symbolic Execution with Separation Logic
Josh Berdine and others (2005) · Programming Languages and Systems, Third Asian Symposium, APLAS 2005, Tsukuba, Japan, November 2-5, 2005, Proceedings · Springer
A Decidable Fragment of Separation Logic
Josh Berdine and others (2004) · FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science · Springer
A Semantic Basis for Local Reasoning
Hongseok Yang and others (2002) · Foundations of Software Science and Computation Structures · Springer
Computability and Complexity Results for a Spatial Assertion Language for Data Structures
Cristiano Calcagno and others (2001) · Foundations of Software Technology and Theoretical Computer Science (FSTTCS) · Springer
BI as an assertion language for mutable data structures
Samin S. Ishtiaq and others (2001) · 28th ACM Symposium on Principles of Programming Languages (POPL)
Local Reasoning about Programs that Alter Data Structures
Peter W. O'Hearn and others (2001) · Computer Science Logic · Springer
The logic of bunched implications
Peter W. O'Hearn and others (1999) · Bulletin of Symbolic Logic