This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
A Set of Inference Rules for Quantified Formula Handling and Array Handling in Verification of Programs Over Integers
November 1989 (vol. 15 no. 11)
pp. 1368-1381

Because of the undecidability problem of program verification, it becomes necessary for an automated verifier to seek human assistance for proving theorems which fall beyond its capability. In order that the user be able to interact smoothly with the machine, it is desired that the theorems be maintained and processed by the prover in a form as close as possible to the popular algebraic notation. Motivated by the need of such an automated verifier, which works in an environment congenial to human participation and at the same time uses the methodologies of resolution provers of first-order logic, some inference rules have previously been proposed by the authors for integer arithmetic, and their completeness issues have been discussed. In the present work, the authors examine how these rules can be applied to quantified formulas vis-a-vis verification of programs involving arrays. An interesting situation, referred to as bound-extension, has been found to occur frequently in proving the quantified verification conditions of the paths in a program. A novel rule, called bound-extension rule, has been devised to consolidate and depict the various issues involved in a bound-extension process. It has been proved that the rule set proposed previously by the authors is adequate for handling a more general phenomenon, called bound-modification, which covers bound-extension in all its entirety.

[1] Z. Manna,Mathematical Theory of Computation. New York: McGraw-Hill, 1974.
[2] J. C. King, "A program verifier," Ph.D. dissertation, Carnegie-Mellon Univ., 1970.
[3] J. V. Majitsevic, "Enumerable sets are diophantine,"Sov. Math. Dokl., vol. 11, no. 2, pp. 354-358, 1970.
[4] D. I. Good, "Toward a man-machine system for proving program correctness," Ph.D. dissertation, Univ. Wisconsin, 1970.
[5] L. P. Deutsch, "An interactive program verifier," Ph.D. dissertation, Univ. California, Berkeley, 1973.
[6] W. W. Bledsoe and P. Bruell, "A man-machine theorem proving system,"Artificial Intell., vol. 5, no. 1, pp. 51-72, 1974.
[7] D. I. Good, R. L. London, and W. W. Bledsoe, "An interactive program verification systems,"IEEE Trans. Software Eng., vol. SE- 1, no. 1, pp. 59-67, 1975.
[8] M. S. Moriconi, "A designer/verifier's assistant,"IEEE Trans. Software Eng., vol. SE-5, no. 4, pp. 387-402, 1979.
[9] C. L. Chang and R. C. T. Lee,Symbolic Logic and Mechanical Theorem Proving. New York: Academic, 1973.
[10] J. A. Robinson, "A machined-oriented logic based on the resolution principle,"J. Assoc. Comput. Mach., vol. 12, no. 1, pp. 23-41, Jan. 1965.
[11] J. A. Robinson, "Generalized resolution principle " inMachine Intelligence, vol. 3, D. Michie, Ed. New York: American Elsevier, 1968, pp. 77-94.
[12] G. A. Robinson and L. Wos, "Paramodulation and theorem proving in first-order theories with equality," inMachine Intelligence 4, B. Meltzer and D. Michie, Eds. New York: American Elsevier, 1969, pp. 135-150.
[13] L. Wos, G. A. Robinson, and D. F. Carson, "Efficiency and completeness of the set of support strategy in theorem proving,"J. ACM, vol. 12, pp. 536-541, 1965.
[14] W. W. Bledsoe, "Splitting and reduction heuristics in automatic theorem proving,"Artificial Intell., vol. 2, no. 1, pp. 55-77, 1971.
[15] R. S. Boyer, "Locking: A restriction of resolution," Ph.D. dissertation, Univ. Texas at Austin, 1971.
[16] C. L. Chang and J. R. Slagle, "Completeness of linear resolution for theories with equality,"J. ACM, vol. 18, no. 1, pp. 126-136, 1971.
[17] D. Luckham and N. J. Nilson, "Extracting information from resolution proof trees,"Artificial Intell., vol. 2, no. 1, pp. 27-54, 1971.
[18] R. C. T. Lee, "Fuzzy logic and the resolution principle,"J. ACM, vol. 19, no. 1, pp. 109-119, Jan. 1972.
[19] J. R. Slagle--"Automated theorem proving with renamable and semantic resolution,"J. ACM, vol. 14, pp. 687-697, 1967.
[20] J. R. Slagle, "An approach for finding C-linear complete inference systems,"J. ACM, vol. 19, pp, 496-516, 1972.
[21] J. R. Slagle, Automated theorem proving with built-in theories,"J. ACM, vol. 19, pp. 120-135, Jan. 1972.
[22] J. R. Slagle and L. M. Norton, "Experiments with an automated theorem prover having partial ordering inference rules,"Commun. ACM, vol. 16, pp. 682-688, 1973.
[23] J. R. Stagle and L. M. Norton, "Automated theorem proving for the theories of partial ordering,"Comput. J., vol. 18, no. 1, pp. 49-54, 1975.
[24] D. Brand, "Analytic resolution in theorem proving,"Artificial Intell., vol. 7, no. 4, pp. 285-318, 1976.
[25] D. J. Lawrence and J. D. Starkey, "Experimental tests of resolution-based theorem proving strategies,"Inform. Sci., vol. 10, pp. 131- 154, 1976.
[26] C. M. Harrison and N. Rubin, "Author generalization of resolution,"J. ACM, vol. 25, no. 3, pp. 341-352, 1978.
[27] F. M. Brown, "Towards the automation of set theory and its logic,"Artificial Intell., vol. 10, no. 3, pp. 281-316, 1978.
[28] D. A. Plaisted, "Theorem proving with abstraction,"Artificial Intell., vol. 16, no. 1, pp. 47-108, 1981.
[29] M. E. Stickel, "A non-clausal connection graph resolution theorem proving program," inProc. Nat. Conf. Artificial Intelligence, Pittsburgh, PA, 1982, pp. 229-233.
[30] N. V. Murray, "Completely non-clausal theorem proving,"Artificial Intell., vol. 18, pp. 67-85, 1982.
[31] Z. Manna and R. Waldinger, "Deduction with relation matching," inProc. Fifth Conf. Foundations of Software Technology and Theoretical Computer Science, New Delhi, (Lecture Notes in Computer Science 206), G. Goos and J. Hartmanis, Eds. New York: Springer-Verlag, 1985, pp. 212-224.
[32] J. Hsiang "Refutational theorem proving using term-rewriting systems,"Artificial Intell., pp. 255-300, 1985.
[33] D. Sarkar and S. C. De Sarkar, "Some inference rules for integer arithmetic for verification of flowchart programs on integers,"IEEE Trans. Software Eng., vol. 15, no. 1, pp. 1-9, Jan. 1989.
[34] J. McCarthey, "A basis for a mathematical theory of computation," inComputer Programming and Formal Systems, P. Braffort and D. Hirschberg, Eds. Amsterdam, The Netherlands: North-Holland, 1963, pp. 33-70.
[35] D. Kaplan, "Some completeness results in the mathematical theory of computation,"J. ACM, vol. 15, no. 1, pp. 124-134, 1968.
[36] R. W. Floyd, "Assigning meanings to programs," inProc. Symp. Appl. Math., vol. 19 (Mathematical Aspects of Computer Science), J. T. Schwartz, Ed., Amer. Math. Soc., Providence, RI, 1967, pp. 19-32.

Index Terms:
inference rules; quantified formula handling; array handling; undecidability problem; program verification; automated verifier; first-order logic; integer arithmetic; quantified formulas; bound-extension rule; bound-modification; decidability; inference mechanisms; program verification; theorem proving
Citation:
D. Sarkar, S.C. De Sarkar, "A Set of Inference Rules for Quantified Formula Handling and Array Handling in Verification of Programs Over Integers," IEEE Transactions on Software Engineering, vol. 15, no. 11, pp. 1368-1381, Nov. 1989, doi:10.1109/32.41330
Usage of this product signifies your acceptance of the Terms of Use.