I am currently focused on my PhD research; about verifying Graph Programs.
Graphs are the most natural way to show a complex situation. Graphs can model structures and relations in a 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 of 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 logic. He introduced E-condition and M-condition as assertions for the verification process. The conditions are an extension of nested conditions that were described by Pennemann. However, nested conditions may seem unnatural for readers who are not familiar with it. In addition, there are no tools to support the verification with nested conditions so that it is hard to minimalise human-error.
In my study, I introduce standard logic as assertions for graph program verification. This assertion should be easier to comprehend by the general reader. Also, the existence of tools like Isabelle may help the implementation of the verification with this assertion.