Online Publications
























Separation Logic. P O'Hearn. Communications of the ACM, February 2019, Vol. 62 No. 2, Pages 86-95. ( Appendix on Mechanized Reasoning )

A True Positives Theorem for a Static Race Detector. N Gorogiannis, P O'Hearn and I Sergey POPL'19

Why Separation Logic Works D Pym, JM Spring, and P O'Hearn. P. Philos. Technol. (2018)

RacerD: Compositional Static Race Detection. S Blackshear, N Gorogiannis, P O'Hearn and I Sergey. OOPSLA'18

From Start-ups to Scale-ups: Opportunities and Open Problems for Static and Dynamic Program Analysis. M Harman and P O'Hearn. Invited paper at SCAM'18

Experience developing and deploying concurrency analysis at Facebook. P O'Hearn. Invited tutorial at SAS'18

Continuous Reasoning: Scaling the impact of formal methods. . P O'Hearn. LICS'18 paper associated with my plenary talk at FLoc

Why Separation Logic Works D Pym, JM Spring, and P O'Hearn. P. Philos. Technol. (2018)

Concurrent Separation Logic.
Steve Brookes and Peter O'Hearn. ACM SIGLOG News Vol 3, No 3, pp 47-65, July 2016

From Categorical Logic to Facebook Engineering. P O'Hearn
30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pp17-21

Moving Fast with Software Verification.
NASA Formal Methods symposium, 2015

On the relation between Concurrent Separation Logic and Concurrent Kleene Algebra. P. O'Hearn, R. L. Petersen, J. Villard and A. Hussain.
Journal of Logical and Algebraic Methods in Programming 84(3): 285-302 (2015)

Disproving Termination with Overapproximation. B. Cook, C. Fuhs, K. Nimkar, and P. O'Hearn
Proceedings of the 14th International Conference on Formal Methods in Computer-Aided Design (FMCAD '14), Lausanne, Switzerland, 2014

Developments in Concurrent Kleene Algebra. Tony Hoare, Stephan van Staden, Bernhard Möller, Georg Struth, Jules Villard, Huibiao Zhu, Peter W. O'Hearn.
RAMICS 2014: 1-18

Proving Nontermination via Safety. Hong Yi Chen, Byron Cook, Carsten Fuhs, Kaustubh Nimkar, Peter W. O'Hearn
TACAS 2014: 156-171

The Essence of Reynolds. Tribute to John C. Reynolds.
POPL'14, pages 251-255. Also published in Formal Asp. Comput. 26(3): 435-439 (2014)

A Primer on Separation Logic (and Automatic Program Verification and Analysis). PW O'Hearn.
In Software Safety and Secuurity; Tools for Analysis and Verification. NATO Science for Peace and Security Series, vol 33, pp286-318, 2012.

Verification Condition Generation and Variable Conditions in Smallfoot. J Berdine, C Calcagno, PW O'Hearn. CoRR abs/1204.4804: (2012)

Compositional Shape Analysis by means of Bi-Abduction. Journal of the ACM (JACM), Volume 58 Issue 6, December 2011. 73 pages.
C Calcagno, D Distefano, PW O'Hearn and H Yang.

On Locality and the Exchange Law for Concurrent Processes.
CAR Hoare, A Hussain, B Moller, PW O'Hearn, RL Petersen and G Struth. CONCUR 2011

The Complexity of Abduction for Separated Heap Abstractions.
N Gorogiannis, M Kanovich and PW O'Hearn. SAS 2011

Abstraction for Concurrent Objects
I Filipovic, PW O'Hearn, N Rinetzky and H Yang. Theoretical Computer Science, vol 411(51-52), pp4379--4398, December 2010.

Blaming the Client: On Data Refinement in the Presence of Pointers
I Filipovic, P O'Hearn, N Torp-Smith and H Yang. Formal Aspects of Computing 22(5) pp 547-583, Sept 2010

Verifying Linearizability with Hindsight
PW O'Hearn, N Rinetzky, M Vechev, E Yahav, G Yorsh. PODC 2010, pp85-94.

Graphical Models of Separation Logic
I Wehrman, T Hoare, P O'Hearn. Information Processing Letters, June 2009.

Separation and Information Hiding.
P O'Hearn, H Yang and J Reynolds. ACM TOPLAS 31(3), April 2009. (Prelim version appeared in POPL'04.)

Abstraction for Concurrent Objects
I Filipovic, PW O'Hearn, N Rinetzky and H Yang. ESOP'09

