Slides from
several talks
may be found at the bottom of this page.
Abstraction for Concurrent Objects
I Filipovic, PW O'Hearn, N Rinetzky and H Yang.
Theoretical Computer Science, vol 411(51-52), pp4379--4398, December 201
0.
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
Refinement and Separation Contexts
J Berdine, C Calcagno
and P O'Hearn
Proceedings of FSTTCS 2004, 97-109.
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
Linearly Used Cont
inuations
On Garbage and Program
Logic
Semantic Analysis of Pointer Aliasing, Allocation and Disposal in Hoare
Logic
From Algol to Polymorphic Linear Lambda-calculus
(
postscript
)
Petri Net Semantics of Bunched Implications
The logic of bunched implications
Resource Interpretations, Bunched Implications
and the alpha-lambda-calculus
Bireflectivity.
Syntactic Control of Interference Revisited .
Objects, Interference and the Yoneda Embedding .
Polymorphism, Objects and Abstract Types
An Axiomatic Approach to Binary Logical Relations, with applications
to Data Refinement .
Domains and Denotational Semantics: History, Accomplishments, and Open Problems .
Note on Algol and Conservatively Extending Functional Programming .
P. W. O'Hearn
Kripke Logical Relations and PCF .
Parametricity and Local Variables .
Semantical analysis of specification logic, part 2
.
Abstract .
A model for Syntactic Control of Interference
.
Semantics of Local Variables.
Algol-like languages
Tutorial on Separation Logic.
Space Invading Systems Code.
Resources, Concurrency and Local Reasoning
Local Reasoning about Programs that Alter Data Structures.
Reasoning about Shared Mutable Data Structure.
Semantics of Storage
Josh Berdine, Peter O'Hearn, Uday Reddy, Hayo Thielecke
Proceedings of Continuations Workshop, 2001
Cristiano Calcagno, Peter O'Hearn
Proceedings of FOSSACS'01.
Cristiano Calcago, Samin Ishtiaq, Peter O'Hearn
Proceedings of PPDP'00.
PDF version
P. W. O'Hearn and J. C. Reynolds
Journal of the ACM ,
47(1), pp167-223, January 2000.
Peter O'Hearn and Hongseok Yang
Unpublished Manuscript, 14 Oct, 1999
P.W. O'Hearn and D. J. Pym. Bulletin of Symbolic Logic ,
5(2), June 1999, pp215-244
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''.
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.
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.
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.
P. W. O'Hearn
SIGACT News , Volume 29(4), pp39-50, December 1998
Y. Kinoshita, P. O'Hearn, J. Power, M. Takeyama, R. Tennent,
TACS'97
©Springer-Verlag.
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.
J. Func. Programming, 6(1), pp171--180, January 1996.
P. W. O'Hearn and J. G. Riecke.
Information and Computation,
120(1):107-116, 1995.
P. W. O'Hearn and R. D. Tennent.
J.ACM. 42(3): 658-709, May 1995.
P. W. O'Hearn and R. D. Tennent.
Information and Computation 107(1), pp25-57, 1993.
P. W. O'Hearn.
Mathematical Structures in Computewr Science, 1993.
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.
P.W. O'Hearn and R.D. Tennent editors
Progress in Theoretical Computer Science, Birkhauser, 1997
CAV Invited Tutorial, July 2008, Princeton
LOPSTR Invited Talk, July 2008, Valencia.
Short paper in the LOPSTR Proceedings
Slides from invited talk at ETAPS'04 .
Peter O'Hearn, John Reynolds, Hongseok Yang
Slides from invited talk at CSL'01.
John Reynolds, Peter O'Hearn
Slides from invited talk at
SPACE 2001.
PDF version
Slides from Invited Lecture, MFPS00, Hoboken NJ.