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
A grouping.
Peter W. O'Hearn: separation logic from the connective to the tool - bunched implications, local reasoning, concurrent separation logic, then Smallfoot, shape analysis and bi-abduction.
24 references
Finding real bugs in big programs with incorrectness logic
Quang Loc Le and others (2022) · Proceedings of the ACM on Programming Languages · Association for Computing Machinery
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
Continuous Reasoning
Peter W. O’Hearn (2018) · Proceedings - Symposium on Logic in Computer Science · Institute of Electrical and Electronics Engineers
Concurrent separation logic
Stephen Brookes and others (2016) · ACM SIGLOG News
From categorical logic to Facebook engineering
Peter O'Hearn (2015) · 2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science · IEEE
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
Scalable Shape Analysis for Systems Code
Hongseok Yang and others (2008) · Lecture notes in computer science · Springer Science+Business Media
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
Permission accounting in separation logic
Richard Bornat and others (2005) · Proceedings of the 32nd ACM Symposium on Principles of Programming Languages
A Decidable Fragment of Separation Logic
Josh Berdine and others (2004) · FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science · Springer
Refinement and Separation Contexts
Ivana Mijajlović and others (2004) · FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science · Springer Berlin Heidelberg
Possible worlds and resources: the semantics of BI
David J. Pym and others (2004) · Theoretical Computer Science · Elsevier BV
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