Verifying Monadic Second-Order Properties of Graph Programs

TL;DR

This paper extends assertion languages for graph programs to express monadic second-order properties, enabling verification of global graph properties like acyclicity and connectivity.

Contribution

It introduces a weakest liberal precondition construction for monadic second-order assertions, facilitating formal verification of complex graph properties.

Findings

Extended nested graph conditions to match monadic second-order logic.

Developed a precondition construction for verifying global graph properties.

Demonstrated verification of non-local correctness specifications.

Abstract

The core challenge in a Hoare- or Dijkstra-style proof system for graph programs is in defining a weakest liberal precondition construction with respect to a rule and a postcondition. Previous work addressing this has focused on assertion languages for first-order properties, which are unable to express important global properties of graphs such as acyclicity, connectedness, or existence of paths. In this paper, we extend the nested graph conditions of Habel, Pennemann, and Rensink to make them equivalently expressive to monadic second-order logic on graphs. We present a weakest liberal precondition construction for these assertions, and demonstrate its use in verifying non-local correctness specifications of graph programs in the sense of Habel et al.