Peter W. O'Hearn
According to our database^{1},
Peter W. O'Hearn
authored at least 90 papers
between 1989 and 2019.
Collaborative distances:
Collaborative distances:
Timeline
Legend:
Book In proceedings Article PhD thesis OtherLinks
Homepages:

at viaf.org

at orcid.org

at id.loc.gov

at dnb.info

at isni.org

at andrej.com

at dl.acm.org
On csauthors.net:
Bibliography
2019
A true positives theorem for a static race detector.
PACMPL, 2019
2018
RacerD: compositional static race detection.
PACMPL, 2018
From Startups to Scaleups: Opportunities and Open Problems for Static and Dynamic Program Analysis.
Proceedings of the 18th IEEE International Working Conference on Source Code Analysis and Manipulation, 2018
Experience Developing and Deploying Concurrency Analysis at Facebook.
Proceedings of the Static Analysis  25th International Symposium, 2018
Continuous Reasoning: Scaling the impact of formal methods.
Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, 2018
2016
Concurrent separation logic.
SIGLOG News, 2016
2015
Embracing Overapproximation for Proving Nontermination.
TinyToCS, 2015
On the relation between Concurrent Separation Logic and Concurrent Kleene Algebra.
J. Log. Algebr. Meth. Program., 2015
Moving Fast with Software Verification.
Proceedings of the NASA Formal Methods  7th International Symposium, 2015
From Categorical Logic to Facebook Engineering.
Proceedings of the 30th Annual ACM/IEEE Symposium on Logic in Computer Science, 2015
2014
Proving Nontermination via Safety.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2014
The essence of Reynolds.
Proceedings of the 41st Annual ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, 2014
Disproving termination with overapproximation.
Proceedings of the Formal Methods in ComputerAided Design, 2014
Developments in Concurrent Kleene Algebra.
Proceedings of the Relational and Algebraic Methods in Computer Science, 2014
2012
A Primer on Separation Logic (and Automatic Program Verification and Analysis).
Proceedings of the Software Safety and Security  Tools for Analysis and Verification, 2012
Presentation of the SIGPLAN distinguished achievement award to Sir Charles Antony Richard Hoare, FRS, FREng, FBCS; and interview.
Proceedings of the 39th ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, 2012
2011
The Complexity of Abduction for Separated Heap Abstractions.
Proceedings of the Static Analysis  18th International Symposium, 2011
Reasoning about Programs Using a Scientific Method.
Proceedings of the Formal Methods and Software Engineering, 2011
Algebra, Logic, Locality, Concurrency.
Proceedings of the Certified Programs and Proofs  First International Conference, 2011
On Locality and the Exchange Law for Concurrent Processes.
Proceedings of the CONCUR 2011  Concurrency Theory  22nd International Conference, 2011
Algebra, Logic, Locality, Concurrency.
Proceedings of the Programming Languages and Systems  9th Asian Symposium, 2011
2010
Blaming the client: on data refinement in the presence of pointers.
Formal Asp. Comput., 2010
Verifying linearizability with hindsight.
Proceedings of the 29th Annual ACM Symposium on Principles of Distributed Computing, 2010
Abductive, Inductive and Deductive Reasoning about Resources.
Proceedings of the Computer Science Logic, 24th International Workshop, 2010
2009
Graphical models of separation logic.
Inf. Process. Lett., 2009
Compositional shape analysis by means of biabduction.
Proceedings of the 36th ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, 2009
Abstraction for Concurrent Objects.
Proceedings of the Programming Languages and Systems, 2009
09301 Executive Summary  Typing, Analysis, and Verification of HeapManipulating Programs.
Proceedings of the Typing, Analysis and Verification of HeapManipulating Programs, 19.07., 2009
09301 Abstracts Collection  Typing, Analysis, and Verification of HeapManipulating Programs.
Proceedings of the Typing, Analysis and Verification of HeapManipulating Programs, 19.07., 2009
2008
Separation Logic Semantics for Communicating Processes.
Electr. Notes Theor. Comput. Sci., 2008
Space Invading Systems Code.
Proceedings of the LogicBased Program Synthesis and Transformation, 2008
Separation Logic Tutorial.
Proceedings of the Logic Programming, 24th International Conference, 2008
Scalable Shape Analysis for Systems Code.
Proceedings of the Computer Aided Verification, 20th International Conference, 2008
Tutorial on Separation Logic (Invited Tutorial).
Proceedings of the Computer Aided Verification, 20th International Conference, 2008
2007
Resources, concurrency, and local reasoning.
Theor. Comput. Sci., 2007
Preface.
Theor. Comput. Sci., 2007
Footprint Analysis: A Shape Analysis That Discovers Preconditions.
Proceedings of the Static Analysis, 14th International Symposium, 2007
Modular verification of a nonblocking stack.
Proceedings of the 34th ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, 2007
Variance analyses from invariance analyses.
Proceedings of the 34th ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, 2007
Local Action and Abstract Separation Logic.
Proceedings of the 22nd IEEE Symposium on Logic in Computer Science (LICS 2007), 2007
Separation logic and concurrent resource management.
Proceedings of the 6th International Symposium on Memory Management, 2007
Shape Analysis for Composite Data Structures.
Proceedings of the Computer Aided Verification, 19th International Conference, 2007
2006
Strong Update, Disposal, and Encapsulation in Bunched Typing.
Electr. Notes Theor. Comput. Sci., 2006
Verified Software: A Grand Challenge.
IEEE Computer, 2006
A Local Shape Analysis Based on Separation Logic.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2006
Separation Logic and Program Analysis.
Proceedings of the Static Analysis, 13th International Symposium, 2006
Beyond Reachability: Shape Abstraction in the Presence of Pointer Arithmetic.
Proceedings of the Static Analysis, 13th International Symposium, 2006
Automatic Termination Proofs for Programs with ShapeShifting Heaps.
Proceedings of the Computer Aided Verification, 18th International Conference, 2006
2005
Scalable Specification and Reasoning: Challenges for Program Logic.
Proceedings of the Verified Software: Theories, 2005
Permission accounting in separation logic.
Proceedings of the 32nd ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, 2005
Smallfoot: Modular Automatic Assertion Checking with Separation Logic.
Proceedings of the Formal Methods for Components and Objects, 4th International Symposium, 2005
Symbolic Execution with Separation Logic.
Proceedings of the Programming Languages and Systems, Third Asian Symposium, 2005
2004
Possible worlds and resources: the semantics of BI.
Theor. Comput. Sci., 2004
Separation and information hiding.
Proceedings of the 31st ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, 2004
Refinement and Separation Contexts.
Proceedings of the FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science, 2004
A Decidable Fragment of Separation Logic.
Proceedings of the FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science, 2004
Resources, Concurrency, and Local Reasoning (Abstract).
Proceedings of the Programming Languages and Systems, 2004
Resources, Concurrency and Local Reasoning.
Proceedings of the CONCUR 2004  Concurrency Theory, 15th International Conference, London, UK, August 31, 2004
2003
Program logic and equivalence in the presence of garbage collection.
Theor. Comput. Sci., 2003
On bunched typing.
J. Funct. Program., 2003
2002
Linear ContinuationPassing.
HigherOrder and Symbolic Computation, 2002
A Semantic Basis for Local Reasoning.
Proceedings of the Foundations of Software Science and Computation Structures, 2002
2001
BI as an Assertion Language for Mutable Data Structures.
Proceedings of the Conference Record of POPL 2001: The 28th ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, 2001
Computability and Complexity Results for a Spatial Assertion Language for Data Structures.
Proceedings of the FST TCS 2001: Foundations of Software Technology and Theoretical Computer Science, 2001
On Garbage and Program Logic.
Proceedings of the Foundations of Software Science and Computation Structures, 2001
Local Reasoning about Programs that Alter Data Structures.
Proceedings of the Computer Science Logic, 15th International Workshop, 2001
Computability and Complexity Results for a Spatial Assertion Language for Data Structures.
Proceedings of the Second Asian Workshop on Programming Languages and Systems, 2001
2000
From Algol to polymorphic linear lambdacalculus.
J. ACM, 2000
Semantic analysis of pointer aliasing, allocation and disposal in Hoare logic351292.
Proceedings of the 2nd international ACM SIGPLAN conference on on Principles and practice of declarative programming, 2000
1999
Objects, Interference, and the Yoneda Embedding.
Theor. Comput. Sci., 1999
Syntactic Control of Interference Revisited.
Theor. Comput. Sci., 1999
Bireflectivity.
Theor. Comput. Sci., 1999
The logic of bunched implications.
Bulletin of Symbolic Logic, 1999
Resource Interpretations, Bunched Implications and the alpha lambdaCalculus.
Proceedings of the Typed Lambda Calculi and Applications, 4th International Conference, 1999
1998
Polymorphism, objects and abstract types.
SIGACT News, 1998
1997
An Axiomatic Approach to Binary Logical Relations with Applications to Data Refinement.
Proceedings of the Theoretical Aspects of Computer Software, Third International Symposium, 1997
1996
Note on Algol and Conservatively Extending Functional Programming.
J. Funct. Program., 1996
1995
Kripke Logical Relations and PCF
Inf. Comput., July, 1995
Parametricity and Local Variables.
J. ACM, 1995
Objects, interference and the Yoneda embedding.
Electr. Notes Theor. Comput. Sci., 1995
Syntactic control of interference revisited.
Electr. Notes Theor. Comput. Sci., 1995
Bireflectivity.
Electr. Notes Theor. Comput. Sci., 1995
1994
Fully Abstract Translations and Parametric Polymorphism.
Proceedings of the Programming Languages and Systems, 1994
1993
Semantical Analysis of Specification Logic, 2
Inf. Comput., November, 1993
A Model for Syntactic Control of Interference.
Mathematical Structures in Computer Science, 1993
Relational Parametricity and Local Variables.
Proceedings of the Conference Record of the Twentieth Annual ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, 1993
1992
Resolution Framework for FinitelyValued FirstOrder Logics.
J. Symb. Comput., 1992
1991
Linear Logic and Interference Control.
Proceedings of the Category Theory and Computer Science, 1991
1989
A Resolution Framework for FinitelyValued FirstOrder Logics.
SCAI, 1989
Note on Theorem Proving Strategies for Resolution Counterparts of NonClassical Logics.
Proceedings of the ACMSIGSAM 1989 International Symposium on Symbolic and Algebraic Computation, 1989