Requiem for a Bug – Verifying Software, Part 2: Formal Verification through SPARK 2014 (.PDF Download)

This article is part of the Embedded Software Series: Enforced Coding Using Ada Contracts

Read this article online

In our previous article (“Requiem for a Bug—Verifying Software: Testing and Static Analysis”), we presented a sample Ada program to perform a binary search of a sorted array, and we used both traditional testing and the CodePeer static analysis tool to locate bugs. Let's now move to formal verification using SPARK 2014 technology...