GP2 is a graph transformation rule-based graph programming language that facilitates analysis and verification of programs. Verification of a graph program with GP2 can be done with formal proof in first-order or monadic second-order logic. The process of verifying a graph program tends to be complex if it is done manually. This paper discusses the result of the preliminary analysis of the utilization of Isabelle as a proof assistant to help show the validity of a graph program. This study aims to see how much Isabelle can be used as a proof assistant to verify a graph program in GP2. Experimental results show that complex theory is one of the factors in Isabelle’s failure to prove certain properties. The research results show that Isabelle can verify some properties for graph program verification, but it is limited to certain theories.
Keywords: GP2, graph program, Isabelle, proof assistant