Verifying Graph Programs with First-Order Logic (Extended Version)

TL;DR

This paper introduces a method for verifying graph programs in GP 2 using standard first-order logic, making formal verification more accessible and applicable to complex, loop-free graph programs.

Contribution

It presents a novel approach to verify GP 2 programs with first-order logic, extending previous methods to handle a broader class of programs including nested loops.

Findings

Allows reasoning about a wider class of graph programs

Enables verification of nested loop programs

Constructs strongest liberal postconditions for program verification

Abstract

We consider Hoare-style verification for the graph programming language GP 2. In previous work, graph properties were specified by so-called E-conditions which extend nested graph conditions. However, this type of assertions is not easy to comprehend by programmers that are used to formal specifications in standard first-order logic. In this paper, we present an approach to verify GP 2 programs with a standard first-order logic. We show how to construct a strongest liberal postcondition with respect to a rule schema and a precondition. We then extend this construction to obtain strongest liberal postconditions for arbitrary loop-free programs. Compared with previous work, this allows to reason about a vastly generalised class of graph programs. In particular, many programs with nested loops can be verified with the new calculus.