Formal Verification for High Assurance Software: A Case Study Using the SPARK Auto-Active Verification Toolset

Software is an increasingly integral and sophisticated part of safety- and mission-critical systems. Poorly written software can lead to information leakage, undetected cyber breaches, and even human injury in cases where the software directly interfaces with components of a physical system. These systems may range from power facilities to remotely piloted aircraft. Software bugs and vulnerabilities can lead to severe economic hardships and loss of life in these domains. As fast as software spreads to automate many facets of our lives, it also grows in complexity. The complexity of software systems combined with the nature of the critical domains dependent on those systems results in a need to verify and validate the security and functional correctness of such software to a high level of assurance. The current generation of formal verification tools make it possible to write code with formal, machine-checked proofs of correctness. This thesis demonstrates the process of proving the correctness of code via a formal methods toolchain. It serves as a proof of concept for this powerful method of safety- and mission-critical software development