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

详细信息    查看全文

• 作者：Natarajan Shankar^a ; ^{shankar@csl.sri.com} ; K. Subramani^b ; ^{ksmani@csee.wvu.edu}
• 关键词：Negative cost cycle detection ; Graph algorithms ; Decision algorithms ; Formal verification ; Interactive theorem proving
• 刊名：Science of Computer Programming
• 出版年：2011
• 出版时间：1 July 2011
• 年：2011
• 卷：76
• 期：7
• 页码：609-626
• 全文大小：329 K

文摘

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.