Implementing Order Relations on Graphs

The design of automatic verification methods for programs manipulating dynamic data structures is a challenging problem. We consider programs that operate on a data structures with one next-pointer, such as singly linked lists and circular lists. We refer to such data structures as heaps. We represent a heap as a graph, where vertices in the graph represent cells in the heap. To test that a program is safe, we should check that the out put of this program is well formed and is sorted. The aim of this project is to design a number of algorithms to test the different orderings between graphs which arise when including heaps. More precisely, given two graphs, G1 and G2, we check that G1 can be included in G2, using different type of orderings