Paper Info
Title
The Specification, Verification, and Implementation of a High-Assurance Data Structure: An ACL2 Approach
Abstract
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.
Year
DOI
Venue
2013
10.1109/HICSS.2013.541
HICSS
Keywords
Field
DocType
theorem proving,formal specification,formal verification,data structures
Specification language,Programming language,Programming language specification,Computer science,Runtime verification,Theoretical computer science,Formal specification,Verification,Language Of Temporal Ordering Specification,Formal methods,Formal verification
Conference
ISSN
Citations 
PageRank 
1060-3425
0
0.34
References 
Authors
4
1
Name
Order
Citations
PageRank
David S. Hardin1273.90