Author name cluster

Peter W. O'Hearn

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

5 papers

2 author rows

CSL Conference 2010 Invited Paper

Abductive, Inductive and Deductive Reasoning about Resources

Peter W. O'Hearn

Abstract We describe a method for reasoning about programs that uses a mixture of abductive, inductive and deductive inference. It allows us to synthesize a pre/post spec for a program procedure, without requiring any information about the procedure’s calling context. The method can be used to obtain partial specifications for portions of large code bases in the millions of lines of code.

Details

LOPSTR Conference 2008 Conference Paper

Space Invading Systems Code

Cristiano Calcagno
Dino Distefano
Peter W. O'Hearn
Hongseok Yang

Abstract Space Invader is a static analysis tool that aims to perform accurate, automatic verification of the way that programs use pointers. It uses separation logic assertions [10, 11] to describe states, and works by performing a proof search, using abstract interpretation to enable convergence. As well as having roots in separation logic, Invader draws on the fundamental work of Sagiv et. al. on shape analysis [12]. It is complementary to other tools - e. g. , SLAM [1], Blast [8], ASTRÉE [6] - that use abstract interpretation for verification, but that use coarse or limited models of the heap.

Details

TCS Journal 2004 Journal Article

Possible worlds and resources: the semantics of BI

David J. Pym
Peter W. O'Hearn
Hongseok Yang

The logic of bunched implications, BI, is a substructural system which freely combines an additive (intuitionistic) and a multiplicative (linear) implication via bunches (contexts with two combining operations, one which admits Weakening and Contraction and one which does not). BI may be seen to arise from two main perspectives. On the one hand, from proof-theoretic or categorical concerns and, on the other, from a possible-worlds semantics based on preordered (commutative) monoids. This semantics may be motivated from a basic model of the notion of resource. We explain BI's proof-theoretic, categorical and semantic origins. We discuss in detail the question of completeness, explaining the essential distinction between BI with and without ⊥ (the unit of ∨). We give an extensive discussion of BI as a semantically based logic of resources, giving concrete models based on Petri nets, ambients, computer memory, logic programming, and money.

Details DOI

CSL Conference 2001 Invited Paper

Local Reasoning about Programs that Alter Data Structures

Peter W. O'Hearn
John C. Reynolds
Hongseok Yang

Abstract We describe an extension of Hoare’s logic for reasoning about programs that alter data structures. We consider a low-level storage model based on a heap with associated lookup, update, allocation and deallocation operations, and unrestricted address arithmetic. The assertion language is based on a possible worlds model of the logic of bunched implications, and includes spatial conjunction and implication connectives alongside those of classical logic. Heap operations are axiomatized using what we call the “small axioms”, each of which mentions only those cells accessed by a particular command. Through these and a number of examples we show that the formalism supports local reasoning: A specification and proof can concentrate on only those cells in memory that a program accesses. This paper builds on earlier work by Burstall, Reynolds, Ishtiaq and O’Hearn on reasoning about data structures.

Details

TCS Journal 1999 Journal Article

Objects, interference, and the Yoneda embedding

Peter W. O'Hearn
Uday S. Reddy

We present a new semantics for Algol-like languages that combines methods from two prior lines of development: 1. the object-based approach of Reddy, where the meaning of an imperative program is described in terms of sequences of observable actions, and 2. the functor-category approach initiated by Reynolds, where the varying nature of the run-time stack is explained using functors from a category of store shapes to a category of cpos. The semantics gives an account of both the phemomena of local state and irreversibility of state change. As an indication of the accuracy obtained, we present a full abstraction result for closed terms of second-order type in a language containing active expressions, i. e. value-returning commands.

Details DOI