کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
435536 | 1441724 | 2011 | 18 صفحه PDF | دانلود رایگان |
![عکس صفحه اول مقاله: A mechanical verification of the stressing algorithm for negative cost cycle detection in networks A mechanical verification of the stressing algorithm for negative cost cycle detection in networks](/preview/png/435536.png)
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.
Journal: Science of Computer Programming - Volume 76, Issue 7, 1 July 2011, Pages 609–626