Dijkstra's Shortest Path Algorithm

Benedikt Nordhoff 📧 and Peter Lammich 🌐

January 30, 2012

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