Dijkstra's Shortest Path Algorithm

 

Title: Dijkstra's Shortest Path Algorithm
Authors: Benedikt Nordhoff (b_nord01 /at/ uni-muenster /dot/ de) and Peter Lammich
Submission date: 2012-01-30
Abstract: We implement and prove correct Dijkstra's algorithm for the single source shortest path problem, conceived in 1956 by E. Dijkstra. The algorithm is implemented using the data refinement framework for monadic, nondeterministic programs. An efficient implementation is derived using data structures from the Isabelle Collection Framework.
BibTeX:
@article{Dijkstra_Shortest_Path-AFP,
  author  = {Benedikt Nordhoff and Peter Lammich},
  title   = {Dijkstra's Shortest Path Algorithm},
  journal = {Archive of Formal Proofs},
  month   = jan,
  year    = 2012,
  note    = {\url{http://isa-afp.org/entries/Dijkstra_Shortest_Path.shtml},
            Formal proof development},
  ISSN    = {2150-914x},
}
License: BSD License
Depends on: Collections
Used by: Formal_SSA, Koenigsberg_Friendship, Refine_Imperative_HOL