## 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