Peter W. O'Hearn

According to our database, Peter W. O'Hearn authored at least 97 papers between 1989 and 2024.

Collaborative distances:

• Dijkstra number of two.
• Erdős number of four.

2024

Non-termination Proving at Scale.

Azalea Raad, Julien Vanegue, Peter W. O'Hearn

Proc. ACM Program. Lang., 2024

2023

A General Approach to Under-Approximate Reasoning About Concurrent Programs.

Azalea Raad, Julien Vanegue, Josh Berdine, Peter W. O'Hearn

Proceedings of the 34th International Conference on Concurrency Theory, 2023

2022

Concurrent incorrectness separation logic.

Azalea Raad, Josh Berdine, Derek Dreyer, Peter W. O'Hearn

Proc. ACM Program. Lang., 2022

Finding real bugs in big programs with incorrectness logic.

Quang Loc Le, Azalea Raad, Jules Villard, Josh Berdine, Derek Dreyer, Peter W. O'Hearn

Proc. ACM Program. Lang., 2022

Applying formal verification to microkernel IPC at meta.

Quentin Carbonneaux, Noam Zilberstein, Christoph Klee, Peter W. O'Hearn, Francesco Zappa Nardelli

Proceedings of the CPP '22: 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, Philadelphia, PA, USA, January 17, 2022

2021

On Algebra of Program Correctness and Incorrectness.

Bernhard Möller, Peter W. O'Hearn, Tony Hoare

Proceedings of the Relational and Algebraic Methods in Computer Science, 2021

2020

Incorrectness logic.

Peter W. O'Hearn

Proc. ACM Program. Lang., 2020

Formal reasoning and the hacker way (keynote).

Peter W. O'Hearn

Proceedings of the 9th ACM SIGPLAN International Workshop on the State Of the Art in Program Analysis, 2020

Local Reasoning About the Presence of Bugs: Incorrectness Separation Logic.

Azalea Raad, Josh Berdine, Hoang-Hai Dang, Derek Dreyer, Peter W. O'Hearn, Jules Villard

Proceedings of the Computer Aided Verification - 32nd International Conference, 2020

2019

A true positives theorem for a static race detector.

Nikos Gorogiannis, Peter W. O'Hearn, Ilya Sergey

Proc. ACM Program. Lang., 2019

Separation logic.

Peter W. O'Hearn

Commun. ACM, 2019

Scaling static analyses at Facebook.

Dino Distefano, Manuel Fähndrich, Francesco Logozzo, Peter W. O'Hearn

Commun. ACM, 2019

2018

RacerD: compositional static race detection.

Sam Blackshear, Nikos Gorogiannis, Peter W. O'Hearn, Ilya Sergey

Proc. ACM Program. Lang., 2018

A True Positives Theorem for a Static Race Detector - Extended Version.

Nikos Gorogiannis, Peter W. O'Hearn, Ilya Sergey

CoRR, 2018

From Start-ups to Scale-ups: Opportunities and Open Problems for Static and Dynamic Program Analysis.

Mark Harman, Peter W. O'Hearn

Proceedings of the 18th IEEE International Working Conference on Source Code Analysis and Manipulation, 2018

Experience Developing and Deploying Concurrency Analysis at Facebook.

Peter W. O'Hearn

Proceedings of the Static Analysis - 25th International Symposium, 2018

Continuous Reasoning: Scaling the impact of formal methods.

Peter W. O'Hearn

Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, 2018

2016

Concurrent separation logic.

Stephen Brookes, Peter W. O'Hearn

ACM SIGLOG News, 2016

2015

Embracing Overapproximation for Proving Nontermination.

Byron Cook, Carsten Fuhs, Kaustubh Nimkar, Peter W. O'Hearn

Adv. Math. Commun., 2015

On the relation between Concurrent Separation Logic and Concurrent Kleene Algebra.

Peter W. O'Hearn, Rasmus Lerchedahl Petersen, Jules Villard, Akbar Hussain

J. Log. Algebraic Methods Program., 2015

Moving Fast with Software Verification.

Cristiano Calcagno, Dino Distefano, Jérémy Dubreil, Dominik Gabi, Pieter Hooimeijer, Martino Luca, Peter W. O'Hearn, Irene Papakonstantinou, Jim Purbrick, Dulma Rodriguez

Proceedings of the NASA Formal Methods - 7th International Symposium, 2015

From Categorical Logic to Facebook Engineering.

Peter W. O'Hearn

Proceedings of the 30th Annual ACM/IEEE Symposium on Logic in Computer Science, 2015

