A Shape Graph Logic and A Shape System

Analysis and verification of pointer programs are still difficult problems so far. This paper uses a shape graph logic and a shape system to solve these problems in two stages. First, shape graphs at every program point are constructed using an analysis tool. Then, they are used to support the verification of other properties （e.g., orderedness）. Our prototype supports automatic verification of programs manipulating complex data structures such as splay trees, treaps, AVL trees and AA trees, etc. The proposed shape graph logic, as an extension to Hoare logic, uses shape graphs directly as assertions. It can be used in the analysis and verification of programs manipulating mutable data structures. The benefit using shape graphs as assertions is that it is convenient for acquiring the relations between pointers in the verification stage. The proposed shape system requires programmers to provide lightweight shape declarations in recursive structure type declarations. It can help rule out programs that construct shapes deviating from what programmers expect （reflected in shape declarations） in the analysis stage. As a benefit, programmers need not provide specifications （e.g., pre-/post-conditions, loop invariants） about pointers. Moreover, we present a method doing verification in the second stage using traditional Hoare logic rules directly by eliminating aliasing with the aid of shape graphs. Thus, verification conditions could be discharged by general theorem provers.

Shape correspondence for cel animation based on a shape association graph and spectral matching

We present an effective spectral matching method based on a shape association graph for finding region correspondences between two cel animation keyframes.We formulate the correspondence problem as an adapted quadratic assignment problem,which comprehensively considers both the intrinsic geometric and topology of regions to find the globally optimal correspondence.To simultaneously represent the geometric and topological similarities between regions,we propose a shape association graph(SAG),whose node attributes indicate the geometric distance between regions,and whose edge attributes indicate the topological distance between combined region pairs.We convert topological distance to geometric distance between geometric objects with topological features of the pairs,and introduce Kendall shape space to calculate the intrinsic geometric distance.By utilizing the spectral properties of the affinity matrix induced by the SAG,our approach can efficiently extract globally optimal region correspondences,even if shapes have inconsistent topology and severe deformation.It is also robust to shapes undergoing similarity transformations,and compatible with parallel computing techniques.