Formal Verification of Prim’s Algorithm in SPARK

Many distributed systems use a minimum spanning tree (MST) as the backbone of efficient communication within the system. Given its critical role, it is important that the MST be implemented correctly. One way to ensure its correctness with a high degree of confidence is to use formal methods, i.e. mathematically-based tools and approaches for design and verification of software and hardware. Toward this end, we implement Prim’s algorithm for construction of MSTs in SPARK, which is both a programming language and associated set of formal verification tools. At the most basic levels, formal verification in SPARK requires proving that code satisfies contracts on data flow and initialization and is free of run-time errors, which often reveals rare or subtle errors that are hard to detect through testing alone. Once errors are corrected and formal verification is complete, the result is code that is mathematically proven to satisfy the verified properties. In this paper, we provide background on SPARK and describe the process of using it to implement and verify basic properties of MSTs constructed using Prim’s algorithm