This Article 
 Bibliographic References 
 Add to: 
A Formally Verified Sorting Certifier
December 1997 (vol. 46 no. 12)
pp. 1304-1312

Abstract—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.

[1] G.F. Sullivan and G.M. Masson, "Using Certification Trails to Achieve Software Fault Tolerance," Digest 1990 Fault Tolerant Computing Symp., pp. 423-431, 1990.
[2] G.F. Sullivan and G.M. Masson, "Certification Trails for Data Structures," Digest 1991 Fault Tolerant Computing Symp., pp. 240-247, 1991.
[3] D.S. Wilson, G.F. Sullivan, and G.M. Masson, "Experimental Evaluation of Certification Trails Using Abstract-Data-Type Validation," Proc. 1992 Computer Software and Applications Conf., pp. 300-306, 1992.
[4] G.F. Sullivan, D.S. Wilson, and G.M. Masson, "Certification Trails and Software Design for Testability," Proc. 1993 Int'l Test Conf., pp. 200-209, 1993.
[5] G.F. Sullivan, D.S. Wilson, and G.M. Masson, "Certification of Computational Results," IEEE Trans. Computers, vol. 44, pp. 833-847, 1995.
[6] B.W. Johnson, Design and Analysis of Fault-Tolerant Digital Systems, pp. 394-402. Reading, Mass.: Addison-Wesley, June 1989.
[7] A. Avizienis, "The N-Version Approach to Fault Tolerant Software," IEEE Trans. Software Eng., vol. 11, no. 12, pp. 1,491-1,501, Dec. 1985.
[8] A. Avizienis and J. Kelly, "Fault Tolerance by Design Diversity: Concepts and Experiments," Computer, vol. 17, no. 8, pp. 67-80, Aug. 1984.
[9] L. Chen and A. Avizienis, "N-Version Programming: A Fault Tolerant Approach to Reliability of Software Operation," Digest 1978 Fault Tolerant Computing Symp., pp. 3-9, 1978.
[10] B. Randell, "System Structure for Software Fault Tolerance," IEEE Trans. Software Eng., vol. 1, pp. 220-232, June 1975.
[11] J.D. Bright and G.F. Sullivan, "Checking Mergeable Priority Queues," Digest 24th Symp. Fault-Tolerant Computing, pp. 144-153, June 1994.
[12] M. Blum and S. Kannan,"Designing Programs that Check Their Work," Proc. 21st Symp. Theory of Computing, pp. 86-97, 1989.
[13] R.A. Rubinfeld, "A Mathematical Theory of Self-checking, Self-testing and Self-correcting Programs," PhD thesis, Univ. of California, Berkeley, 1990.
[14] M. Blum and H. Wasserman, "Reflections on the Pentium Division Bug," IEEE Trans. Computers, vol. 45, no. 4, pp. 385-393, Apr. 1996.
[15] S. Purushothaman and P.A. Subrahmanyam, "Mechanical Certification of Systolic Algorithms," J. Automated Reasoning, vol. 5, pp. 67-91, 1989.
[16] R.S. Boyer and J.S. Moore, A Computational Logic.New York: Academic Press, 1979.
[17] R. Boyer and J. Moore, A Computational Logic Handbook. New York: Academic Press, 1988.
[18] M. Kaufmann, "Response to fm91 Survey of Formal Methods: Nqthm and pc-nqthm," Technical Report 75, Computational Logic Inc., Mar. 1992.
[19] J.D. Bright, "Checking and Certifying Computational Results," PhD thesis, Johns Hopkins Univ., 1994.
[20] J. C. Guzmán and P. Hudak, "Single-Threaded Polymorphic Lambda Calculus," Proc. Fifth Ann. IEEE Symp. Logic in Computer Science, pp. 333-343,Philadelphia, June 1990.
[21] F. Honsell, I.A. Mason, S. Smith, and C. Talcott, "A Variable Typed Logic of Effects," Information and Computation, vol. 119, pp. 55-90, 1995.
[22] A.V.S. Sastry, W. Clinger, and Z. Ariola, "Order-of-Evaluation Analysis for Destructive Updates in Strict Functional Languages with Flat Aggregates," Proc. Conf. Functional Programming Languages and Computers, pp. 266-275, 1993.
[23] C.A.R. Hoare, "Quicksort," Computer J., vol. 5, no. 1, pp. 10-15, 1962.
[24] R.S. Boyer and Y. Yu, "Automated Correctness Proofs of Machine Code Programs for a Commercial Microprocessor," Technical Report TR-91-33, Computer Science Dept., Univ. of Texas, Austin, Nov. 1991.

Index Terms:
Sorting, formal program verification, software correctness, certification trails, program result checking.
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, Dec. 1997, doi:10.1109/12.641931
Usage of this product signifies your acceptance of the Terms of Use.