Dijkstra's Shortest Path Algorithm in Isabelle/HOL
Nordhoff Benedikt, Lammich Peter
Sonstige wissenschaftliche VeröffentlichungZusammenfassung
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 zur Publikation
Status: Veröffentlicht
Veröffentlichungsjahr: 2012 (30.01.2012)
Sprache, in der die Publikation verfasst ist: Englisch
Link zum Volltext: http://afp.sourceforge.net/entries/Dijkstra_Shortest_Path.shtml
Stichwörter: Isabelle; HOL; Dijkstra; graph; algorithm; code generation; verified code; theorem proving
Autor*innen der Universität Münster
| Lammich, Peter | Institut für Informatik |
| Nordhoff, Benedikt | Professur für Praktische Informatik (Prof. Müller-Olm) |