Formalização e Verificação em Coq do Algoritmo de Dijkstra

• João Vitor Fröhlich UFMG
• Karina Girardi Roggia UDESC
• Paulo Henrique Torrens University of Kent

DOI: https://doi.org/10.5753/etc.2024.3163

Resumo

Um assistente de provas é uma ferramenta de software que auxilia no desenvolvimento de provas formais. Dentre as capacidades de um assistente de provas, como o Coq, é possível modelar estruturas complexas, em particular aplicações, que podem ser representadas por meio de provas. Entre essas estruturas, podemos destacar os grafos, contudo não foram encontradas muitas pesquisas sobre a formalização da implementação dos diversos algoritmos que resolvem problemas da teoria de grafos. Assim, para contribuir com a expansão do uso de assistentes de provas na verificação da corretude de algoritmos da teoria de grafos, este trabalho implementa em Coq o algoritmo de Dijkstra e apresenta uma prova parcial de corretude dessa implementação.

Referências

Appel, A. W. (1998). SSA is functional programming. ACM SIGPLAN Notices, 33(4):17–20.

Appel, K. and Haken, W. (1976). Every planar map is four colorable. Bull. Amer. Math. Soc., 82:711–712.

Barras, B., Boutin, S., Cornes, C., Courant, J., Coscoy, Y., Delahaye, D., de Rauglaudre, D., Filliâtre, J.-C., Giménez, E., Herbelin, H., et al. (1999). The Coq proof assistant reference manual. INRIA, version, 6(11).

Bertot, Y. and Castéran, P. (2013). Interactive Theorem Proving and Program Development: Coq’Art: The Calculus of Inductive Constructions. Springer Science & Business Media.

Gonthier, G. (2008). Formal proof–the four-color theorem. Notices of the AMS, 55(11):1382–1393.

Gonthier, G. (2023). A computer-checked proof of the Four Color Theorem. Technical report, INRIA.

Mange, R. and Kuhn, J. (2007). Verifying Dijkstra’s algorithm in Jahob. Technical report, EPFL.

Mohan, A., Leow, W. X., and Hobor, A. (2021). Functional Correctness of C Implementations of Dijkstra’s, Kruskal’s, and Prim’s Algorithms. In Silva, A. and Leino, K. R. M., editors, Computer Aided Verification, pages 801–826, Cham. Springer International Publishing.

Moore, J. S. and Zhang, Q. (2005). Proof pearl: Dijkstra’s shortest path algorithm verified with ACL2. In Theorem Proving in Higher Order Logics: 18th International Conference, TPHOLs 2005, Oxford, UK, August 22-25, 2005. Proceedings 18, pages 373–384. Springer.

Nordhoff, B. and Lammich, P. (2012). Dijkstra’s Shortest Path Algorithm. Archive of Formal Proofs. [link], Formal proof development.