Relation-algebraic verification of Borůvka's minimum spanning tree algorithm

DOI10.1007/978-3-030-88701-8_14MaRDI QIDQ2695356zbMATH OpenOpenAlexFDO

Authors Walter Guttmann, Nicolas Robinson-O'Brien

Publication date 30 March 2023

Full work available at URL https://doi.org/10.1007/978-3-030-88701-8_14

zbMATH Keywords

algorithm verificationformal methodsKleene algebrasrelation algebrasstone algebrasweighted graphs

Mathematics Subject Classification ID

Theory of computing (68Qxx)

Cites work

• A completeness theorem for Kleene algebras and the algebra of regular events
• A minimum spanning tree algorithm with inverse-Ackermann type complexity
• A randomized linear-time algorithm to find minimum spanning trees
• A relation-algebraic view on evolutionary algorithms for some graph problems
• An \(0(| E|\log\log| V|)\) algorithm for finding minimum spanning trees
• An algebraic framework for minimum spanning tree problems
• Computing tournament solutions using relation algebra and RelView
• scientific article; zbMATH DE number 3936534 (Why is no real title available?)
• scientific article; zbMATH DE number 3501559 (Why is no real title available?)
• scientific article; zbMATH DE number 1210360 (Why is no real title available?)
• scientific article; zbMATH DE number 2110621 (Why is no real title available?)
• scientific article; zbMATH DE number 234018 (Why is no real title available?)
• scientific article; zbMATH DE number 3245483 (Why is no real title available?)
• scientific article; zbMATH DE number 3366846 (Why is no real title available?)
• scientific article; zbMATH DE number 7649972 (Why is no real title available?)
• Isabelle/HOL. A proof assistant for higher-order logic
• On the History of the Minimum Spanning Tree Problem
• On the shortest spanning subtree of a graph and the traveling salesman problem
• Otakar Borůvka on minimum spanning tree problem. Translation of both the 1926 papers, comments, history
• Relation algebras
• Relation-algebraic verification of Prim's minimum spanning tree algorithm
• Sur la liaison et la division des points d'un ensemble fini
• Verifying minimum spanning tree algorithms with Stone relation algebras
• Winskel is (almost) right: Towards a mechanized semantics textbook

Cited in

(1)

• Verifying the Correctness of Disjoint-Set Forests with Kleene Relation Algebras

Describes a project that uses

Uses Software

• RelView
• Isabelle/HOL
• Archive Formal Proofs

This page was built for publication: Relation-algebraic verification of Borůvka's minimum spanning tree algorithm

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2695356)