2014

The Essence of Reynolds.

Stephen Brookes, Peter W. O'Hearn, Uday S. Reddy

Formal Aspects Comput., 2014

Proving Nontermination via Safety.

Hong Yi Chen, Byron Cook, Carsten Fuhs, Kaustubh Nimkar, Peter W. O'Hearn

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2014

Disproving termination with overapproximation.

Byron Cook, Carsten Fuhs, Kaustubh Nimkar, Peter W. O'Hearn

Proceedings of the Formal Methods in Computer-Aided Design, 2014

Developments in Concurrent Kleene Algebra.

Tony Hoare, Stephan van Staden, Bernhard Möller, Georg Struth, Jules Villard, Huibiao Zhu, Peter W. O'Hearn

Proceedings of the Relational and Algebraic Methods in Computer Science, 2014

2012

A Primer on Separation Logic (and Automatic Program Verification and Analysis).

Peter W. O'Hearn

Proceedings of the Software Safety and Security - Tools for Analysis and Verification, 2012

Verification Condition Generation and Variable Conditions in Smallfoot

Josh Berdine, Cristiano Calcagno, Peter W. O'Hearn

CoRR, 2012

Presentation of the SIGPLAN distinguished achievement award to Sir Charles Antony Richard Hoare, FRS, FREng, FBCS; and interview.

Andrew P. Black, Peter W. O'Hearn

Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2012

2011

Compositional Shape Analysis by Means of Bi-Abduction.

Cristiano Calcagno, Dino Distefano, Peter W. O'Hearn, Hongseok Yang

J. ACM, 2011

The Complexity of Abduction for Separated Heap Abstractions.

Nikos Gorogiannis, Max I. Kanovich, Peter W. O'Hearn

Proceedings of the Static Analysis - 18th International Symposium, 2011

Reasoning about Programs Using a Scientific Method.

Peter W. O'Hearn

Proceedings of the Formal Methods and Software Engineering, 2011

On Locality and the Exchange Law for Concurrent Processes.

C. A. R. Hoare, Akbar Hussain, Bernhard Möller, Peter W. O'Hearn, Rasmus Lerchedahl Petersen, Georg Struth

Proceedings of the CONCUR 2011 - Concurrency Theory - 22nd International Conference, 2011

Algebra, Logic, Locality, Concurrency.

Peter W. O'Hearn

Proceedings of the Programming Languages and Systems - 9th Asian Symposium, 2011

2010

Abstraction for concurrent objects.

Ivana Filipovic, Peter W. O'Hearn, Noam Rinetzky, Hongseok Yang

Theor. Comput. Sci., 2010

Blaming the client: on data refinement in the presence of pointers.

Ivana Filipovic, Peter W. O'Hearn, Noah Torp-Smith, Hongseok Yang

Formal Aspects Comput., 2010

Verifying linearizability with hindsight.

Peter W. O'Hearn, Noam Rinetzky, Martin T. Vechev, Eran Yahav, Greta Yorsh

Proceedings of the 29th Annual ACM Symposium on Principles of Distributed Computing, 2010

Abductive, Inductive and Deductive Reasoning about Resources.

Peter W. O'Hearn

Proceedings of the Computer Science Logic, 24th International Workshop, 2010

2009

Separation and information hiding.

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

ACM Trans. Program. Lang. Syst., 2009

Graphical models of separation logic.

Ian Wehrman, C. A. R. Hoare, Peter W. O'Hearn

Inf. Process. Lett., 2009

09301 Executive Summary - Typing, Analysis, and Verification of Heap-Manipulating Programs.

Mooly Sagiv, Arnd Poetzsch-Heffter, Peter W. O'Hearn

Proceedings of the Typing, Analysis and Verification of Heap-Manipulating Programs, 19.07., 2009

09301 Abstracts Collection - Typing, Analysis, and Verification of Heap-Manipulating Programs.

Mooly Sagiv, Arnd Poetzsch-Heffter, Peter W. O'Hearn

Proceedings of the Typing, Analysis and Verification of Heap-Manipulating Programs, 19.07., 2009

2008

Separation Logic Semantics for Communicating Processes.

Tony Hoare, Peter W. O'Hearn

Proceedings of the First International Conference on Foundations of Informatics, 2008

Space Invading Systems Code.

Cristiano Calcagno, Dino Distefano, Peter W. O'Hearn, Hongseok Yang

Proceedings of the Logic-Based Program Synthesis and Transformation, 2008

Separation Logic Tutorial.

Peter W. O'Hearn

