A mechanical verification of the stressing algorithm for negative cost cycle detection in networks

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.