[10-29]Seminar on A Pointer Logic for ...

Date:2007-12-27

Title: A Pointer Logic for Object Diagrams
Speaker: Yifeng Chen
         Department of Computer Science, University of Durham, Durham DH1 3LE, UK.
Time:    10am, 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.