Graph Inclusion and Matching Algorithms for Programs Manipulating Singly linked Heaps

Programs that manipulate heaps such as singlylinked lists, doublylinked lists, skiplists, and treesare ubiquitous, and hence ensuring their correctness is of utmost importance. Analysing correctness properties for such programs is not trivial since they induce dynamic data structures, leading to unbounded state spaces with intricate patterns. One approach that has been adopted to tackle this problem is the use of symbolic searching techniques. The state space is encoded using graphs where the nodes represent memory cells, and the edges represent pointers between the cells. It is necessary to prune the search to avoid generating massive numbers of graphs, thus making the procedure unpractical. Pruning strategies are defined based on operations such as graph matching and inclusion. In this paper, a set of algorithms for performing these operations are presented. It is demonstrated that the proposed algorithms can handle typical graphs that arise in the verification of heap manipulating programs.