The Specification, Verification, and Implementation of a High-Assurance Data Structure: An ACL2 Approach

We present a complete specification and formal verification of a high-assurance data structure, namely an array-based set (or alternatively, a multiset), of arbitrary size, using the ACL2 theorem prover. This particular data structure is a sanitized version of one that was used in a high-assurance development at Rockwell Collins. We additionally demonstrate how this high-assurance specification can be readily translated to an implementation in a traditional, imperative programming language. The specification is accomplished via the ACL2 single-threaded object (stobj) formulation, as the stobj yields the most straightforward translation to traditional programming language implementations, as well as high-performance, scalable executable specifications within the ACL2 system itself. Use of the stobj is known to present certain difficulties in proof development, but we describe a simple means to access the underlying representation of the stobj, which makes reasoning much more straightforward. We discuss characteristics of ACL2 that aided the proofs, as well as ones that presented challenges. We also compare the ACL2 proof results with other verification efforts previously attempted on this data structure using model checking and symbolic execution.