Proceedings of the Logic Programming, 24th International Conference, 2008

Scalable Shape Analysis for Systems Code.

Hongseok Yang, Oukseh Lee, Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, Peter W. O'Hearn

Proceedings of the Computer Aided Verification, 20th International Conference, 2008

Tutorial on Separation Logic (Invited Tutorial).

Peter W. O'Hearn

Proceedings of the Computer Aided Verification, 20th International Conference, 2008

2007

Resources, concurrency, and local reasoning.

Peter W. O'Hearn

Theor. Comput. Sci., 2007

Preface.

Olivier Danvy, Peter W. O'Hearn, Philip Wadler

Theor. Comput. Sci., 2007

Footprint Analysis: A Shape Analysis That Discovers Preconditions.

Cristiano Calcagno, Dino Distefano, Peter W. O'Hearn, Hongseok Yang

Proceedings of the Static Analysis, 14th International Symposium, 2007

Modular verification of a non-blocking stack.

Matthew J. Parkinson, Richard Bornat, Peter W. O'Hearn

Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2007

Variance analyses from invariance analyses.

Josh Berdine, Aziem Chawdhary, Byron Cook, Dino Distefano, Peter W. O'Hearn

Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2007

Local Action and Abstract Separation Logic.

Cristiano Calcagno, Peter W. O'Hearn, Hongseok Yang

Proceedings of the 22nd IEEE Symposium on Logic in Computer Science (LICS 2007), 2007

Separation logic and concurrent resource management.

Peter W. O'Hearn

Proceedings of the 6th International Symposium on Memory Management, 2007

Shape Analysis for Composite Data Structures.

Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, Peter W. O'Hearn, Thomas Wies, Hongseok Yang

Proceedings of the Computer Aided Verification, 19th International Conference, 2007

2006

Strong Update, Disposal, and Encapsulation in Bunched Typing.

Josh Berdine, Peter W. O'Hearn

Proceedings of the 22nd Annual Conference on Mathematical Foundations of Programming Semantics, 2006

Verified Software: A Grand Challenge.

Cliff B. Jones, Peter W. O'Hearn, Jim Woodcock

Computer, 2006

A Local Shape Analysis Based on Separation Logic.

Dino Distefano, Peter W. O'Hearn, Hongseok Yang

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2006

Separation Logic and Program Analysis.

Peter W. O'Hearn

Proceedings of the Static Analysis, 13th International Symposium, 2006

Beyond Reachability: Shape Abstraction in the Presence of Pointer Arithmetic.

Cristiano Calcagno, Dino Distefano, Peter W. O'Hearn, Hongseok Yang

Proceedings of the Static Analysis, 13th International Symposium, 2006

Automatic Termination Proofs for Programs with Shape-Shifting Heaps.

Josh Berdine, Byron Cook, Dino Distefano, Peter W. O'Hearn

Proceedings of the Computer Aided Verification, 18th International Conference, 2006

2005

Scalable Specification and Reasoning: Challenges for Program Logic.

Peter W. O'Hearn

Proceedings of the Verified Software: Theories, 2005

Permission accounting in separation logic.

Richard Bornat, Cristiano Calcagno, Peter W. O'Hearn, Matthew J. Parkinson

Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2005

Smallfoot: Modular Automatic Assertion Checking with Separation Logic.

Josh Berdine, Cristiano Calcagno, Peter W. O'Hearn

Proceedings of the Formal Methods for Components and Objects, 4th International Symposium, 2005

Symbolic Execution with Separation Logic.

Josh Berdine, Cristiano Calcagno, Peter W. O'Hearn

Proceedings of the Programming Languages and Systems, Third Asian Symposium, 2005

2004

Possible worlds and resources: the semantics of BI.

David J. Pym, Peter W. O'Hearn, Hongseok Yang

Theor. Comput. Sci., 2004

Refinement and Separation Contexts.

Ivana Mijajlovic, Noah Torp-Smith, Peter W. O'Hearn

Proceedings of the FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science, 2004

A Decidable Fragment of Separation Logic.

Josh Berdine, Cristiano Calcagno, Peter W. O'Hearn

Proceedings of the FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science, 2004

Resources, Concurrency, and Local Reasoning (Abstract).

Peter W. O'Hearn

Proceedings of the Programming Languages and Systems, 2004

2003

Program logic and equivalence in the presence of garbage collection.

Cristiano Calcagno, Peter W. O'Hearn, Richard Bornat

Theor. Comput. Sci., 2003

On bunched typing.

Peter W. O'Hearn

J. Funct. Program., 2003

2002

Linear Continuation-Passing.

Josh Berdine, Peter W. O'Hearn, Uday S. Reddy, Hayo Thielecke

High. Order Symb. Comput., 2002

A Semantic Basis for Local Reasoning.

Hongseok Yang, Peter W. O'Hearn

Proceedings of the Foundations of Software Science and Computation Structures, 2002

2001

BI as an Assertion Language for Mutable Data Structures.

Samin S. Ishtiaq, Peter W. O'Hearn

Proceedings of the Conference Record of POPL 2001: The 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2001

On Garbage and Program Logic.

Cristiano Calcagno, Peter W. O'Hearn

Proceedings of the Foundations of Software Science and Computation Structures, 2001

Local Reasoning about Programs that Alter Data Structures.

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

Proceedings of the Computer Science Logic, 15th International Workshop, 2001

Computability and Complexity Results for a Spatial Assertion Language for Data Structures.

Cristiano Calcagno, Hongseok Yang, Peter W. O'Hearn

Proceedings of the Second Asian Workshop on Programming Languages and Systems, 2001

2000

From Algol to polymorphic linear lambda-calculus.

Peter W. O'Hearn, John C. Reynolds

J. ACM, 2000

Semantic analysis of pointer aliasing, allocation and disposal in Hoare logic351292.

Cristiano Calcagno, Samin S. Ishtiaq, Peter W. O'Hearn

Proceedings of the 2nd international ACM SIGPLAN conference on on Principles and practice of declarative programming, 2000

1999

Objects, Interference, and the Yoneda Embedding.

Peter W. O'Hearn, Uday S. Reddy

Theor. Comput. Sci., 1999

Syntactic Control of Interference Revisited.

Peter W. O'Hearn, John Power, Makoto Takeyama, Robert D. Tennent

Theor. Comput. Sci., 1999

Bireflectivity.

Peter J. Freyd, Peter W. O'Hearn, A. John Power, Makoto Takeyama, R. Street, Robert D. Tennent

Theor. Comput. Sci., 1999

The logic of bunched implications.

Peter W. O'Hearn, David J. Pym

Bull. Symb. Log., 1999

Resource Interpretations, Bunched Implications and the <i>alpha lambda</i>-Calculus.

Peter W. O'Hearn

Proceedings of the Typed Lambda Calculi and Applications, 4th International Conference, 1999

1998

Polymorphism, objects and abstract types.

Peter W. O'Hearn

SIGACT News, 1998

1997

An Axiomatic Approach to Binary Logical Relations with Applications to Data Refinement.

Yoshiki Kinoshita, Peter W. O'Hearn, John Power, Makoto Takeyama, Robert D. Tennent

Proceedings of the Theoretical Aspects of Computer Software, Third International Symposium, 1997

1996

Note on Algol and Conservatively Extending Functional Programming.

Peter W. O'Hearn

J. Funct. Program., 1996

1995

Kripke Logical Relations and PCF

Peter W. O'Hearn, Jon G. Riecke

Inf. Comput., July, 1995

Parametricity and Local Variables.

Peter W. O'Hearn, Robert D. Tennent

J. ACM, 1995

Bireflectivity.

Peter J. Freyd, Peter W. O'Hearn, John Power, Robert D. Tennent, Makoto Takeyama

Proceedings of the Eleventh Annual Conference on Mathematical Foundations of Programming Semantics, 1995

1994

Fully Abstract Translations and Parametric Polymorphism.

Peter W. O'Hearn, Jon G. Riecke

Proceedings of the Programming Languages and Systems, 1994

1993

Semantical Analysis of Specification Logic, 2

Peter W. O'Hearn, Robert D. Tennent

Inf. Comput., November, 1993

A Model for Syntactic Control of Interference.

Peter W. O'Hearn

Math. Struct. Comput. Sci., 1993

Relational Parametricity and Local Variables.

Peter W. O'Hearn, Robert D. Tennent

Proceedings of the Conference Record of the Twentieth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 1993

1992

Resolution Framework for Finitely-Valued First-Order Logics.

Peter W. O'Hearn, Zbigniew Stachniak

J. Symb. Comput., 1992

1991

Linear Logic and Interference Control.

Peter W. O'Hearn

Proceedings of the Category Theory and Computer Science, 1991

1989

Note on Theorem Proving Strategies for Resolution Counterparts of Non-Classical Logics.

Peter W. O'Hearn, Zbigniew Stachniak

Proceedings of the ACM-SIGSAM 1989 International Symposium on Symbolic and Algebraic Computation, 1989