Email Gateway (Jul 06 2026 at 16:16): Email Gateway (Jul 06 2026 at 16:16):From: Lawrence Paulson <lp15@cam.ac.uk>
Subject: [isabelle] New in the AFP: Correctness and Complexity of bounded multi-source shortest path
I'm happy to announce a new and remarkably large contribution by ever-productive Arthur Freitas Ramos and his team.
Correctness and Complexity of BMSSP in Isabelle/HOL
Arthur Freitas Ramos, David Barros Hulak and Ruy Jose Guerra Barretto de Queiroz
This development formalizes the bounded multi-source shortest path (BMSSP) algorithm underlying the deterministic directed single-source shortest path algorithm of Duan, Mao, Mao, Shu, and Yin [2]. It proves three explicit claims. First, the executable bmssp_distances computes the exact reachable shortest-distance map for well-formed f inite natural weighted digraphs. Second, a separate costed BMSSP recurrence satisfies the O(mlog2/3 n) bound under the abstract In sert/BatchPrepend/Pull operation-cost interface. Third, the bucketed partition operations realize the primitive costs required by that interface. The formalization does not state a single generated-code machine-step theorem for the executable. The entry also exports executable SML and includes a checked worked shortest-path example whose evaluated output is [(0,0),(1,3),(2,5),(3,8),(4,6)]
https://isa-afp.org/entries/BMSSP_Correctness.html
Last updated: Jul 22 2026 at 14:00 UTC