Title:A Pointer Logic for Object Diagrams

Speaker: Yifeng Chen £¨Department of Computer Science, University of Durham,
Durham DH1 3LE, UK.£©

Time: 9am, Monday October 29

Venue: Lecture room, Lab for Computer Science, Level 3 Building #5, Institute
of Software, CAS

Abstract:

Compositional reasoning about pointers and references is crucial to verification
of contemporary software. This talk introduces a pointer logic that extends
Separation Logic with a fixpoint operator and new compositions different from
separating conjunction. Higher level of abstraction can be achieved if the right
compositions are used in the right places. In particular, if a relation is a
'full unique decomposition' then the corresponding composition decomposes any
given graph uniquely into two parts; an example is the separation between the
non-garbage and garbage parts of memory. The logic is proved to be largely satisfaction-decidable
in the sense that there is a finite procedure to determine whether or not a
program state satisfies a formula. The main technical result of the paper is
that if only full unique decompositions are used in compositions, then a rather
general fragment becomes validity-decidable. The logic is axiomatized and, with
the help of an infinitary inference rule, proved to be complete. Separation
Logic without pointer arithmetic is shown to be a fragment of the logic.

.