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.shtml},
            Formal proof development},
  ISSN    = {2150-914x},
}
License: BSD License
Depends on: Refine_Imperative_HOL