Dijkstra's Shortest Path Algorithm

June 22, 2010 – 6 years, 10 months ago, by reklov

Short Description

Verify implementations of Dijkstra's Algorithm

Submitted by

Volker Klasen <reklov@uni-koblenz.de>


Solution

Tool/Method

KeY + JML

Code/Specification

4 simple (abstract) implementations
1 efficient (concrete) implementation

Link

Solution-problem relationship

Abstract implementations almost fully verified.
For the concrete implementation only the inner loop verified.

Missing proofs due to issues with KeY.

Interactivity, effort needed

For the abstract implementations some to many instantiations (depending on which implementation) are needed, most of them similar to one another. About 1 hour to proof each abstract implementation (when knowing what to do).
Many more interactions needed for concrete implementation. Several hours to proof the inner loop only.

Published

Diploma Thesis (March 2010, Link)

Submitted by

Volker Klasen <reklov@uni-koblenz.de>