The Floyd-Warshall Algorithm for Shortest Paths

Title:	The Floyd-Warshall Algorithm for Shortest Paths
Authors:	Simon Wimmer and Peter Lammich
Submission date:	2017-05-08
Abstract:	The Floyd-Warshall algorithm [Flo62, Roy59, War62] is a classic dynamic programming algorithm to compute the length of all shortest paths between any two vertices in a graph (i.e. to solve the all-pairs shortest path problem, or APSP for short). Given a representation of the graph as a matrix of weights M, it computes another matrix M' which represents a graph with the same path lengths and contains the length of the shortest path between any two vertices i and j. This is only possible if the graph does not contain any negative cycles. However, in this case the Floyd-Warshall algorithm will detect the situation by calculating a negative diagonal entry. This entry includes a formalization of the algorithm and of these key properties. The algorithm is refined to an efficient imperative version using the Imperative Refinement Framework.
BibTeX:	@article{Floyd_Warshall-AFP, author = {Simon Wimmer and Peter Lammich}, title = {The Floyd-Warshall Algorithm for Shortest Paths}, journal = {Archive of Formal Proofs}, month = may, year = 2017, note = {\url{http://isa-afp.org/entries/Floyd_Warshall.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Depends on:	Refine_Imperative_HOL
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.