Skip to main content
Conference Proceedings

Proof pearl: Dijkstra's shortest path algorithm verified with ACL2

Lecture Notes in Computer Science (2005) 3603 373-384
DOI: 10.1007/11541868_24
8Citations
Citations of this article
7Readers
Mendeley users who have this article in their library.
Get full text

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. © Springer-Verlag Berlin Heidelberg 2005.

Cite

CITATION STYLE

APA

Moore, J. S., & Zhang, Q. (2005). Proof pearl: Dijkstra’s shortest path algorithm verified with ACL2. In Lecture Notes in Computer Science (Vol. 3603, pp. 373–384). Springer Verlag. https://doi.org/10.1007/11541868_24

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free