Michael Nagel 

Karlsruhe Institute of Technology, Studienarbeit, 2012

In this thesis we apply bounded program verification techniques to an implementation of Dijkstra’s Algorithm optimized for execution speed.

Bounded program verification is a formal technique to build confidence in the correctness of a computer program. All possible inputs in a user-defined scope are guaranteed to be checked, but no statement is made about inputs outside the bounds. Dijkstra’s Algorithm is a well-known algorithm to calculate shortest paths in graphs. One of its applications is in route planning to search the shortest route from Karlsruhe to Berlin in a graph representation of the European road network. The algorithm utilizes a priority queue often implemented using a binary heap.

We port Julian Delling’s implementation of Dijkstra’s Algorithm to Java because we use JForge and InspectJ for bounded program verification. This way we are able to verify important properties of the underlying BinaryHeap data structure. We report a bug in the implementation undiscovered by previous testing. Furthermore, we find two more bugs in our untested Java port of the codebase. We also discover many implicit assumptions on the implementation level.

The aforementioned results were obtained by a modular bottom-up approach. Originally, we used a top-down approach, characterizing valid inputs and criteria for correct outputs. We intended to verify the correctness of an implementation of Dijkstra’s Algorithm within a bounded scope and increase the scope as far as possible without specifying the internals. Top-down verification of the FlatBaseDijkstra.run() method that calculates the shortest path between nodes in a graph did not succeed for several reasons: performance issues, complex analysis of counterexamples, and optimized code not created with verification in mind.

The analyzed implementation of Dijkstra’s Algorithm was not specially created to be easy to verify; it uses complex data structures for the priority queue and graph representation and implements different optimization techniques important for real-world usage. For example, memory layout is taken into consideration in order to minimize cache footprint.