Dijkstra Shortest Path swMATH ID: 28550 Software Authors: Benedikt Nordhoff; Peter Lammich Description: Dijkstra’s Shortest Path Algorithm. 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. Homepage: https://www.isa-afp.org/entries/Dijkstra_Shortest_Path.html Dependencies: Isabelle Related Software: Isabelle/HOL; Isabelle; HOL; Archive Formal Proofs; Separation Logic; Edmonds-Karp; Gabow SCC; Why3; CAVA LTL Modelchecker; Refinement Monadic; MLton; Isar; Coq; Fiat; Autoref; Locales; CeTA; BEEM; ACL2; Graph Theory Cited in: 9 Publications all top 5 Cited by 11 Authors 5 Lammich, Peter 2 Sefidgar, S. Reza 1 Alkassar, Eyad 1 Böhme, Sascha 1 Lochbihler, Andreas 1 Mehlhorn, Kurt 1 Noschinski, Lars 1 Omodeo, Eugenio Giovanni 1 Rizkallah, Christine 1 Tomescu, Alexandru Ioan 1 Zhan, Bohua Cited in 2 Serials 5 Journal of Automated Reasoning 1 Mathematics in Computer Science Cited in 4 Fields 8 Computer science (68-XX) 4 Combinatorics (05-XX) 2 Operations research, mathematical programming (90-XX) 1 Mathematical logic and foundations (03-XX) Citations by Year