Dijkstra's Shortest Path Algorithm

Benedikt Nordhoff 📧 and Peter Lammich 🌐

January 30, 2012

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

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.

License

BSD License

Topics

Session Dijkstra_Shortest_Path

Depends on

Used by

Cite

× 
@article{Dijkstra_Shortest_Path-AFP,
  author  = {Benedikt Nordhoff and Peter Lammich},
  title   = {Dijkstra's Shortest Path Algorithm},
  journal = {Archive of Formal Proofs},
  month   = {January},
  year    = {2012},
  note    = {\url{https://isa-afp.org/entries/Dijkstra_Shortest_Path.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest

Older releases: