A Pointer Logic for Object Diagrams

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