Incorrectness Logic for Graph Programs

TL;DR

This paper introduces an under-approximate program logic for nondeterministic graph programs, enabling deductive reasoning about program incorrectness, which could improve scalability over traditional over-approximate methods.

Contribution

It presents the first sound and complete under-approximate logic for graph programs to reason about bugs and incorrectness.

Findings

Logic is sound and complete for reasoning about graph program incorrectness

Enables deductive proofs of bug presence and finite failures

Potential for scalable bug detection in graph programming

Abstract

Program logics typically reason about an over-approximation of program behaviour to prove the absence of bugs. Recently, program logics have been proposed that instead prove the presence of bugs by means of under-approximate reasoning, which has the promise of better scalability. In this paper, we present an under-approximate program logic for a nondeterministic graph programming language, and show how it can be used to reason deductively about program incorrectness, whether defined by the presence of forbidden graph structure or by finitely failing executions. We prove this incorrectness logic to be sound and complete, and speculate on some possible future applications of it.