2005 | OriginalPaper | Chapter
Proof Pearl: Dijkstra’s Shortest Path Algorithm Verified with ACL2
Authors : J. Strother Moore, Qiang Zhang
Published in: Theorem Proving in Higher Order Logics
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
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.