Dijkstra's Shortest Path Algorithm Verified with ACL2

J Strother Moore
Qiang Zhang
Department of Computer Sciences
University of Texas at Austin


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.