Compositional Shape Analysis by means of Bi-Abduction
C Calcagno, D Distefano, PW O'Hearn and H Yang. POPL'09 . Extended version to appear in J.ACM.

Separation Logic Semantics of Communicating Processes
T Hoare and P O'Hearn, Proceedings of 1st FICS conference, ENTCS, 2008.

Scalable Shape Analysis for Systems Code
Hongseok Yang, Oukseh Lee, Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, Peter W. O'Hearn.
In CAV'08 , pp385-398

Local Action and Abstract Separation Logic.
C Calcagno, PW O'Hearn and H Yang. In LICS'07 .

Resources, Concurrency and Local Reasoning
PW O'Hearn, Theoretical Computer Science 375(1-3) , pp271-307, May 2007.
A preliminary version appeared in the Proceedings of CONCUR'04, LNCS 3170, pp49-67.

Festschrift for John C Reynolds's 70th Birthday.
Theoretical Computer Science, Vol 375(1-3), 1 May 2007.

Shape analysis for composite data structures.
J Berdine, C Calcagno, B Cook, D Distefano, PW O'Hearn, T Wies and H Yang.
In CAV'07 .

Footprint Analysis: A shape analysis that discovers preconditions.
C Calcagno, D Distefano, P O'Hearn and H Yang. In SAS'07

Variance Analyses from Invariance Analyses (or, Termination Analyzers for Free!)
J Berdine, A Chawdhary, B Cook, D Distefano and P O'Hearn
POPL 2007

Modular Verification of a Non-blocking Stack
M Parkinson, R Bornat and P O'Hearn
POPL 2007

Strong Update, Disposal, and Encapsulation in Bunched Typing.
J Berdine and PW O'Hearn. MFPS 2006.

Verified Software: A Grand Challenge
C Jones, P O'Hearn and J Woodcock. IEEE Computer, March 2006, pp93-95.

Beyond Reachability: Shape Abstraction in the Presence of Pointer Arithmetic.
C Calcagno, D Distefano, P O'Hearn and H Yang. In 13th SAS, LNCS 4134, 182-203, 2006

Automatic termination proofs for programs with shape-shifting heaps.
J Berdine, B Cook, D Distefano and P O'Hearn.In 18th CAV, LNCS 4144, pp386-400, 2006

Smallfoot: Modular Automatic Assertion Checking with Separation Logic
J Berdine, C Calcagno and PW O'Hearn. In 4th FMCO, LNCS 4111, 2006
A Collection of Example Smallfoot Programs

A local shape analysis based on separation logic
D Distefano, P O'Hearn and H Yang. In 12th TACAS, LNCS 3920, pp287-302, 2006.

Symbolic Execution with Separation Logic.
J Berdine, C Calcagno and PW O'Hearn. Proceedings of APLAS'05, LNCS 3780, pp52-68.

Permission Accounting in Separation Logic
R Bornat, C Calcagno, P O'Hearn and M Parkinson
POPL 2005, 59-70.

A Decidable Fragment of Separation Logic
J Berdine, C Calcagno and P O'Hearn
Proceedings of FSTTCS 2004, 97-109.

Refinement and Separation Contexts
I Mijajlovic, N Torp-Smith and and P O'Hearn
FSTTCS 2004, 421-433.

Local Reasoning, Separation and Aliasing
R Bornat, C Calcagno and P O'Hearn
In the informal proceedings of SPACE 2004.

Separation and Information Hiding
PW O'Hearn, H Yang and JC Reynolds
POPL'04, pages 268-280.

Possible worlds and resources: The semantics of BI
David Pym, Peter O'Hearn, Hongseok Yang
Theoretical Computer Science 315(1), pp257-305, 2004.

Program Logic and Equivalence in the Presence of Garbage Collection
Cristiano Calcagno, Peter O'Hearn, Richard Bornat.
Theoretical Computer Science, vol. 298/3, pp557-581, 2003.

On Bunched Typing
Journal of Functional Programming, 13(4), pp747-796, 2003. PDF version

Linear Continuation-Passing
Josh Berdine, Peter O'Hearn, Uday Reddy, Hayo Thielecke.
Higher Order and Symbolic Computation, 15(2/3):181--208, September 2002.

A Semantic Basis for Local Reasoning
Hongseok Yang, Peter O'Hearn
Proceedings of FOSSACS'02. PDF version

Local Reasoning about Programs that Alter Data Structures
Peter O'Hearn, John Reynolds, Hongseok Yang
Proceedings of CSL'01, Paris, 2001. Pages 1-19, LNCS 2142 ©Springer-Verlag. PDF version

