Graph Inclusion and Matching Algorithms for Programs Manipulating Singly linked Heaps

Abstract

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.