Abstract: 
The FloydWarshall 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 allpairs
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 FloydWarshall 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_WarshallAFP,
author = {Simon Wimmer and Peter Lammich},
title = {The FloydWarshall Algorithm for Shortest Paths},
journal = {Archive of Formal Proofs},
month = may,
year = 2017,
note = {\url{http://isaafp.org/entries/Floyd_Warshall.html},
Formal proof development},
ISSN = {2150914x},
}
