A formal correctness proof of Boruvka's minimum spanning tree algorithm.

dc.contributor.author	Robinson-O'Brien, Nicolas
dc.date.accessioned	2020-10-14T00:44:51Z
dc.date.available	2020-10-14T00:44:51Z
dc.date.issued	2020	en
dc.description.abstract	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.	en
dc.identifier.uri	https://hdl.handle.net/10092/101132
dc.identifier.uri	http://dx.doi.org/10.26021/10196
dc.language	English
dc.language.iso	en
dc.publisher	University of Canterbury	en
dc.rights	All Right Reserved	en
dc.rights.uri	https://canterbury.libguides.com/rights/theses	en
dc.title	A formal correctness proof of Boruvka's minimum spanning tree algorithm.	en
dc.type	Theses / Dissertations	en
thesis.degree.discipline	Computer Science	en
thesis.degree.grantor	University of Canterbury	en
thesis.degree.level	Masters	en
thesis.degree.name	Master of Science	en
uc.bibnumber	2957908	en
uc.college	Faculty of Engineering	en

Now showing 1 - 1 of 1