Dijkstra Shortest Path

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.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element

References in zbMATH (referenced in 9 articles )

Showing results 1 to 9 of 9.
Sorted by year (citations)

  1. Lammich, Peter: Refinement to imperative HOL (2019)
  2. Lammich, Peter; Lochbihler, Andreas: Automatic refinement to efficient data structures: a comparison of two approaches (2019)
  3. Lammich, Peter; Sefidgar, S. Reza: Formalizing network flow algorithms: a refinement approach in Isabelle/HOL (2019)
  4. Zhan, Bohua: Efficient verification of imperative programs using auto2 (2018)
  5. Lammich, Peter; Sefidgar, S. Reza: Formalizing the Edmonds-Karp algorithm (2016)
  6. Lammich, Peter: Refinement to Imperative/HOL (2015)
  7. Noschinski, Lars: A graph library for Isabelle (2015)
  8. Alkassar, Eyad; Böhme, Sascha; Mehlhorn, Kurt; Rizkallah, Christine: A framework for the verification of certifying computations (2014)
  9. Omodeo, Eugenio G.; Tomescu, Alexandru I.: Set graphs. III: Proof pearl: Claw-free graphs mirrored into transitive hereditarily finite sets (2014)