Reseña: Relation-algebraic verification of Prim’s minimum spanning tree algorithm

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL titulado Relation-algebraic verification of Prim’s minimum spanning tree algorithm.

Su autor es Walter Guttmann (de la University of Canterbury, Nueva Zelanda).

Su resumen es

We formally prove the correctness of Prim’s algorithm for computing minimum spanning trees. We introduce new generalisations of relation algebras and Kleene algebras, in which most of the proof can be carried out. Only a small part needs additional operations, for which we introduce a new algebraic structure. We instantiate these algebras by matrices over extended reals, which model the weighted graphs used in the algorithm. Many existing results from relation algebras and Kleene algebras generalise from the relation model to the weighted-graph model with no or small changes. The overall structure of the proof uses Hoare logic. All results are formally verified in Isabelle/HOL heavily using its integrated automated theorem provers.

El trabajo se presentará el 24 de octubre en el ICTAC2016 (13th International Colloquium on Theoretical Aspects of Computing).

El código de las correspondientes teorías en Isabelle/HOL se encuentra aquí.