Graph is the most natural way in showing complex situation. Graphs can model structures and relations in simple way so that it can be used to model many practical problems. The use of graph theory in solving many practical problems motivated the development and study about algorithms that operate on graphs. One widely studied about this is graph transformation, which has a lot of applications such as programs for manipulating pointer. Graph Transformation also can simulate Chomsky Graph Grammar and Turing Machine, which show that it is a powerful theory in Computer Science.

There is a non-deterministic programming language for computing by graph transformation, called GP (Graph Programs) that is described in Christopher Bak’s thesis. It has a simple syntax but it is also can program every computable function on graphs. This programming language is designed to facilitate formal reasoning about programs.

In 2013, Christopher M. Poskitt in his thesis shows reasoning of graph programs based on Hoare logics. Graph based Hoare logic also used for reasoning about object-oriented programs by Liang Zhao et.al. . Deltef Plump then shows reasoning of graph programs using standard mathematical language for expressing assertions and proofs.

It then comes to an idea that this project will develop the study of reasoning about graph programs. Separation logic is one idea that is likely to give a good result in this area. Separation logic itself is an extension of Hoare logic, which is a way of reasoning about programs. Separation logic can be used to specify graph classes and verifying graph transformation.