Languages

Shape Graph Logic and Shape System

strict warning: Only variables should be passed by reference in /var/www/drupal/modules/book/book.module on line 559.

Hoare logic is unsound in the presence of pointers, while separation logic makes automated theorem proving more difficult. We take a new approach in this paper. We combine shape analysis with Hoare-style verification. The analysis creates shape graphs at each program point, including loop invariants. This information is fed to the verification phase to simplify inference rules and reduce the burden on theorem provers. For instance, aliasing can be detected easily from the generated shape graphs and be eliminated by substitution of access paths, which make the use of Hoare logic rules sound.
 
The whole system consists of two parts, namely a shape graph logic (SGL) and a shape system. The shape system requires programmers to provide light-weight shape declarations instead of assertions about pointers. It then generates shape graphs at each program point, and rules out those programs that construct shapes inconsistent with the programmers’ declarations. The succedent verification phase, based on SGL, only considers the well-shaped programs and does not have to worry about the shape invariants of data structures. SGL is an extension to Hoare logic by adding shape graphs as assertions directly, thus information collected from the analysis phase, such as aliasing relations, can be used in the verification. We have implemented a prototype. It supports programs with (circular) singly-/doubly-linked lists and trees, some of which cannot be verified in separation-logic based tools (e.g. Smallfoot).
 
The system work flow of our prototype is shown below.

[Papers]
A Shape Graph Logic and A Shape System   Zhao-Peng Li, Yu Zhang, and Yi-Yun Chen. Journal of Computer Science & Technology, Vol. 28, No. 6, pp. 1063-1084, Nov. 2013. click here
An Automated Program Verifier for PointerC: Design and Implementation (Chinese version) click here
Analysis of Pointer Programs and Inferece of Loop-Invariant Shape Graphs (Chinese version) click here
[Tools]
A Prototype of A Program Verifier for PointerC (including test cases) download here  
Graphviz (software needed to run the demo, version 2.24) download here
 

AttachmentSize
A Shape Graph and A Shape System (Chinese Version).doc558.5 KB