Formal Verification of Prim’s Algorithm in SPARK

Date
2023-01-03
Authors
Wheelhouse, Brian
Hopkinson, Kenneth
Humphrey, Laura
Contributor
Advisor
Department
Instructor
Depositor
Speaker
Researcher
Consultant
Interviewer
Journal Title
Journal ISSN
Volume Title
Publisher
Volume
Number/Issue
Starting Page
6695
Ending Page
Alternative Title
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.
Description
Keywords
Cybersecurity and Software Assurance, formal methods, program verification, spanning trees
Citation
Extent
9
Format
Geographic Location
Time Period
Related To
Proceedings of the 56th Hawaii International Conference on System Sciences
Rights
Attribution-NonCommercial-NoDerivatives 4.0 International
Rights Holder
Email libraryada-l@lists.hawaii.edu if you need this content in ADA-compliant format.