Peter W. O'Hearn

116 papers A* 17A 5B 24C 7Journal 44Unranked 16

Year	Rank	Type	Title / Venue / Authors
2026	J	`jnl`	LLMs versus the Halting Problem: Revisiting Program Termination Prediction. CoRR Oren Sultan, Jordi Armengol-Estapé, Pascal Kesseli, Julien Vanegue, Dafna Shahaf, Yossi Adi, Peter W. O'Hearn
2026	J	`jnl`	WybeCoder: Verified Imperative Code Generation. CoRR Fabian Gloeckle, Mantas Baksys, Darius Feher, Kunhao Zheng, Amaury Hayat, Sean B. Holden, Gabriel Synnaeve, Peter W. O'Hearn
2025	J	`jnl`	CWM: An Open-Weights LLM for Research on Code Generation with World Models. CoRR FAIR CodeGen team, Jade Copet, Quentin Carbonneaux, Gal Cohen, Jonas Gehring, Jacob Kahn, Jannik Kossen, Felix Kreuk, Emily McMilin, Michel Meyer, Yuxiang Wei, David Zhang, Kunhao Zheng, Jordi Armengol-Estapé, Pedram Bashiri, Maximilian Beck, Pierre Chambon, Abhishek Charnalia, Chris Cummins, Juliette Decugis, Zacharias V. Fisches, François Fleuret, Fabian Gloeckle, Alex Gu, Michael Hassid, Daniel Haziza, Badr Youbi Idrissi, Christian Keller, Rahul Kindi, Hugh Leather, Gallil Maimon, Aram H. Markosyan, Francisco Massa, Pierre-Emmanuel Mazaré, Vegard Mella, Naila Murray, Keyur Muzumdar, Peter W. O'Hearn, Matteo Pagliardini, Dmitrii Pedchenko, Tal Remez, Volker Seeker, Marco Selvi, Oren Sultan, Sida Wang, Luca Wehrstedt, Ori Yoran, Lingming Zhang, Taco Cohen, Yossi Adi, Gabriel Synnaeve
2025	—	`conf`	Harden and Catch for Just-in-Time Assured LLM-Based Software Testing: Open Research Challenges. SIGSOFT FSE Companion Mark Harman, Peter W. O'Hearn, Shubho Sengupta
2025	J	`jnl`	Harden and Catch for Just-in-Time Assured LLM-Based Software Testing: Open Research Challenges. CoRR Mark Harman, Peter W. O'Hearn, Shubho Sengupta
2025	J	`jnl`	Logic.py: Bridging the Gap between LLMs and Constraint Solvers. CoRR Pascal Kesseli, Peter W. O'Hearn, Ricardo Silveira Cabral
2025	J	`jnl`	Non-Termination Proving: 100 Million LoC and Beyond. CoRR Julien Vanegue, Jules Villard, Peter W. O'Hearn, Azalea Raad
2024	J	`jnl`	Non-termination Proving at Scale. Proc. ACM Program. Lang. Azalea Raad, Julien Vanegue, Peter W. O'Hearn
2023	B	`conf`	A General Approach to Under-Approximate Reasoning About Concurrent Programs. CONCUR Azalea Raad, Julien Vanegue, Josh Berdine, Peter W. O'Hearn
2022	B	`conf`	Applying formal verification to microkernel IPC at meta. CPP Quentin Carbonneaux, Noam Zilberstein, Christoph Klee, Peter W. O'Hearn, Francesco Zappa Nardelli
2022	J	`jnl`	Concurrent incorrectness separation logic. Proc. ACM Program. Lang. Azalea Raad, Josh Berdine, Derek Dreyer, Peter W. O'Hearn
2022	J	`jnl`	Finding real bugs in big programs with incorrectness logic. Proc. ACM Program. Lang. Quang Loc Le, Azalea Raad, Jules Villard, Josh Berdine, Derek Dreyer, Peter W. O'Hearn
2021	C	`conf`	On Algebra of Program Correctness and Incorrectness. RAMiCS Bernhard Möller, Peter W. O'Hearn, Tony Hoare
2020	—	`conf`	Formal reasoning and the hacker way (keynote). SOAP@PLDI Peter W. O'Hearn
2020	J	`jnl`	Incorrectness logic. Proc. ACM Program. Lang. Peter W. O'Hearn
2020	—	`conf`	Local Reasoning About the Presence of Bugs: Incorrectness Separation Logic. CAV (2) Azalea Raad, Josh Berdine, Hoang-Hai Dang, Derek Dreyer, Peter W. O'Hearn, Jules Villard
2019	J	`jnl`	A true positives theorem for a static race detector. Proc. ACM Program. Lang. Nikos Gorogiannis, Peter W. O'Hearn, Ilya Sergey
2019	J	`jnl`	Scaling static analyses at Facebook. Commun. ACM Dino Distefano, Manuel Fähndrich, Francesco Logozzo, Peter W. O'Hearn
2019	J	`jnl`	Separation logic. Commun. ACM Peter W. O'Hearn
2018	J	`jnl`	A True Positives Theorem for a Static Race Detector - Extended Version. CoRR Nikos Gorogiannis, Peter W. O'Hearn, Ilya Sergey
2018	A*	`conf`	Continuous Reasoning: Scaling the impact of formal methods. LICS Peter W. O'Hearn
2018	B	`conf`	Experience Developing and Deploying Concurrency Analysis at Facebook. SAS Peter W. O'Hearn
2018	C	`conf`	From Start-ups to Scale-ups: Opportunities and Open Problems for Static and Dynamic Program Analysis. SCAM Mark Harman, Peter W. O'Hearn
2018	J	`jnl`	RacerD: compositional static race detection. Proc. ACM Program. Lang. Sam Blackshear, Nikos Gorogiannis, Peter W. O'Hearn, Ilya Sergey
2016	J	`jnl`	Concurrent separation logic. ACM SIGLOG News Stephen Brookes, Peter W. O'Hearn
2015	J	`jnl`	Embracing Overapproximation for Proving Nontermination. Tiny Trans. Comput. Sci. Byron Cook, Carsten Fuhs, Kaustubh Nimkar, Peter W. O'Hearn
2015	A*	`conf`	From Categorical Logic to Facebook Engineering. LICS Peter W. O'Hearn
2015	—	`conf`	Moving Fast with Software Verification. NFM Cristiano Calcagno, Dino Distefano, Jérémy Dubreil, Dominik Gabi, Pieter Hooimeijer, Martino Luca, Peter W. O'Hearn, Irene Papakonstantinou, Jim Purbrick, Dulma Rodriguez
2015	J	`jnl`	On the relation between Concurrent Separation Logic and Concurrent Kleene Algebra. J. Log. Algebraic Methods Program. Peter W. O'Hearn, Rasmus Lerchedahl Petersen, Jules Villard, Akbar Hussain
2014	C	`conf`	Developments in Concurrent Kleene Algebra. RAMiCS Tony Hoare, Stephan van Staden, Bernhard Möller, Georg Struth, Jules Villard, Huibiao Zhu, Peter W. O'Hearn
2014	B	`conf`	Disproving termination with overapproximation. FMCAD Byron Cook, Carsten Fuhs, Kaustubh Nimkar, Peter W. O'Hearn
2014	A	`conf`	Proving Nontermination via Safety. TACAS Hong Yi Chen, Byron Cook, Carsten Fuhs, Kaustubh Nimkar, Peter W. O'Hearn
2014	J	`jnl`	The Essence of Reynolds. Formal Aspects Comput. Stephen Brookes, Peter W. O'Hearn, Uday S. Reddy
2014	A*	`conf`	The essence of Reynolds. POPL Stephen Brookes, Peter W. O'Hearn, Uday S. Reddy
2012	—	`ch.`	A Primer on Separation Logic (and Automatic Program Verification and Analysis). Software Safety and Security Peter W. O'Hearn
2012	A*	`conf`	Presentation of the SIGPLAN distinguished achievement award to Sir Charles Antony Richard Hoare, FRS, FREng, FBCS; and interview. POPL Andrew P. Black, Peter W. O'Hearn
2012	J	`jnl`	Verification Condition Generation and Variable Conditions in Smallfoot CoRR Josh Berdine, Cristiano Calcagno, Peter W. O'Hearn
2011	B	`conf`	Algebra, Logic, Locality, Concurrency. APLAS Peter W. O'Hearn
2011	B	`conf`	Algebra, Logic, Locality, Concurrency. CPP Peter W. O'Hearn
2011	J	`jnl`	Compositional Shape Analysis by Means of Bi-Abduction. J. ACM Cristiano Calcagno, Dino Distefano, Peter W. O'Hearn, Hongseok Yang
2011	B	`conf`	On Locality and the Exchange Law for Concurrent Processes. CONCUR C. A. R. Hoare, Akbar Hussain, Bernhard Möller, Peter W. O'Hearn, Rasmus Lerchedahl Petersen, Georg Struth
2011	C	`conf`	Reasoning about Programs Using a Scientific Method. ICFEM Peter W. O'Hearn
2011	B	`conf`	The Complexity of Abduction for Separated Heap Abstractions. SAS Nikos Gorogiannis, Max I. Kanovich, Peter W. O'Hearn
2010	B	`conf`	Abductive, Inductive and Deductive Reasoning about Resources. CSL Peter W. O'Hearn
2010	J	`jnl`	Abstraction for concurrent objects. Theor. Comput. Sci. Ivana Filipovic, Peter W. O'Hearn, Noam Rinetzky, Hongseok Yang
2010	J	`jnl`	Blaming the client: on data refinement in the presence of pointers. Formal Aspects Comput. Ivana Filipovic, Peter W. O'Hearn, Noah Torp-Smith, Hongseok Yang
2010	—	`ed.`	Verified Software: Theories, Tools, Experiments, Third International Conference, VSTTE 2010, Edinburgh, UK, August 16-19, 2010. Proceedings VSTTE Gary T. Leavens, Peter W. O'Hearn, Sriram K. Rajamani
2010	A*	`conf`	Verifying linearizability with hindsight. PODC Peter W. O'Hearn, Noam Rinetzky, Martin T. Vechev, Eran Yahav, Greta Yorsh
2009	—	`conf`	09301 Abstracts Collection - Typing, Analysis, and Verification of Heap-Manipulating Programs. Typing, Analysis and Verification of Heap-Manipulating Programs Mooly Sagiv, Arnd Poetzsch-Heffter, Peter W. O'Hearn
2009	—	`conf`	09301 Executive Summary - Typing, Analysis, and Verification of Heap-Manipulating Programs. Typing, Analysis and Verification of Heap-Manipulating Programs Mooly Sagiv, Arnd Poetzsch-Heffter, Peter W. O'Hearn
2009	A	`conf`	Abstraction for Concurrent Objects. ESOP Ivana Filipovic, Peter W. O'Hearn, Noam Rinetzky, Hongseok Yang
2009	A*	`conf`	Compositional shape analysis by means of bi-abduction. POPL Cristiano Calcagno, Dino Distefano, Peter W. O'Hearn, Hongseok Yang
2009	J	`jnl`	Graphical models of separation logic. Inf. Process. Lett. Ian Wehrman, C. A. R. Hoare, Peter W. O'Hearn
2009	J	`jnl`	Separation and information hiding. ACM Trans. Program. Lang. Syst. Peter W. O'Hearn, Hongseok Yang, John C. Reynolds
2009	—	`ed.`	Typing, Analysis and Verification of Heap-Manipulating Programs, 19.07. - 24.07.2009 Typing, Analysis and Verification of Heap-Manipulating Programs Peter W. O'Hearn, Arnd Poetzsch-Heffter, Mooly Sagiv
2008	A*	`conf`	Scalable Shape Analysis for Systems Code. CAV Hongseok Yang, Oukseh Lee, Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, Peter W. O'Hearn
2008	—	`conf`	Separation Logic Semantics for Communicating Processes. FICS Tony Hoare, Peter W. O'Hearn
2008	B	`conf`	Separation Logic Tutorial. ICLP Peter W. O'Hearn
2008	C	`conf`	Space Invading Systems Code. LOPSTR Cristiano Calcagno, Dino Distefano, Peter W. O'Hearn, Hongseok Yang
2008	A*	`conf`	Tutorial on Separation Logic (Invited Tutorial). CAV Peter W. O'Hearn
2007	B	`conf`	Footprint Analysis: A Shape Analysis That Discovers Preconditions. SAS Cristiano Calcagno, Dino Distefano, Peter W. O'Hearn, Hongseok Yang
2007	A*	`conf`	Local Action and Abstract Separation Logic. LICS Cristiano Calcagno, Peter W. O'Hearn, Hongseok Yang
2007	A*	`conf`	Modular verification of a non-blocking stack. POPL Matthew J. Parkinson, Richard Bornat, Peter W. O'Hearn
2007	J	`jnl`	Preface. Theor. Comput. Sci. Olivier Danvy, Peter W. O'Hearn, Philip Wadler
2007	J	`jnl`	Resources, concurrency, and local reasoning. Theor. Comput. Sci. Peter W. O'Hearn
2007	C	`conf`	Separation logic and concurrent resource management. ISMM Peter W. O'Hearn
2007	A*	`conf`	Shape Analysis for Composite Data Structures. CAV Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, Peter W. O'Hearn, Thomas Wies, Hongseok Yang
2007	A*	`conf`	Variance analyses from invariance analyses. POPL Josh Berdine, Aziem Chawdhary, Byron Cook, Dino Distefano, Peter W. O'Hearn
2006	A	`conf`	A Local Shape Analysis Based on Separation Logic. TACAS Dino Distefano, Peter W. O'Hearn, Hongseok Yang
2006	A*	`conf`	Automatic Termination Proofs for Programs with Shape-Shifting Heaps. CAV Josh Berdine, Byron Cook, Dino Distefano, Peter W. O'Hearn
2006	B	`conf`	Beyond Reachability: Shape Abstraction in the Presence of Pointer Arithmetic. SAS Cristiano Calcagno, Dino Distefano, Peter W. O'Hearn, Hongseok Yang
2006	B	`conf`	Separation Logic and Program Analysis. SAS Peter W. O'Hearn
2006	B	`conf`	Strong Update, Disposal, and Encapsulation in Bunched Typing. MFPS Josh Berdine, Peter W. O'Hearn
2006	J	`jnl`	Verified Software: A Grand Challenge. Computer Cliff B. Jones, Peter W. O'Hearn, Jim Woodcock
2005	A*	`conf`	Permission accounting in separation logic. POPL Richard Bornat, Cristiano Calcagno, Peter W. O'Hearn, Matthew J. Parkinson
2005	—	`conf`	Scalable Specification and Reasoning: Challenges for Program Logic. VSTTE Peter W. O'Hearn
2005	—	`conf`	Smallfoot: Modular Automatic Assertion Checking with Separation Logic. FMCO Josh Berdine, Cristiano Calcagno, Peter W. O'Hearn
2005	B	`conf`	Symbolic Execution with Separation Logic. APLAS Josh Berdine, Cristiano Calcagno, Peter W. O'Hearn
2004	—	`conf`	A Decidable Fragment of Separation Logic. FSTTCS Josh Berdine, Cristiano Calcagno, Peter W. O'Hearn
2004	J	`jnl`	Possible worlds and resources: the semantics of BI. Theor. Comput. Sci. David J. Pym, Peter W. O'Hearn, Hongseok Yang
2004	—	`conf`	Refinement and Separation Contexts. FSTTCS Ivana Mijajlovic, Noah Torp-Smith, Peter W. O'Hearn
2004	B	`conf`	Resources, Concurrency and Local Reasoning. CONCUR Peter W. O'Hearn
2004	A	`conf`	Resources, Concurrency, and Local Reasoning (Abstract). ESOP Peter W. O'Hearn
2004	A*	`conf`	Separation and information hiding. POPL Peter W. O'Hearn, Hongseok Yang, John C. Reynolds
2003	J	`jnl`	On bunched typing. J. Funct. Program. Peter W. O'Hearn
2003	J	`jnl`	Program logic and equivalence in the presence of garbage collection. Theor. Comput. Sci. Cristiano Calcagno, Peter W. O'Hearn, Richard Bornat
2002	B	`conf`	A Semantic Basis for Local Reasoning. FoSSaCS Hongseok Yang, Peter W. O'Hearn
2002	J	`jnl`	Linear Continuation-Passing. High. Order Symb. Comput. Josh Berdine, Peter W. O'Hearn, Uday S. Reddy, Hayo Thielecke
2001	A*	`conf`	BI as an Assertion Language for Mutable Data Structures. POPL Samin S. Ishtiaq, Peter W. O'Hearn
2001	B	`conf`	Computability and Complexity Results for a Spatial Assertion Language for Data Structures. APLAS Cristiano Calcagno, Hongseok Yang, Peter W. O'Hearn
2001	—	`conf`	Computability and Complexity Results for a Spatial Assertion Language for Data Structures. FSTTCS Cristiano Calcagno, Hongseok Yang, Peter W. O'Hearn
2001	B	`conf`	Local Reasoning about Programs that Alter Data Structures. CSL Peter W. O'Hearn, John C. Reynolds, Hongseok Yang
2001	B	`conf`	On Garbage and Program Logic. FoSSaCS Cristiano Calcagno, Peter W. O'Hearn
2000	J	`jnl`	From Algol to polymorphic linear lambda-calculus. J. ACM Peter W. O'Hearn, John C. Reynolds
2000	C	`conf`	Semantic analysis of pointer aliasing, allocation and disposal in Hoare logic351292. PPDP Cristiano Calcagno, Samin S. Ishtiaq, Peter W. O'Hearn
1999	J	`jnl`	Bireflectivity. Theor. Comput. Sci. Peter J. Freyd, Peter W. O'Hearn, A. John Power, Makoto Takeyama, R. Street, Robert D. Tennent
1999	J	`jnl`	Objects, Interference, and the Yoneda Embedding. Theor. Comput. Sci. Peter W. O'Hearn, Uday S. Reddy
1999	—	`conf`	Resource Interpretations, Bunched Implications and the TLCA Peter W. O'Hearn
1999	J	`jnl`	Syntactic Control of Interference Revisited. Theor. Comput. Sci. Peter W. O'Hearn, John Power, Makoto Takeyama, Robert D. Tennent
1999	J	`jnl`	The logic of bunched implications. Bull. Symb. Log. Peter W. O'Hearn, David J. Pym
1998	J	`jnl`	Polymorphism, objects and abstract types. SIGACT News Peter W. O'Hearn
1997	—	`conf`	An Axiomatic Approach to Binary Logical Relations with Applications to Data Refinement. TACS Yoshiki Kinoshita, Peter W. O'Hearn, John Power, Makoto Takeyama, Robert D. Tennent
1996	J	`jnl`	Note on Algol and Conservatively Extending Functional Programming. J. Funct. Program. Peter W. O'Hearn
1995	B	`conf`	Bireflectivity. MFPS Peter J. Freyd, Peter W. O'Hearn, John Power, Robert D. Tennent, Makoto Takeyama
1995	J	`jnl`	Kripke Logical Relations and PCF Inf. Comput. Peter W. O'Hearn, Jon G. Riecke
1995	B	`conf`	Objects, interference and the Yoneda embedding. MFPS Peter W. O'Hearn, Uday S. Reddy
1995	J	`jnl`	Parametricity and Local Variables. J. ACM Peter W. O'Hearn, Robert D. Tennent
1995	B	`conf`	Syntactic control of interference revisited. MFPS Peter W. O'Hearn, John Power, Robert D. Tennent, Makoto Takeyama
1994	A	`conf`	Fully Abstract Translations and Parametric Polymorphism. ESOP Peter W. O'Hearn, Jon G. Riecke
1993	J	`jnl`	A Model for Syntactic Control of Interference. Math. Struct. Comput. Sci. Peter W. O'Hearn
1993	A*	`conf`	Relational Parametricity and Local Variables. POPL Peter W. O'Hearn, Robert D. Tennent
1993	J	`jnl`	Semantical Analysis of Specification Logic, 2 Inf. Comput. Peter W. O'Hearn, Robert D. Tennent
1992	J	`jnl`	Resolution Framework for Finitely-Valued First-Order Logics. J. Symb. Comput. Peter W. O'Hearn, Zbigniew Stachniak
1991	—	`conf`	Linear Logic and Interference Control. Category Theory and Computer Science Peter W. O'Hearn
1989	—	`conf`	A Resolution Framework for Finitely-Valued First-Order Logics. SCAI Peter W. O'Hearn, Zbigniew Stachniak
1989	B	`conf`	Note on Theorem Proving Strategies for Resolution Counterparts of Non-Classical Logics. ISSAC Peter W. O'Hearn, Zbigniew Stachniak