Peter W. O'Hearn

According to our database1, Peter W. O'Hearn authored at least 94 papers between 1989 and 2018.

Collaborative distances:

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Other 

Links

Homepages:

On csauthors.net:

Bibliography

2018
RacerD: compositional static race detection.
PACMPL, 2018

From Start-ups to Scale-ups: 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
The Essence of Reynolds.
Formal Asp. Comput., 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 SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2014

Disproving termination with overapproximation.
Proceedings of the Formal Methods in Computer-Aided 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

Verification Condition Generation and Variable Conditions in Smallfoot
CoRR, 2012

Presentation of the SIGPLAN distinguished achievement award to Sir Charles Antony Richard Hoare, FRS, FREng, FBCS; and interview.
Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2012

2011
Compositional Shape Analysis by Means of Bi-Abduction.
J. ACM, 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
Abstraction for concurrent objects.
Theor. Comput. Sci., 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
Separation and information hiding.
ACM Trans. Program. Lang. Syst., 2009

Graphical models of separation logic.
Inf. Process. Lett., 2009

Compositional shape analysis by means of bi-abduction.
Proceedings of the 36th ACM SIGPLAN-SIGACT 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 Heap-Manipulating Programs.
Proceedings of the Typing, Analysis and Verification of Heap-Manipulating Programs, 19.07., 2009

09301 Abstracts Collection - Typing, Analysis, and Verification of Heap-Manipulating Programs.
Proceedings of the Typing, Analysis and Verification of Heap-Manipulating Programs, 19.07., 2009

2008
Separation Logic Semantics for Communicating Processes.
Electr. Notes Theor. Comput. Sci., 2008

Space Invading Systems Code.
Proceedings of the Logic-Based 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 non-blocking stack.
Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2007

Variance analyses from invariance analyses.
Proceedings of the 34th ACM SIGPLAN-SIGACT 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 Shape-Shifting 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 SIGPLAN-SIGACT 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 SIGPLAN-SIGACT 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 Continuation-Passing.
Higher-Order 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 SIGPLAN-SIGACT 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 lambda-calculus.
J. ACM, 2000

Semantic analysis of pointer aliasing, allocation and disposal in Hoare logic351292.
PPDP, 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 lambda-Calculus.
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 SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 1993

1992
Resolution Framework for Finitely-Valued First-Order 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 Finitely-Valued First-Order Logics.
SCAI, 1989

Note on Theorem Proving Strategies for Resolution Counterparts of Non-Classical Logics.
Proceedings of the ACM-SIGSAM 1989 International Symposium on Symbolic and Algebraic Computation, 1989


  Loading...