Sciweavers

Share
MPC
2010
Springer

Abstraction of Object Graphs in Program Verification

11 years 7 months ago
Abstraction of Object Graphs in Program Verification
ion of Object Graphs in Program Verification Yifeng Chen1 and J.W. Sanders2 1 HCST Key Lab at School of EECS, Peking University, China. 2 UNU-IIST, Macao. A set-theoretic formalism, AOG, is introduced to support automated verification of pointer programs. AOG targets pointer reasoning for source programs before compilation (before removal of field names). Pointer structures are represented as object graphs instead of heaps. Each property in AOG is a relation between object graphs and name assignments of program variables, and specifications result from composing properties. AOG extends Separation Logic's compositions of address-disjoint separating conjunction to more restrictive compositions with different disjointness conditions; the extension is shown to be strict when fixpoints are present. A composition that is a `unique decomposition' decomposes any given graph uniquely into two parts. An example is the separation between the non-garbage and garbage parts of memory. Alth...
Yifeng Chen, Jeff W. Sanders
Added 14 Oct 2010
Updated 14 Oct 2010
Type Conference
Year 2010
Where MPC
Authors Yifeng Chen, Jeff W. Sanders
Comments (0)
books