Dijkstra's Shortest Path Algorithm Verified with ACL2
J Strother Moore
and
Qiang Zhang
Department of Computer Sciences
University of Texas at Austin
Abstract
We briefly describe a mechanically checked proof of
Dijkstra's shortest path algorithm for finite directed graphs with
nonnegative edge lengths. The algorithm and proof are formalized
in ACL2.