| 2023 | CONCUR | A General Approach to Under-Approximate Reasoning About Concurrent Programs. | Azalea Raad, Julien Vanegue, Josh Berdine, Peter W. O'Hearn |
| 2022 | CPP | Applying formal verification to microkernel IPC at meta. | Quentin Carbonneaux, Noam Zilberstein, Christoph Klee, Peter W. O'Hearn, Francesco Zappa Nardelli |
| 2020 | CAV | 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 |
| 2020 | PLDI | Formal reasoning and the hacker way (keynote). | Peter W. O'Hearn |
| 2018 | LICS | Continuous Reasoning: Scaling the impact of formal methods. | Peter W. O'Hearn |
| 2018 | SAS | Experience Developing and Deploying Concurrency Analysis at Facebook. | Peter W. O'Hearn |
| 2018 | SCAM | From Start-ups to Scale-ups: Opportunities and Open Problems for Static and Dynamic Program Analysis. | Mark Harman, Peter W. O'Hearn |
| 2015 | LICS | From Categorical Logic to Facebook Engineering. | Peter W. O'Hearn |
| 2014 | FMCAD | Disproving termination with overapproximation. | Byron Cook, Carsten Fuhs, Kaustubh Nimkar, Peter W. O'Hearn |
| 2014 | POPL | The essence of Reynolds. | Stephen Brookes, Peter W. O'Hearn, Uday S. Reddy |
| 2014 | TACAS | Proving Nontermination via Safety. | Hong Yi Chen, Byron Cook, Carsten Fuhs, Kaustubh Nimkar, Peter W. O'Hearn |
| 2012 | POPL | 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 |
| 2011 | APLAS | Algebra, Logic, Locality, Concurrency. | Peter W. O'Hearn |
| 2011 | CONCUR | On Locality and the Exchange Law for Concurrent Processes. | C. A. R. Hoare, Akbar Hussain, Bernhard Mller, Peter W. O'Hearn, Rasmus Lerchedahl Petersen, Georg Struth |
| 2011 | CPP | Algebra, Logic, Locality, Concurrency. | Peter W. O'Hearn |
| 2011 | ICFEM | Reasoning about Programs Using a Scientific Method. | Peter W. O'Hearn |
| 2011 | SAS | The Complexity of Abduction for Separated Heap Abstractions. | Nikos Gorogiannis, Max I. Kanovich, Peter W. O'Hearn |
| 2010 | CSL | Abductive, Inductive and Deductive Reasoning about Resources. | Peter W. O'Hearn |
| 2010 | PODC | Verifying linearizability with hindsight. | Peter W. O'Hearn, Noam Rinetzky, Martin T. Vechev, Eran Yahav, Greta Yorsh |
| 2009 | ESOP | Abstraction for Concurrent Objects. | Ivana Filipovic, Peter W. O'Hearn, Noam Rinetzky, Hongseok Yang |
| 2009 | POPL | Compositional shape analysis by means of bi-abduction. | Cristiano Calcagno, Dino Distefano, Peter W. O'Hearn, Hongseok Yang |
| 2008 | CAV | Tutorial on Separation Logic (Invited Tutorial). | Peter W. O'Hearn |
| 2008 | CAV | Scalable Shape Analysis for Systems Code. | Hongseok Yang, Oukseh Lee, Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, Peter W. O'Hearn |
| 2008 | ICLP | Separation Logic Tutorial. | Peter W. O'Hearn |
| 2008 | LOPSTR | Space Invading Systems Code. | Cristiano Calcagno, Dino Distefano, Peter W. O'Hearn, Hongseok Yang |
| 2007 | CAV | Shape Analysis for Composite Data Structures. | Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, Peter W. O'Hearn, Thomas Wies, Hongseok Yang |
| 2007 | LICS | Local Action and Abstract Separation Logic. | Cristiano Calcagno, Peter W. O'Hearn, Hongseok Yang |
| 2007 | POPL | Variance analyses from invariance analyses. | Josh Berdine, Aziem Chawdhary, Byron Cook, Dino Distefano, Peter W. O'Hearn |
| 2007 | POPL | Modular verification of a non-blocking stack. | Matthew J. Parkinson, Richard Bornat, Peter W. O'Hearn |
| 2007 | SAS | Footprint Analysis: A Shape Analysis That Discovers Preconditions. | Cristiano Calcagno, Dino Distefano, Peter W. O'Hearn, Hongseok Yang |
| 2006 | CAV | Automatic Termination Proofs for Programs with Shape-Shifting Heaps. | Josh Berdine, Byron Cook, Dino Distefano, Peter W. O'Hearn |
| 2006 | SAS | Beyond Reachability: Shape Abstraction in the Presence of Pointer Arithmetic. | Cristiano Calcagno, Dino Distefano, Peter W. O'Hearn, Hongseok Yang |
| 2006 | SAS | Separation Logic and Program Analysis. | Peter W. O'Hearn |
| 2006 | TACAS | A Local Shape Analysis Based on Separation Logic. | Dino Distefano, Peter W. O'Hearn, Hongseok Yang |
| 2005 | APLAS | Symbolic Execution with Separation Logic. | Josh Berdine, Cristiano Calcagno, Peter W. O'Hearn |
| 2005 | POPL | Permission accounting in separation logic. | Richard Bornat, Cristiano Calcagno, Peter W. O'Hearn, Matthew J. Parkinson |
| 2004 | CONCUR | Resources, Concurrency and Local Reasoning. | Peter W. O'Hearn |
| 2004 | ESOP | Resources, Concurrency, and Local Reasoning (Abstract). | Peter W. O'Hearn |
| 2004 | POPL | Separation and information hiding. | Peter W. O'Hearn, Hongseok Yang, John C. Reynolds |
| 2002 | FOSSACS | A Semantic Basis for Local Reasoning. | Hongseok Yang, Peter W. O'Hearn |
| 2001 | APLAS | Computability and Complexity Results for a Spatial Assertion Language for Data Structures. | Cristiano Calcagno, Hongseok Yang, Peter W. O'Hearn |
| 2001 | CSL | Local Reasoning about Programs that Alter Data Structures. | Peter W. O'Hearn, John C. Reynolds, Hongseok Yang |
| 2001 | FOSSACS | On Garbage and Program Logic. | Cristiano Calcagno, Peter W. O'Hearn |
| 2001 | POPL | BI as an Assertion Language for Mutable Data Structures. | Samin S. Ishtiaq, Peter W. O'Hearn |
| 2000 | PPDP | Semantic analysis of pointer aliasing, allocation and disposal in Hoare logic351292. | Cristiano Calcagno, Samin S. Ishtiaq, Peter W. O'Hearn |
| 1994 | ESOP | Fully Abstract Translations and Parametric Polymorphism. | Peter W. O'Hearn, Jon G. Riecke |
| 1993 | POPL | Relational Parametricity and Local Variables. | Peter W. O'Hearn, Robert D. Tennent |
| 1989 | ISSAC | Note on Theorem Proving Strategies for Resolution Counterparts of Non-Classical Logics. | Peter W. O'Hearn, Zbigniew Stachniak |