Dijkstra's Shortest Path Algorithm


Title: Dijkstra's Shortest Path Algorithm
Authors: Benedikt Nordhoff (b /dot/ n /at/ wwu /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.
  author  = {Benedikt Nordhoff and Peter Lammich},
  title   = {Dijkstra's Shortest Path Algorithm},
  journal = {Archive of Formal Proofs},
  month   = jan,
  year    = 2012,
  note    = {\url{https://isa-afp.org/entries/Dijkstra_Shortest_Path.html},
            Formal proof development},
  ISSN    = {2150-914x},
License: BSD License
Depends on: Collections
Used by: Formal_SSA, Koenigsberg_Friendship, 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.