Automating proofs of the absence of common runtime errors

ABSTRACT

The Runcheck Verifier is a working system for proving the absence of common runtime errors. The language accepted is Pascal without variant records, side effects in functions, shared variable parameters to procedures, or functional arguments. The errors checked are: 1) accessing a variable that has not been assigned a value, 2) array subscripting out of range, 3) subrange type error, 4) dereferencing a NIL pointer, 5) arithmetic overflow, and 6) division by zero.

REFERENCES

• 1: Nachum Dershowitz , Z Manna, Inference rules for program annotation, Stanford University, Stanford, CA, 1977
• 2: Elspas, B., The Semiautomatic Generation of Inductive Assertions for Proving Program Correctness, Stanford Research Institute, Stanford, Calif., SRI Project 2686, July 1974.
• 3: German, S. M., A System for Automatically Proving the Absence of Common Runtime Errors, Stanford A.I. Memo, in preparation.
• 4: German, S. M. and B. Wegbreit, A Synthesizer of Inductive Assertions, IEEE Trans. on Software Engineering, SE-1, 1 (March 1975), pp.68-75.
• 5: C. A. R. Hoare, Proof of a program: FIND, Communications of the ACM, v.14 n.1, p.39-45, Jan. 1971 [doi>10.1145/362452.362489]
• 6: Hoare, C. A. R. and N. Wirth, An Axiomatic Definition of the Programming Language Pascal, Acta Informatica, Vol. 2, 1973, pp.335-355.
• 7: Huet, G., D. Luckham, and D. Oppen, Extended Pascal Semantics for Proving the Absence of Common Runtime Errors, Stanford A.I. Memo, forthcoming.
• 8: Kathleen Jensen , Niklaus Wirth, Pascal-User Manual and Report, Springer-Verlag New York, Inc., Secaucus, NJ, 1975
• 9: Shmuel Katz , Zohar Manna, Logical analysis of programs, Communications of the ACM, v.19 n.4, p.188-206, April 1976 [doi>10.1145/360032.360048]
• 10: Donald E. Knuth, The art of computer programming, volume 1 (3rd ed.): fundamental algorithms, Addison Wesley Longman Publishing Co., Inc., Redwood City, CA, 1997
• 11: David C. Luckham , Norihisa Suzuki, Automatic program verification V: verification-oriented proof rules for arrays, records and pointers, Stanford University, Stanford, CA, 1976
• 12: Greg Nelson , Derek C. Oppen, A simplifier based on efficient decision algorithms, Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.141-150, January 23-25, 1978, Tucson, Arizona [doi>10.1145/512760.512775]
• 13: Sites, R. L., Proving that Computer Programs Terminate Cleanly, Computer Science Department Report CS 418, Stanford University, May 1974.
• 14: Norihisa Suzuki, Automatic verification of programs with complex data structure., 1976
• 15: Norihisa Suzuki , Kiyoshi Ishihata, Implementation of an array bound checker, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.132-143, January 17-19, 1977, Los Angeles, California [doi>10.1145/512950.512963]
• 16: Ben Wegbreit, The synthesis of loop predicates, Communications of the ACM, v.17 n.2, p.102-113, Feb. 1974 [doi>10.1145/360827.360850]
• 17: Niklaus Wirth, Program development by stepwise refinement, Communications of the ACM, v.14 n.4, p.221-227, April 1971 [doi>10.1145/362575.362577]
• 18: Wirth, N., (the ROOT and SENTINEL program was suggested by N. Wirth).