A formal correctness proof of Boruvka's minimum spanning tree algorithm. (2020)
Type of ContentTheses / Dissertations
Thesis DisciplineComputer Science
Degree NameMaster of Science
PublisherUniversity of Canterbury
AuthorsRobinson-O'Brien, Nicolasshow all
Prior work has described an algebraic framework for proving the correctness of Prim's and Kruskal's minimum spanning tree algorithms. We prove partial correctness of an additional minimum spanning tree algorithm, Boruvka's, using the same framework. Our results are formally veri ed using the automated deduction capabilities of the Isabelle proof assistant. This further demonstrates the suitability of the algebraic framework as a sound abstraction for reasoning about weighted-graph algorithms.