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

DOI10.1016/j.scico.2010.08.002zbMath1215.68071OpenAlexW2046514810MaRDI QIDQ532429

Natarajan Shankar, K. Subramani and Vahan Mkrtchyan

Publication date: 4 May 2011

Published in: Science of Computer Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.scico.2010.08.002

zbMATH Keywords

formal verificationgraph algorithmsinteractive theorem provingdecision algorithmsnegative cost cycle detection

Mathematics Subject Classification ID

Graph theory (including graph drawing) in computer science (68R10) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Uses Software

• PVS

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Temporal constraint networks
• Towards mechanical metamathematics
• A zero-space algorithm for negative cost cycle detection in networks
• Verifying and Reflecting Quantifier Elimination for Presburger Arithmetic
• A new approach to dynamic all pairs shortest paths
• Fast and Flexible Difference Constraint Propagation for DPLL(T)

This page was built for publication: A mechanical verification of the stressing algorithm for negative cost cycle detection in networks