The Community for Technology Leaders
RSS Icon
Subscribe
Issue No.12 - December (1997 vol.46)
pp: 1304-1312
ABSTRACT
<p><b>Abstract</b>—In this paper, we describe the use of the certification-trail technique as the basis of a hybrid framework for building formally verified software systems. Our technique involves formally verifying only a part of a software system; however, the technique yields a software system which still satisfies the most important correctness properties. Substantial savings in the overhead of software verification, and also in program running time, are shown to be possible in comparison to traditional methods. We apply our technique to the problem of sorting, since sorting represents one of the most basic operations in computer science, and a formally verified sorting certifier should have significant applicability. The results presented in this paper represent an enhancement of the certification-trail technique relative to the detection of incorrect computational output caused by software faults.</p>
INDEX TERMS
Sorting, formal program verification, software correctness, certification trails, program result checking.
CITATION
Jonathan D. Bright, Gregory F. Sullivan, Gerald M. Masson, "A Formally Verified Sorting Certifier", IEEE Transactions on Computers, vol.46, no. 12, pp. 1304-1312, December 1997, doi:10.1109/12.641931
502 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool