default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDPeter W. O'Hearn
Person information
- affiliation: Facebook Research
- affiliation (former): University College London, UK
- affiliation (former): Queen Mary University of London, UK
- award: Gödel Prize
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
showing all ?? records
2020 – today
- 2024
[j35]Azalea Raad
, Julien Vanegue, Peter W. O'Hearn:
Non-termination Proving at Scale. Proc. ACM Program. Lang. 8(OOPSLA2): 246-274 (2024)- 2023
- [c66]Azalea Raad, Julien Vanegue, Josh Berdine, Peter W. O'Hearn:
A General Approach to Under-Approximate Reasoning About Concurrent Programs. CONCUR 2023: 25:1-25:17 - 2022
- [j34]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(OOPSLA1): 1-27 (2022) - [j33]Azalea Raad, Josh Berdine, Derek Dreyer, Peter W. O'Hearn:
Concurrent incorrectness separation logic. Proc. ACM Program. Lang. 6(POPL): 1-29 (2022) - [c65]Quentin Carbonneaux, Noam Zilberstein, Christoph Klee, Peter W. O'Hearn, Francesco Zappa Nardelli:
Applying formal verification to microkernel IPC at meta. CPP 2022: 116-129 - 2021
- [c64]Bernhard Möller, Peter W. O'Hearn, Tony Hoare:
On Algebra of Program Correctness and Incorrectness. RAMiCS 2021: 325-343 - 2020
- [j32]Peter W. O'Hearn:
Incorrectness logic. Proc. ACM Program. Lang. 4(POPL): 10:1-10:32 (2020) - [c63]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: 225-252 - [c62]Peter W. O'Hearn:
Formal reasoning and the hacker way (keynote). SOAP@PLDI 2020: 1
2010 – 2019
- 2019
- [j31]Peter W. O'Hearn:
Separation logic. Commun. ACM 62(2): 86-95 (2019) - [j30]Dino Distefano, Manuel Fähndrich, Francesco Logozzo, Peter W. O'Hearn:
Scaling static analyses at Facebook. Commun. ACM 62(8): 62-70 (2019) - [j29]Nikos Gorogiannis, Peter W. O'Hearn, Ilya Sergey:
A true positives theorem for a static race detector. Proc. ACM Program. Lang. 3(POPL): 57:1-57:29 (2019) - 2018
- [j28]Sam Blackshear, Nikos Gorogiannis, Peter W. O'Hearn, Ilya Sergey:
RacerD: compositional static race detection. Proc. ACM Program. Lang. 2(OOPSLA): 144:1-144:28 (2018) - [c61]Peter W. O'Hearn:
Continuous Reasoning: Scaling the impact of formal methods. LICS 2018: 13-25 - [c60]Peter W. O'Hearn:
Experience Developing and Deploying Concurrency Analysis at Facebook. SAS 2018: 56-70 - [c59]Mark Harman, Peter W. O'Hearn:
From Start-ups to Scale-ups: Opportunities and Open Problems for Static and Dynamic Program Analysis. SCAM 2018: 1-23 - [i5]Nikos Gorogiannis, Peter W. O'Hearn, Ilya Sergey:
A True Positives Theorem for a Static Race Detector - Extended Version. CoRR abs/1811.03503 (2018) - 2016
- [j27]Stephen Brookes, Peter W. O'Hearn:
Concurrent separation logic. ACM SIGLOG News 3(3): 47-65 (2016) - 2015
- [j26]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): 285-302 (2015) - [c58]Peter W. O'Hearn:
From Categorical Logic to Facebook Engineering. LICS 2015: 17-20 - [c57]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: 3-11 - [i4]Byron Cook, Carsten Fuhs, Kaustubh Nimkar, Peter W. O'Hearn:
Embracing Overapproximation for Proving Nontermination. Adv. Math. Commun. 3 (2015) - 2014
- [j25]Stephen Brookes, Peter W. O'Hearn, Uday S. Reddy:
The Essence of Reynolds. Formal Aspects Comput. 26(3): 435-439 (2014) - [c56]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: 1-18 - [c55]Byron Cook, Carsten Fuhs, Kaustubh Nimkar, Peter W. O'Hearn:
Disproving termination with overapproximation. FMCAD 2014: 67-74 - [c54]Stephen Brookes, Peter W. O'Hearn, Uday S. Reddy:
The essence of Reynolds. POPL 2014: 251-256 - [c53]Hong Yi Chen, Byron Cook, Carsten Fuhs, Kaustubh Nimkar, Peter W. O'Hearn:
Proving Nontermination via Safety. TACAS 2014: 156-171 - 2012
- [c52]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: 1-2 - [p1]Peter W. O'Hearn:
A Primer on Separation Logic (and Automatic Program Verification and Analysis). Software Safety and Security 2012: 286-318 - [i3]Josh Berdine, Cristiano Calcagno, Peter W. O'Hearn:
Verification Condition Generation and Variable Conditions in Smallfoot. CoRR abs/1204.4804 (2012) - 2011
- [j24]Cristiano Calcagno, Dino Distefano, Peter W. O'Hearn, Hongseok Yang:
Compositional Shape Analysis by Means of Bi-Abduction. J. ACM 58(6): 26:1-26:66 (2011) - [c51]Peter W. O'Hearn:
Algebra, Logic, Locality, Concurrency. APLAS 2011: 17-18 - [c50]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: 250-264 - [c49]Peter W. O'Hearn:
Algebra, Logic, Locality, Concurrency. CPP 2011: 3-4 - [c48]Peter W. O'Hearn:
Reasoning about Programs Using a Scientific Method. ICFEM 2011: 14 - [c47]Nikos Gorogiannis, Max I. Kanovich, Peter W. O'Hearn:
The Complexity of Abduction for Separated Heap Abstractions. SAS 2011: 25-42 - 2010
- [j23]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): 547-583 (2010) - [j22]Ivana Filipovic, Peter W. O'Hearn, Noam Rinetzky, Hongseok Yang:
Abstraction for concurrent objects. Theor. Comput. Sci. 411(51-52): 4379-4398 (2010) - [c46]Peter W. O'Hearn:
Abductive, Inductive and Deductive Reasoning about Resources. CSL 2010: 49-50 - [c45]Peter W. O'Hearn, Noam Rinetzky, Martin T. Vechev, Eran Yahav, Greta Yorsh:
Verifying linearizability with hindsight. PODC 2010: 85-94 - [e2]Gary T. Leavens, Peter W. O'Hearn, Sriram K. Rajamani:
Verified Software: Theories, Tools, Experiments, Third International Conference, VSTTE 2010, Edinburgh, UK, August 16-19, 2010. Proceedings. Lecture Notes in Computer Science 6217, Springer 2010, ISBN 978-3-642-15056-2 [contents]
2000 – 2009
- 2009
- [j21]Ian Wehrman, C. A. R. Hoare, Peter W. O'Hearn:
Graphical models of separation logic. Inf. Process. Lett. 109(17): 1001-1004 (2009) - [j20]Peter W. O'Hearn, Hongseok Yang, John C. Reynolds:
Separation and information hiding. ACM Trans. Program. Lang. Syst. 31(3): 11:1-11:50 (2009) - [c44]Ivana Filipovic, Peter W. O'Hearn, Noam Rinetzky, Hongseok Yang:
Abstraction for Concurrent Objects. ESOP 2009: 252-266 - [c43]Cristiano Calcagno, Dino Distefano, Peter W. O'Hearn, Hongseok Yang:
Compositional shape analysis by means of bi-abduction. POPL 2009: 289-300 - [e1]Peter W. O'Hearn, Arnd Poetzsch-Heffter, Mooly Sagiv:
Typing, Analysis and Verification of Heap-Manipulating Programs, 19.07. - 24.07.2009. Dagstuhl Seminar Proceedings 09301, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Germany 2009 [contents] - [i2]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 - [i1]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 - 2008
- [c42]Peter W. O'Hearn:
Tutorial on Separation Logic (Invited Tutorial). CAV 2008: 19-21 - [c41]Hongseok Yang, Oukseh Lee, Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, Peter W. O'Hearn:
Scalable Shape Analysis for Systems Code. CAV 2008: 385-398 - [c40]Peter W. O'Hearn:
Separation Logic Tutorial. ICLP 2008: 15-21 - [c39]Cristiano Calcagno, Dino Distefano, Peter W. O'Hearn, Hongseok Yang:
Space Invading Systems Code. LOPSTR 2008: 1-3 - [c38]Tony Hoare, Peter W. O'Hearn:
Separation Logic Semantics for Communicating Processes. FICS 2008: 3-25 - 2007
- [j19]Olivier Danvy, Peter W. O'Hearn, Philip Wadler:
Preface. Theor. Comput. Sci. 375(1-3): 1-2 (2007) - [j18]Peter W. O'Hearn:
Resources, concurrency, and local reasoning. Theor. Comput. Sci. 375(1-3): 271-307 (2007) - [c37]Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, Peter W. O'Hearn, Thomas Wies, Hongseok Yang:
Shape Analysis for Composite Data Structures. CAV 2007: 178-192 - [c36]Peter W. O'Hearn:
Separation logic and concurrent resource management. ISMM 2007: 1 - [c35]Cristiano Calcagno, Peter W. O'Hearn, Hongseok Yang:
Local Action and Abstract Separation Logic. LICS 2007: 366-378 - [c34]Josh Berdine, Aziem Chawdhary, Byron Cook, Dino Distefano, Peter W. O'Hearn:
Variance analyses from invariance analyses. POPL 2007: 211-224 - [c33]Matthew J. Parkinson, Richard Bornat, Peter W. O'Hearn:
Modular verification of a non-blocking stack. POPL 2007: 297-302 - [c32]Cristiano Calcagno, Dino Distefano, Peter W. O'Hearn, Hongseok Yang:
Footprint Analysis: A Shape Analysis That Discovers Preconditions. SAS 2007: 402-418 - 2006
- [j17]Cliff B. Jones, Peter W. O'Hearn, Jim Woodcock:
Verified Software: A Grand Challenge. Computer 39(4): 93-95 (2006) - [c31]Josh Berdine, Byron Cook, Dino Distefano, Peter W. O'Hearn:
Automatic Termination Proofs for Programs with Shape-Shifting Heaps. CAV 2006: 386-400 - [c30]Peter W. O'Hearn:
Separation Logic and Program Analysis. SAS 2006: 181 - [c29]Cristiano Calcagno, Dino Distefano, Peter W. O'Hearn, Hongseok Yang:
Beyond Reachability: Shape Abstraction in the Presence of Pointer Arithmetic. SAS 2006: 182-203 - [c28]Dino Distefano, Peter W. O'Hearn, Hongseok Yang:
A Local Shape Analysis Based on Separation Logic. TACAS 2006: 287-302 - [c27]Josh Berdine, Peter W. O'Hearn:
Strong Update, Disposal, and Encapsulation in Bunched Typing. MFPS 2006: 81-98 - 2005
- [c26]Josh Berdine, Cristiano Calcagno, Peter W. O'Hearn:
Symbolic Execution with Separation Logic. APLAS 2005: 52-68 - [c25]Josh Berdine, Cristiano Calcagno, Peter W. O'Hearn:
Smallfoot: Modular Automatic Assertion Checking with Separation Logic. FMCO 2005: 115-137 - [c24]Richard Bornat, Cristiano Calcagno, Peter W. O'Hearn, Matthew J. Parkinson:
Permission accounting in separation logic. POPL 2005: 259-270 - [c23]Peter W. O'Hearn:
Scalable Specification and Reasoning: Challenges for Program Logic. VSTTE 2005: 116-133 - 2004
- [j16]David J. Pym, Peter W. O'Hearn, Hongseok Yang:
Possible worlds and resources: the semantics of BI. Theor. Comput. Sci. 315(1): 257-305 (2004) - [c22]Peter W. O'Hearn:
Resources, Concurrency and Local Reasoning. CONCUR 2004: 49-67 - [c21]Peter W. O'Hearn:
Resources, Concurrency, and Local Reasoning (Abstract). ESOP 2004: 1-2 - [c20]Josh Berdine, Cristiano Calcagno, Peter W. O'Hearn:
A Decidable Fragment of Separation Logic. FSTTCS 2004: 97-109 - [c19]Ivana Mijajlovic, Noah Torp-Smith, Peter W. O'Hearn:
Refinement and Separation Contexts. FSTTCS 2004: 421-433 - [c18]Peter W. O'Hearn, Hongseok Yang, John C. Reynolds:
Separation and information hiding. POPL 2004: 268-280 - 2003
- [j15]Peter W. O'Hearn:
On bunched typing. J. Funct. Program. 13(4): 747-796 (2003) - [j14]Cristiano Calcagno, Peter W. O'Hearn, Richard Bornat:
Program logic and equivalence in the presence of garbage collection. Theor. Comput. Sci. 298(3): 557-581 (2003) - 2002
- [j13]Josh Berdine, Peter W. O'Hearn, Uday S. Reddy, Hayo Thielecke:
Linear Continuation-Passing. High. Order Symb. Comput. 15(2-3): 181-208 (2002) - [c17]Hongseok Yang, Peter W. O'Hearn:
A Semantic Basis for Local Reasoning. FoSSaCS 2002: 402-416 - 2001
- [c16]Cristiano Calcagno, Hongseok Yang, Peter W. O'Hearn:
Computability and Complexity Results for a Spatial Assertion Language for Data Structures. APLAS 2001: 289-300 - [c15]Peter W. O'Hearn, John C. Reynolds, Hongseok Yang:
Local Reasoning about Programs that Alter Data Structures. CSL 2001: 1-19 - [c14]Cristiano Calcagno, Peter W. O'Hearn:
On Garbage and Program Logic. FoSSaCS 2001: 137-151 - [c13]Cristiano Calcagno, Hongseok Yang, Peter W. O'Hearn:
Computability and Complexity Results for a Spatial Assertion Language for Data Structures. FSTTCS 2001: 108-119 - [c12]Samin S. Ishtiaq, Peter W. O'Hearn:
BI as an Assertion Language for Mutable Data Structures. POPL 2001: 14-26 - 2000
- [j12]Peter W. O'Hearn, John C. Reynolds:
From Algol to polymorphic linear lambda-calculus. J. ACM 47(1): 167-223 (2000) - [c11]Cristiano Calcagno, Samin S. Ishtiaq, Peter W. O'Hearn:
Semantic analysis of pointer aliasing, allocation and disposal in Hoare logic351292. PPDP 2000: 190-201
1990 – 1999
- 1999
- [j11]Peter W. O'Hearn, David J. Pym:
The logic of bunched implications. Bull. Symb. Log. 5(2): 215-244 (1999) - [j10]Peter J. Freyd, Peter W. O'Hearn, A. John Power, Makoto Takeyama, R. Street, Robert D. Tennent:
Bireflectivity. Theor. Comput. Sci. 228(1-2): 49-76 (1999) - [j9]Peter W. O'Hearn, John Power, Makoto Takeyama, Robert D. Tennent:
Syntactic Control of Interference Revisited. Theor. Comput. Sci. 228(1-2): 211-252 (1999) - [j8]Peter W. O'Hearn, Uday S. Reddy:
Objects, Interference, and the Yoneda Embedding. Theor. Comput. Sci. 228(1-2): 253-282 (1999) - [c10]Peter W. O'Hearn:
Resource Interpretations, Bunched Implications and the alpha lambda-Calculus. TLCA 1999: 258-279 - 1998
- [j7]Peter W. O'Hearn:
Polymorphism, objects and abstract types. SIGACT News 29(4): 39-50 (1998) - 1997
- [c9]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: 191-212 - 1996
- [j6]Peter W. O'Hearn:
Note on Algol and Conservatively Extending Functional Programming. J. Funct. Program. 6(1): 171-180 (1996) - 1995
- [j5]Peter W. O'Hearn, Jon G. Riecke:
Kripke Logical Relations and PCF. Inf. Comput. 120(1): 107-116 (1995) - [j4]Peter W. O'Hearn, Robert D. Tennent:
Parametricity and Local Variables. J. ACM 42(3): 658-709 (1995) - [c8]Peter J. Freyd, Peter W. O'Hearn, John Power, Robert D. Tennent, Makoto Takeyama:
Bireflectivity. MFPS 1995: 199-213 - [c7]Peter W. O'Hearn, John Power, Robert D. Tennent, Makoto Takeyama:
Syntactic control of interference revisited. MFPS 1995: 447-486 - [c6]Peter W. O'Hearn, Uday S. Reddy:
Objects, interference and the Yoneda embedding. MFPS 1995: 487-514 - 1994
- [c5]Peter W. O'Hearn, Jon G. Riecke:
Fully Abstract Translations and Parametric Polymorphism. ESOP 1994: 454-468 - 1993
- [j3]Peter W. O'Hearn, Robert D. Tennent:
Semantical Analysis of Specification Logic, 2. Inf. Comput. 107(1): 25-57 (1993) - [j2]Peter W. O'Hearn:
A Model for Syntactic Control of Interference. Math. Struct. Comput. Sci. 3(4): 435-465 (1993) - [c4]Peter W. O'Hearn, Robert D. Tennent:
Relational Parametricity and Local Variables. POPL 1993: 171-184 - 1992
- [j1]Peter W. O'Hearn, Zbigniew Stachniak:
Resolution Framework for Finitely-Valued First-Order Logics. J. Symb. Comput. 13(3): 235-254 (1992) - 1991
- [c3]Peter W. O'Hearn:
Linear Logic and Interference Control. Category Theory and Computer Science 1991: 74-93
1980 – 1989
- 1989
- [c2]Peter W. O'Hearn, Zbigniew Stachniak:
Note on Theorem Proving Strategies for Resolution Counterparts of Non-Classical Logics. ISSAC 1989: 364-372 - [c1]Peter W. O'Hearn, Zbigniew Stachniak:
A Resolution Framework for Finitely-Valued First-Order Logics. SCAI 1989: 69-81
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from 
to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the 
of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from 
, 
, and 
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from 
.
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-12-12 21:57 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
