Peter W. O'Hearn

ORCID

Publication Activity (10 Years)

Years Active: 1989-2023
Publications (10 Years): 21

Top Venues

Proc. ACM Program. Lang.

RAMiCS

LICS

Commun. ACM

Publications

Azalea Raad, Julien Vanegue, Josh Berdine, Peter W. O'Hearn
A General Approach to Under-Approximate Reasoning About Concurrent Programs. CONCUR (2023)
Azalea Raad, Josh Berdine, Derek Dreyer, Peter W. O'Hearn
Concurrent incorrectness separation logic. Proc. ACM Program. Lang. 6 (POPL) (2022)
Quentin Carbonneaux, Noam Zilberstein, Christoph Klee, Peter W. O'Hearn, Francesco Zappa Nardelli
Applying formal verification to microkernel IPC at meta. CPP (2022)
Quang Loc Le, Azalea Raad, Jules Villard, Josh Berdine, Derek Dreyer, Peter W. O'Hearn
Finding real bugs in big programs with incorrectness logic. Proc. ACM Program. Lang. 6 (OOPSLA) (2022)
Bernhard Möller, Peter W. O'Hearn, Tony Hoare
On Algebra of Program Correctness and Incorrectness. RAMiCS (2021)
Peter W. O'Hearn
Incorrectness logic. Proc. ACM Program. Lang. 4 (POPL) (2020)
Azalea Raad, Josh Berdine, Hoang-Hai Dang, Derek Dreyer, Peter W. O'Hearn, Jules Villard
Local Reasoning About the Presence of Bugs: Incorrectness Separation Logic. CAV (2) (2020)
Peter W. O'Hearn
Formal reasoning and the hacker way (keynote). SOAP@PLDI (2020)
Nikos Gorogiannis, Peter W. O'Hearn, Ilya Sergey
A true positives theorem for a static race detector. Proc. ACM Program. Lang. 3 (POPL) (2019)
Dino Distefano, Manuel Fähndrich, Francesco Logozzo, Peter W. O'Hearn
Scaling static analyses at Facebook. Commun. ACM 62 (8) (2019)
Peter W. O'Hearn
Separation logic. Commun. ACM 62 (2) (2019)
Nikos Gorogiannis, Peter W. O'Hearn, Ilya Sergey
A True Positives Theorem for a Static Race Detector - Extended Version. CoRR (2018)
Sam Blackshear, Nikos Gorogiannis, Peter W. O'Hearn, Ilya Sergey
RacerD: compositional static race detection. Proc. ACM Program. Lang. 2 (OOPSLA) (2018)
Peter W. O'Hearn
Continuous Reasoning: Scaling the impact of formal methods. LICS (2018)
Peter W. O'Hearn
Experience Developing and Deploying Concurrency Analysis at Facebook. SAS (2018)
Mark Harman, Peter W. O'Hearn
From Start-ups to Scale-ups: Opportunities and Open Problems for Static and Dynamic Program Analysis. SCAM (2018)
Stephen Brookes, Peter W. O'Hearn
Concurrent separation logic. ACM SIGLOG News 3 (3) (2016)
Byron Cook, Carsten Fuhs, Kaustubh Nimkar, Peter W. O'Hearn
Embracing Overapproximation for Proving Nontermination. Tiny Trans. Comput. Sci. 3 (2015)
Peter W. O'Hearn, Rasmus Lerchedahl Petersen, Jules Villard, Akbar Hussain
On the relation between Concurrent Separation Logic and Concurrent Kleene Algebra. J. Log. Algebraic Methods Program. 84 (3) (2015)
Peter W. O'Hearn
From Categorical Logic to Facebook Engineering. LICS (2015)
Cristiano Calcagno, Dino Distefano, Jérémy Dubreil, Dominik Gabi, Pieter Hooimeijer, Martino Luca, Peter W. O'Hearn, Irene Papakonstantinou, Jim Purbrick, Dulma Rodriguez
Moving Fast with Software Verification. NFM (2015)
Stephen Brookes, Peter W. O'Hearn, Uday S. Reddy
The essence of Reynolds. POPL (2014)
Byron Cook, Carsten Fuhs, Kaustubh Nimkar, Peter W. O'Hearn
Disproving termination with overapproximation. FMCAD (2014)
Stephen Brookes, Peter W. O'Hearn, Uday S. Reddy
The Essence of Reynolds. Formal Aspects Comput. 26 (3) (2014)
Tony Hoare, Stephan van Staden, Bernhard Möller, Georg Struth, Jules Villard, Huibiao Zhu, Peter W. O'Hearn
Developments in Concurrent Kleene Algebra. RAMiCS (2014)
Hong Yi Chen, Byron Cook, Carsten Fuhs, Kaustubh Nimkar, Peter W. O'Hearn
Proving Nontermination via Safety. TACAS (2014)
Andrew P. Black, Peter W. O'Hearn
Presentation of the SIGPLAN distinguished achievement award to Sir Charles Antony Richard Hoare, FRS, FREng, FBCS; and interview. POPL (2012)
Josh Berdine, Cristiano Calcagno, Peter W. O'Hearn
Verification Condition Generation and Variable Conditions in Smallfoot CoRR (2012)
Nikos Gorogiannis, Max I. Kanovich, Peter W. O'Hearn
The Complexity of Abduction for Separated Heap Abstractions. SAS (2011)
Cristiano Calcagno, Dino Distefano, Peter W. O'Hearn, Hongseok Yang
Compositional Shape Analysis by Means of Bi-Abduction. J. ACM 58 (6) (2011)
Peter W. O'Hearn
Reasoning about Programs Using a Scientific Method. ICFEM (2011)
Peter W. O'Hearn
Algebra, Logic, Locality, Concurrency. CPP (2011)
Peter W. O'Hearn
Algebra, Logic, Locality, Concurrency. APLAS (2011)
C. A. R. Hoare, Akbar Hussain, Bernhard Möller, Peter W. O'Hearn, Rasmus Lerchedahl Petersen, Georg Struth
On Locality and the Exchange Law for Concurrent Processes. CONCUR (2011)
Peter W. O'Hearn, Noam Rinetzky, Martin T. Vechev, Eran Yahav, Greta Yorsh
Verifying linearizability with hindsight. PODC (2010)
Peter W. O'Hearn
Abductive, Inductive and Deductive Reasoning about Resources. CSL (2010)
Ivana Filipovic, Peter W. O'Hearn, Noam Rinetzky, Hongseok Yang
Abstraction for concurrent objects. Theor. Comput. Sci. 411 (51-52) (2010)
Ivana Filipovic, Peter W. O'Hearn, Noah Torp-Smith, Hongseok Yang
Blaming the client: on data refinement in the presence of pointers. Formal Aspects Comput. 22 (5) (2010)
Mooly Sagiv, Arnd Poetzsch-Heffter, Peter W. O'Hearn
09301 Executive Summary - Typing, Analysis, and Verification of Heap-Manipulating Programs. Typing, Analysis and Verification of Heap-Manipulating Programs (2009)
Ian Wehrman, C. A. R. Hoare, Peter W. O'Hearn
Graphical models of separation logic. Inf. Process. Lett. 109 (17) (2009)
Ivana Filipovic, Peter W. O'Hearn, Noam Rinetzky, Hongseok Yang
Abstraction for Concurrent Objects. ESOP (2009)
Mooly Sagiv, Arnd Poetzsch-Heffter, Peter W. O'Hearn
09301 Abstracts Collection - Typing, Analysis, and Verification of Heap-Manipulating Programs. Typing, Analysis and Verification of Heap-Manipulating Programs (2009)
Peter W. O'Hearn, Hongseok Yang, John C. Reynolds
Separation and information hiding. ACM Trans. Program. Lang. Syst. 31 (3) (2009)
Cristiano Calcagno, Dino Distefano, Peter W. O'Hearn, Hongseok Yang
Compositional shape analysis by means of bi-abduction. POPL (2009)
Peter W. O'Hearn
Separation Logic Tutorial. ICLP (2008)
Cristiano Calcagno, Dino Distefano, Peter W. O'Hearn, Hongseok Yang
Space Invading Systems Code. LOPSTR (2008)
Tony Hoare, Peter W. O'Hearn
Separation Logic Semantics for Communicating Processes. Electron. Notes Theor. Comput. Sci. 212 (2008)
Peter W. O'Hearn
Tutorial on Separation Logic (Invited Tutorial). CAV (2008)
Hongseok Yang, Oukseh Lee, Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, Peter W. O'Hearn
Scalable Shape Analysis for Systems Code. CAV (2008)
Cristiano Calcagno, Peter W. O'Hearn, Hongseok Yang
Local Action and Abstract Separation Logic. LICS (2007)
Peter W. O'Hearn
Separation logic and concurrent resource management. ISMM (2007)
Peter W. O'Hearn
Resources, concurrency, and local reasoning. Theor. Comput. Sci. 375 (1-3) (2007)
Matthew J. Parkinson, Richard Bornat, Peter W. O'Hearn
Modular verification of a non-blocking stack. POPL (2007)
Josh Berdine, Aziem Chawdhary, Byron Cook, Dino Distefano, Peter W. O'Hearn
Variance analyses from invariance analyses. POPL (2007)
Cristiano Calcagno, Dino Distefano, Peter W. O'Hearn, Hongseok Yang
Footprint Analysis: A Shape Analysis That Discovers Preconditions. SAS (2007)
Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, Peter W. O'Hearn, Thomas Wies, Hongseok Yang
Shape Analysis for Composite Data Structures. CAV (2007)
Olivier Danvy, Peter W. O'Hearn, Philip Wadler
Preface. Theor. Comput. Sci. 375 (1-3) (2007)
Dino Distefano, Peter W. O'Hearn, Hongseok Yang
A Local Shape Analysis Based on Separation Logic. TACAS (2006)
Cliff B. Jones, Peter W. O'Hearn, Jim Woodcock
Verified Software: A Grand Challenge. Computer 39 (4) (2006)
Peter W. O'Hearn
Separation Logic and Program Analysis. SAS (2006)
Josh Berdine, Byron Cook, Dino Distefano, Peter W. O'Hearn
Automatic Termination Proofs for Programs with Shape-Shifting Heaps. CAV (2006)
Josh Berdine, Peter W. O'Hearn
Strong Update, Disposal, and Encapsulation in Bunched Typing. MFPS (2006)
Cristiano Calcagno, Dino Distefano, Peter W. O'Hearn, Hongseok Yang
Beyond Reachability: Shape Abstraction in the Presence of Pointer Arithmetic. SAS (2006)
Peter W. O'Hearn
Scalable Specification and Reasoning: Challenges for Program Logic. VSTTE (2005)
Josh Berdine, Cristiano Calcagno, Peter W. O'Hearn
Symbolic Execution with Separation Logic. APLAS (2005)
Richard Bornat, Cristiano Calcagno, Peter W. O'Hearn, Matthew J. Parkinson
Permission accounting in separation logic. POPL (2005)
Josh Berdine, Cristiano Calcagno, Peter W. O'Hearn
Smallfoot: Modular Automatic Assertion Checking with Separation Logic. FMCO (2005)
Peter W. O'Hearn
Resources, Concurrency and Local Reasoning. CONCUR (2004)
Peter W. O'Hearn, Hongseok Yang, John C. Reynolds
Separation and information hiding. POPL (2004)
Ivana Mijajlovic, Noah Torp-Smith, Peter W. O'Hearn
Refinement and Separation Contexts. FSTTCS (2004)
Peter W. O'Hearn
Resources, Concurrency, and Local Reasoning (Abstract). ESOP (2004)
Josh Berdine, Cristiano Calcagno, Peter W. O'Hearn
A Decidable Fragment of Separation Logic. FSTTCS (2004)
David J. Pym, Peter W. O'Hearn, Hongseok Yang
Possible worlds and resources: the semantics of BI. Theor. Comput. Sci. 315 (1) (2004)
Cristiano Calcagno, Peter W. O'Hearn, Richard Bornat
Program logic and equivalence in the presence of garbage collection. Theor. Comput. Sci. 298 (3) (2003)
Peter W. O'Hearn
On bunched typing. J. Funct. Program. 13 (4) (2003)
Josh Berdine, Peter W. O'Hearn, Uday S. Reddy, Hayo Thielecke
Linear Continuation-Passing. High. Order Symb. Comput. 15 (2-3) (2002)
Hongseok Yang, Peter W. O'Hearn
A Semantic Basis for Local Reasoning. FoSSaCS (2002)
Cristiano Calcagno, Hongseok Yang, Peter W. O'Hearn
Computability and Complexity Results for a Spatial Assertion Language for Data Structures. APLAS (2001)
Cristiano Calcagno, Peter W. O'Hearn
On Garbage and Program Logic. FoSSaCS (2001)
Cristiano Calcagno, Hongseok Yang, Peter W. O'Hearn
Computability and Complexity Results for a Spatial Assertion Language for Data Structures. FSTTCS (2001)
Peter W. O'Hearn, John C. Reynolds, Hongseok Yang
Local Reasoning about Programs that Alter Data Structures. CSL (2001)
Samin S. Ishtiaq, Peter W. O'Hearn
BI as an Assertion Language for Mutable Data Structures. POPL (2001)
Peter W. O'Hearn, John C. Reynolds
From Algol to polymorphic linear lambda-calculus. J. ACM 47 (1) (2000)
Cristiano Calcagno, Samin S. Ishtiaq, Peter W. O'Hearn
Semantic analysis of pointer aliasing, allocation and disposal in Hoare logic351292. PPDP (2000)
Peter W. O'Hearn, David J. Pym
The logic of bunched implications. Bull. Symb. Log. 5 (2) (1999)
Peter W. O'Hearn, John Power, Makoto Takeyama, Robert D. Tennent
Syntactic Control of Interference Revisited. Theor. Comput. Sci. 228 (1-2) (1999)
Peter J. Freyd, Peter W. O'Hearn, A. John Power, Makoto Takeyama, R. Street, Robert D. Tennent
Bireflectivity. Theor. Comput. Sci. 228 (1-2) (1999)
Peter W. O'Hearn
-Calculus. TLCA (1999)
Peter W. O'Hearn, Uday S. Reddy
Objects, Interference, and the Yoneda Embedding. Theor. Comput. Sci. 228 (1-2) (1999)
Peter W. O'Hearn
Polymorphism, objects and abstract types. SIGACT News 29 (4) (1998)
Yoshiki Kinoshita, Peter W. O'Hearn, John Power, Makoto Takeyama, Robert D. Tennent
An Axiomatic Approach to Binary Logical Relations with Applications to Data Refinement. TACS (1997)
Peter W. O'Hearn
Note on Algol and Conservatively Extending Functional Programming. J. Funct. Program. 6 (1) (1996)
Peter W. O'Hearn, Jon G. Riecke
Kripke Logical Relations and PCF Inf. Comput. 120 (1) (1995)
Peter J. Freyd, Peter W. O'Hearn, John Power, Robert D. Tennent, Makoto Takeyama
Bireflectivity. MFPS (1995)
Peter W. O'Hearn, Uday S. Reddy
Objects, interference and the Yoneda embedding. MFPS (1995)
Peter W. O'Hearn, Robert D. Tennent
Parametricity and Local Variables. J. ACM 42 (3) (1995)
Peter W. O'Hearn, John Power, Robert D. Tennent, Makoto Takeyama
Syntactic control of interference revisited. MFPS (1995)
Peter W. O'Hearn, Jon G. Riecke
Fully Abstract Translations and Parametric Polymorphism. ESOP (1994)
Peter W. O'Hearn, Robert D. Tennent
Semantical Analysis of Specification Logic, 2 Inf. Comput. 107 (1) (1993)
Peter W. O'Hearn, Robert D. Tennent
Relational Parametricity and Local Variables. POPL (1993)

Peter W. O'Hearn.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Peter W. O'Hearn