# 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{https://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.