Dijkstra's Shortest Path Algorithm in Isabelle/HOL
Nordhoff Benedikt, Lammich Peter
Other scientific publicationAbstract
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.
Details about the publication
Status: Published
Release year: 2012 (30/01/2012)
Language in which the publication is written: English
Link to the full text: http://afp.sourceforge.net/entries/Dijkstra_Shortest_Path.shtml
Keywords: Isabelle; HOL; Dijkstra; graph; algorithm; code generation; verified code; theorem proving
Authors from the University of Münster
| Lammich, Peter | Institute of Computer Science |
| Nordhoff, Benedikt | Professorship for practical computer science (Prof. Müller-Olm) |