Formal Verification of Prim’s Algorithm in SPARK

Document Type

Conference Proceeding

Publication Date

1-2023

Abstract

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.

Comments

The "Link to Full Text" on this page opens or loads the PDF of the conference paper, hosted at the conference series website.

Published under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International license (CC BY-NC-ND 4.0)

DOI

https://hdl.handle.net/10125/103443

Source Publication

Proceedings of the Annual Hawaii International Conference on System Sciences 2023

Link to Full Text

Share

COinS