A Mechanical Verification of the Stressing Algorithm for Negative Cost Cycle Detection in Networks

Abstract

The negative cost cycle detection (NCCD) problem in weighted directed graphs is a fundamental problems in theoretical computer science with applications in a wide range of domains ranging from maximum flows to image segmentation. From the perspective of program verification, this problem is identical to the problem of checking the satisfiability of a conjunction of difference constraints. There exist a number of approaches in the literature for NCCD with each approach having its own set of advantages. Recently, a greedy, space-efficient algorithm called the stressing algorithm was proposed for this problem. In this paper, we present a novel proof of the Stressing algorithm and its verification using the Prototype Verification System (PVS) theorem prover. This example is part of a larger research program to verify the soundness and completeness of a core set of decision procedures.

Research highlights

► We develop a novel proof of correctness for the stressing algorithm.

► This algorithm detects negative cycles in weighted directed graphs.

► Our proof has been verified interactively using the Prototype Verification Systems.

► We present the details of the formal verification of the stressing algorithm.