Computability and Complexity Results for a Spatial Assertion Language for Data Structures
Cristiano Calcagno, Hongseok Yang, Peter O'Hearn
Proceedings of FSTTCS'01. PDF version

BI as an Assertion Language for Mutable Data Structures.
Samin Ishtiaq, Peter O'Hearn
Proceedings of POPL'01. PDF version
2011 Most Influential POPL Paper Award

Linearly Used Continuations
Josh Berdine, Peter O'Hearn, Uday Reddy, Hayo Thielecke
Proceedings of Continuations Workshop, 2001 Note: This paper has been superceded by ``Linear Continuation-Passing''.

On Garbage and Program Logic
Cristiano Calcagno, Peter O'Hearn
Proceedings of FOSSACS'01.

Semantic Analysis of Pointer Aliasing, Allocation and Disposal in Hoare Logic
Cristiano Calcago, Samin Ishtiaq, Peter O'Hearn
Proceedings of PPDP'00. PDF version

From Algol to Polymorphic Linear Lambda-calculus ( postscript )
P. W. O'Hearn and J. C. Reynolds
Journal of the ACM , 47(1), pp167-223, January 2000.

Petri Net Semantics of Bunched Implications
Peter O'Hearn and Hongseok Yang Unpublished Manuscript, 14 Oct, 1999

The logic of bunched implications
P.W. O'Hearn and D. J. Pym. Bulletin of Symbolic Logic , 5(2), June 1999, pp215-244

Resource Interpretations, Bunched Implications and the alpha-lambda-calculus
P. W. O'Hearn, in J.-Y. Girard, ed., Proceedings, 4th Conference on Typed Lambda-Calculi and Applications, L'Aquila, Italy, April 1999. pages 258-279. LNCS 1581 ©Springer-Verlag.
Note: This paper has been superceded by ``On Bunched Typing''.

Bireflectivity.
P. J. Freyd, P. W. O'Hearn, A. J. Power, R. Street, M. Takeyama and R. D. Tennent.
Theoretical Computer Science 228(1-2) 49-76, 1999.
Preliminary version appeared in Proceedings of MFPS XI.

Syntactic Control of Interference Revisited .
P. W. O'Hearn, A. J. Power, M. Takeyama and R. D. Tennent.
Theoretical Computer Science 228(1-2) 211-252, 1999.
Preliminary version appeared in Proceedings of MFPS XI.

Objects, Interference and the Yoneda Embedding .
P. W. O'Hearn and U.S. Reddy.
Theoretical Computer Science 228(1-2) 253-282, 1999.
Preliminary version appeared in Proceedings of MFPS XI.

Polymorphism, Objects and Abstract Types
P. W. O'Hearn
SIGACT News , Volume 29(4), pp39-50, December 1998

An Axiomatic Approach to Binary Logical Relations, with applications to Data Refinement .
Y. Kinoshita, P. O'Hearn, J. Power, M. Takeyama, R. Tennent, TACS'97
©Springer-Verlag.

Domains and Denotational Semantics: History, Accomplishments, and Open Problems .
M. P. Fiore, A. Jung, E. Moggi, P. O'Hearn, J. Riecke, G. Rosolini, and I. Stark.
In number 59 of Bulletin of the European Association for Theoretical Computer Science, pages 227--256, 1996.

Note on Algol and Conservatively Extending Functional Programming . P. W. O'Hearn
J. Func. Programming, 6(1), pp171--180, January 1996.

Kripke Logical Relations and PCF .
P. W. O'Hearn and J. G. Riecke.
Information and Computation, 120(1):107-116, 1995.

Parametricity and Local Variables .
P. W. O'Hearn and R. D. Tennent.
J.ACM. 42(3): 658-709, May 1995.

Semantical analysis of specification logic, part 2 . Abstract .
P. W. O'Hearn and R. D. Tennent.
Information and Computation 107(1), pp25-57, 1993.

A model for Syntactic Control of Interference .
P. W. O'Hearn.
Mathematical Structures in Computewr Science, 1993.

Semantics of Local Variables.
P. W. O'Hearn and R. D. Tennent.
Applications of Categories in Computer Science, volume 177 of the London Math Society Lecture Notes Steris, pp. 217-238, Cambridge Univ Press, 1992.

Algol-like languages
P.W. O'Hearn and R.D. Tennent editors
Progress in Theoretical Computer Science, Birkhauser, 1997