|
| This Article | ||
| ||
| Share | ||
| Bibliographic References | ||
| Add to: | ||
 Digg  Furl  Spurl  Blink  Simpy  Google  Del.icio.us  Y!MyWeb | ||
| Search | ||
| ||
| ASCII Text | x | ||
| 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. | |||
| BibTex | x | ||
| @article{ 10.1109/12.641931, author = {Jonathan D. Bright and Gregory F. Sullivan and Gerald M. Masson}, title = {A Formally Verified Sorting Certifier}, journal ={IEEE Transactions on Computers}, volume = {46}, number = {12}, issn = {0018-9340}, year = {1997}, pages = {1304-1312}, doi = {http://doi.ieeecomputersociety.org/10.1109/12.641931}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, } | |||
| RefWorks Procite/RefMan/Endnote | x | ||
| TY - JOUR JO - IEEE Transactions on Computers TI - A Formally Verified Sorting Certifier IS - 12 SN - 0018-9340 SP1304 EP1312 EPD - 1304-1312 A1 - Jonathan D. Bright, A1 - Gregory F. Sullivan, A1 - Gerald M. Masson, PY - 1997 KW - Sorting KW - formal program verification KW - software correctness KW - certification trails KW - program result checking. VL - 46 JA - IEEE Transactions on Computers ER - | |||
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.