2009 |
63 | EE | Ivana Filipovic,
Peter W. O'Hearn,
Noam Rinetzky,
Hongseok Yang:
Abstraction for Concurrent Objects.
ESOP 2009: 252-266 |
62 | EE | Cristiano Calcagno,
Dino Distefano,
Peter W. O'Hearn,
Hongseok Yang:
Compositional shape analysis by means of bi-abduction.
POPL 2009: 289-300 |
61 | EE | Peter W. O'Hearn,
Hongseok Yang,
John C. Reynolds:
Separation and information hiding.
ACM Trans. Program. Lang. Syst. 31(3): (2009) |
2008 |
60 | EE | Peter W. O'Hearn:
Tutorial on Separation Logic (Invited Tutorial).
CAV 2008: 19-21 |
59 | EE | Hongseok Yang,
Oukseh Lee,
Josh Berdine,
Cristiano Calcagno,
Byron Cook,
Dino Distefano,
Peter W. O'Hearn:
Scalable Shape Analysis for Systems Code.
CAV 2008: 385-398 |
58 | EE | Peter W. O'Hearn:
Separation Logic Tutorial.
ICLP 2008: 15-21 |
57 | EE | Cristiano Calcagno,
Dino Distefano,
Peter W. O'Hearn,
Hongseok Yang:
Space Invading Systems Code.
LOPSTR 2008: 1-3 |
56 | EE | Tony Hoare,
Peter W. O'Hearn:
Separation Logic Semantics for Communicating Processes.
Electr. Notes Theor. Comput. Sci. 212: 3-25 (2008) |
2007 |
55 | EE | Josh Berdine,
Cristiano Calcagno,
Byron Cook,
Dino Distefano,
Peter W. O'Hearn,
Thomas Wies,
Hongseok Yang:
Shape Analysis for Composite Data Structures.
CAV 2007: 178-192 |
54 | EE | Peter W. O'Hearn:
Separation logic and concurrent resource management.
ISMM 2007: 1 |
53 | EE | Cristiano Calcagno,
Peter W. O'Hearn,
Hongseok Yang:
Local Action and Abstract Separation Logic.
LICS 2007: 366-378 |
52 | EE | Josh Berdine,
Aziem Chawdhary,
Byron Cook,
Dino Distefano,
Peter W. O'Hearn:
Variance analyses from invariance analyses.
POPL 2007: 211-224 |
51 | EE | Matthew J. Parkinson,
Richard Bornat,
Peter W. O'Hearn:
Modular verification of a non-blocking stack.
POPL 2007: 297-302 |
50 | EE | Cristiano Calcagno,
Dino Distefano,
Peter W. O'Hearn,
Hongseok Yang:
Footprint Analysis: A Shape Analysis That Discovers Preconditions.
SAS 2007: 402-418 |
49 | EE | Olivier Danvy,
Peter W. O'Hearn,
Philip Wadler:
Preface.
Theor. Comput. Sci. 375(1-3): 1-2 (2007) |
48 | EE | Peter W. O'Hearn:
Resources, concurrency, and local reasoning.
Theor. Comput. Sci. 375(1-3): 271-307 (2007) |
2006 |
47 | EE | Josh Berdine,
Byron Cook,
Dino Distefano,
Peter W. O'Hearn:
Automatic Termination Proofs for Programs with Shape-Shifting Heaps.
CAV 2006: 386-400 |
46 | EE | Peter W. O'Hearn:
Separation Logic and Program Analysis.
SAS 2006: 181 |
45 | EE | Cristiano Calcagno,
Dino Distefano,
Peter W. O'Hearn,
Hongseok Yang:
Beyond Reachability: Shape Abstraction in the Presence of Pointer Arithmetic.
SAS 2006: 182-203 |
44 | EE | Dino Distefano,
Peter W. O'Hearn,
Hongseok Yang:
A Local Shape Analysis Based on Separation Logic.
TACAS 2006: 287-302 |
43 | EE | Josh Berdine,
Peter W. O'Hearn:
Strong Update, Disposal, and Encapsulation in Bunched Typing.
Electr. Notes Theor. Comput. Sci. 158: 81-98 (2006) |
42 | EE | Cliff B. Jones,
Peter W. O'Hearn,
Jim Woodcock:
Verified Software: A Grand Challenge.
IEEE Computer 39(4): 93-95 (2006) |
2005 |
41 | EE | Josh Berdine,
Cristiano Calcagno,
Peter W. O'Hearn:
Symbolic Execution with Separation Logic.
APLAS 2005: 52-68 |
40 | EE | Josh Berdine,
Cristiano Calcagno,
Peter W. O'Hearn:
Smallfoot: Modular Automatic Assertion Checking with Separation Logic.
FMCO 2005: 115-137 |
39 | EE | Richard Bornat,
Cristiano Calcagno,
Peter W. O'Hearn,
Matthew J. Parkinson:
Permission accounting in separation logic.
POPL 2005: 259-270 |
38 | EE | Peter W. O'Hearn:
Scalable Specification and Reasoning: Challenges for Program Logic.
VSTTE 2005: 116-133 |
2004 |
37 | EE | Peter W. O'Hearn:
Resources, Concurrency and Local Reasoning.
CONCUR 2004: 49-67 |
36 | EE | Peter W. O'Hearn:
Resources, Concurrency, and Local Reasoning (Abstract).
ESOP 2004: 1-2 |
35 | EE | Ivana Mijajlovic,
Noah Torp-Smith,
Peter W. O'Hearn:
Refinement and Separation Contexts.
FSTTCS 2004: 421-433 |
34 | EE | Josh Berdine,
Cristiano Calcagno,
Peter W. O'Hearn:
A Decidable Fragment of Separation Logic.
FSTTCS 2004: 97-109 |
33 | EE | Peter W. O'Hearn,
Hongseok Yang,
John C. Reynolds:
Separation and information hiding.
POPL 2004: 268-280 |
32 | EE | David J. Pym,
Peter W. O'Hearn,
Hongseok Yang:
Possible worlds and resources: the semantics of BI.
Theor. Comput. Sci. 315(1): 257-305 (2004) |
2003 |
31 | EE | Peter W. O'Hearn:
On bunched typing.
J. Funct. Program. 13(4): 747-796 (2003) |
30 | EE | Cristiano Calcagno,
Peter W. O'Hearn,
Richard Bornat:
Program logic and equivalence in the presence of garbage collection.
Theor. Comput. Sci. 3(298): 557-581 (2003) |
2002 |
29 | EE | Hongseok Yang,
Peter W. O'Hearn:
A Semantic Basis for Local Reasoning.
FoSSaCS 2002: 402-416 |
28 | | Josh Berdine,
Peter W. O'Hearn,
Uday S. Reddy,
Hayo Thielecke:
Linear Continuation-Passing.
Higher-Order and Symbolic Computation 15(2-3): 181-208 (2002) |
2001 |
27 | | Cristiano Calcagno,
Hongseok Yang,
Peter W. O'Hearn:
Computability and Complexity Results for a Spatial Assertion Language for Data Structures.
APLAS 2001: 289-300 |
26 | EE | Peter W. O'Hearn,
John C. Reynolds,
Hongseok Yang:
Local Reasoning about Programs that Alter Data Structures.
CSL 2001: 1-19 |
25 | EE | Cristiano Calcagno,
Hongseok Yang,
Peter W. O'Hearn:
Computability and Complexity Results for a Spatial Assertion Language for Data Structures.
FSTTCS 2001: 108-119 |
24 | EE | Cristiano Calcagno,
Peter W. O'Hearn:
On Garbage and Program Logic.
FoSSaCS 2001: 137-151 |
23 | | Samin S. Ishtiaq,
Peter W. O'Hearn:
BI as an Assertion Language for Mutable Data Structures.
POPL 2001: 14-26 |
2000 |
22 | EE | Cristiano Calcagno,
Samin S. Ishtiaq,
Peter W. O'Hearn:
Semantic analysis of pointer aliasing, allocation and disposal in Hoare logic351292.
PPDP 2000: 190-201 |
21 | EE | Peter W. O'Hearn,
John C. Reynolds:
From Algol to polymorphic linear lambda-calculus.
J. ACM 47(1): 167-223 (2000) |
1999 |
20 | EE | Peter W. O'Hearn:
Resource Interpretations, Bunched Implications and the alpha lambda-Calculus.
TLCA 1999: 258-279 |
19 | EE | Peter W. O'Hearn,
David J. Pym:
The logic of bunched implications.
Bulletin of Symbolic Logic 5(2): 215-244 (1999) |
18 | EE | Peter W. O'Hearn,
John Power,
Makoto Takeyama,
Robert D. Tennent:
Syntactic Control of Interference Revisited.
Theor. Comput. Sci. 228(1-2): 211-252 (1999) |
17 | EE | Peter W. O'Hearn,
Uday S. Reddy:
Objects, Interference, and the Yoneda Embedding.
Theor. Comput. Sci. 228(1-2): 253-282 (1999) |
16 | EE | Peter J. Freyd,
Peter W. O'Hearn,
A. John Power,
Makoto Takeyama,
R. Street,
Robert D. Tennent:
Bireflectivity.
Theor. Comput. Sci. 228(1-2): 49-76 (1999) |
1997 |
15 | | Yoshiki Kinoshita,
Peter W. O'Hearn,
John Power,
Makoto Takeyama,
Robert D. Tennent:
An Axiomatic Approach to Binary Logical Relations with Applications to Data Refinement.
TACS 1997: 191-212 |
1996 |
14 | | Peter W. O'Hearn:
Note on Algol and Conservatively Extending Functional Programming.
J. Funct. Program. 6(1): 171-180 (1996) |
1995 |
13 | EE | Peter J. Freyd,
Peter W. O'Hearn,
John Power,
Robert D. Tennent,
Makoto Takeyama:
Bireflectivity.
Electr. Notes Theor. Comput. Sci. 1: (1995) |
12 | EE | Peter W. O'Hearn,
Uday S. Reddy:
Objects, interference and the Yoneda embedding.
Electr. Notes Theor. Comput. Sci. 1: (1995) |
11 | EE | Peter W. O'Hearn,
John Power,
Robert D. Tennent,
Makoto Takeyama:
Syntactic control of interference revisited.
Electr. Notes Theor. Comput. Sci. 1: (1995) |
10 | | Peter W. O'Hearn,
Jon G. Riecke:
Kripke Logical Relations and PCF
Inf. Comput. 120(1): 107-116 (1995) |
9 | EE | Peter W. O'Hearn,
Robert D. Tennent:
Parametricity and Local Variables.
J. ACM 42(3): 658-709 (1995) |
1994 |
8 | | Peter W. O'Hearn,
Jon G. Riecke:
Fully Abstract Translations and Parametric Polymorphism.
ESOP 1994: 454-468 |
1993 |
7 | | Peter W. O'Hearn,
Robert D. Tennent:
Relational Parametricity and Local Variables.
POPL 1993: 171-184 |
6 | | Peter W. O'Hearn,
Robert D. Tennent:
Semantical Analysis of Specification Logic, 2
Inf. Comput. 107(1): 25-57 (1993) |
5 | | Peter W. O'Hearn:
A Model for Syntactic Control of Interference.
Mathematical Structures in Computer Science 3(4): 435-465 (1993) |
1992 |
4 | | Peter W. O'Hearn,
Zbigniew Stachniak:
Resolution Framework for Finitely-Valued First-Order Logics.
J. Symb. Comput. 13(3): 235-254 (1992) |
1991 |
3 | | Peter W. O'Hearn:
Linear Logic and Interference Control.
Category Theory and Computer Science 1991: 74-93 |
1989 |
2 | EE | Peter W. O'Hearn,
Zbigniew Stachniak:
Note on Theorem Proving Strategies for Resolution Counterparts of Non-Classical Logics.
ISSAC 1989: 364-372 |
1 | | Peter W. O'Hearn,
Zbigniew Stachniak:
A Resolution Framework for Finitely-Valued First-Order Logics.
SCAI 1989: 69-81 |