Ph.D. Theses

Automated Verification of Generic Computer Software Components

By Robert E. Cook, Jr.
Advisor: David Musser
December 19, 1997

The current trend in software engineering is for larger, more complicated, systems that run critical applications. For these applications, software testing is often insufficient, and often is performed using a ``hit or miss'' approach. Formal verification would provide greater assurance, but is typically not applied. One reason why it is not applied is that significant knowledge of, and experience with, computer-assisted theorem provers is often required. A second reason why it is not applied is the amount of time required to perform a verification.

In our research, we have developed a framework for formal verification of software utilizing PVS. We have created a set of axioms to symbolically execute functions, and have formed a representation for the formal specifications. The axioms, combined with a set of user-defined proof strategies, permit a formal verification to be performed by issuing only one command to the theorem prover. Therefore, to perform a formal verification, the engineer is not required to have extensive knowledge of the theorem prover. The framework we have developed was designed to be capable of formally verifying generic functions. Therefore, even though the time to formally specify a function for use by the verification system can be substantial, the time involved can be amortized over the many expected instantiations of the generic function.

The generic functions we have formally verified come from the C++ Standard Template Library, part of the new ANSI/ISO C++ standard. Of greatest significance, we have formally verified the correctness of the insert_aux member function of the vector container class. To perform such verifications, concepts such as memory references, iterators and iterator concepts, manipulation of array data, and dynamic memory allocation needed to be addressed. While the system is not without limitations and the time involved in performing the verification can be sizable, we believe that a system specifically designed for formal verifications, based on our framework, could realistically be applied to formally verifying functions that are expected to experience significant levels of reuse or that require ultra-high assurance.

Return to main PhD Theses page