
This Article  
 
Share  
Bibliographic References  
Add to:  
Digg Furl Spurl Blink Simpy Del.icio.us Y!MyWeb  
Search  
 
ASCII Text  x  
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. 13681381, November, 1989.  
BibTex  x  
@article{ 10.1109/32.41330, author = {D. Sarkar and S.C. De Sarkar}, title = {A Set of Inference Rules for Quantified Formula Handling and Array Handling in Verification of Programs Over Integers}, journal ={IEEE Transactions on Software Engineering}, volume = {15}, number = {11}, issn = {00985589}, year = {1989}, pages = {13681381}, doi = {http://doi.ieeecomputersociety.org/10.1109/32.41330}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }  
RefWorks Procite/RefMan/Endnote  x  
TY  JOUR JO  IEEE Transactions on Software Engineering TI  A Set of Inference Rules for Quantified Formula Handling and Array Handling in Verification of Programs Over Integers IS  11 SN  00985589 SP1368 EP1381 EPD  13681381 A1  D. Sarkar, A1  S.C. De Sarkar, PY  1989 KW  inference rules; quantified formula handling; array handling; undecidability problem; program verification; automated verifier; firstorder logic; integer arithmetic; quantified formulas; boundextension rule; boundmodification; decidability; inference mechanisms; program verification; theorem proving VL  15 JA  IEEE Transactions on Software Engineering ER   
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 firstorder 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 visavis verification of programs involving arrays. An interesting situation, referred to as boundextension, has been found to occur frequently in proving the quantified verification conditions of the paths in a program. A novel rule, called boundextension rule, has been devised to consolidate and depict the various issues involved in a boundextension process. It has been proved that the rule set proposed previously by the authors is adequate for handling a more general phenomenon, called boundmodification, which covers boundextension in all its entirety.
[1] Z. Manna,Mathematical Theory of Computation. New York: McGrawHill, 1974.
[2] J. C. King, "A program verifier," Ph.D. dissertation, CarnegieMellon Univ., 1970.
[3] J. V. Majitsevic, "Enumerable sets are diophantine,"Sov. Math. Dokl., vol. 11, no. 2, pp. 354358, 1970.
[4] D. I. Good, "Toward a manmachine 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 manmachine theorem proving system,"Artificial Intell., vol. 5, no. 1, pp. 5172, 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. 5967, 1975.
[8] M. S. Moriconi, "A designer/verifier's assistant,"IEEE Trans. Software Eng., vol. SE5, no. 4, pp. 387402, 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 machinedoriented logic based on the resolution principle,"J. Assoc. Comput. Mach., vol. 12, no. 1, pp. 2341, Jan. 1965.
[11] J. A. Robinson, "Generalized resolution principle " inMachine Intelligence, vol. 3, D. Michie, Ed. New York: American Elsevier, 1968, pp. 7794.
[12] G. A. Robinson and L. Wos, "Paramodulation and theorem proving in firstorder theories with equality," inMachine Intelligence 4, B. Meltzer and D. Michie, Eds. New York: American Elsevier, 1969, pp. 135150.
[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. 536541, 1965.
[14] W. W. Bledsoe, "Splitting and reduction heuristics in automatic theorem proving,"Artificial Intell., vol. 2, no. 1, pp. 5577, 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. 126136, 1971.
[17] D. Luckham and N. J. Nilson, "Extracting information from resolution proof trees,"Artificial Intell., vol. 2, no. 1, pp. 2754, 1971.
[18] R. C. T. Lee, "Fuzzy logic and the resolution principle,"J. ACM, vol. 19, no. 1, pp. 109119, Jan. 1972.
[19] J. R. Slagle"Automated theorem proving with renamable and semantic resolution,"J. ACM, vol. 14, pp. 687697, 1967.
[20] J. R. Slagle, "An approach for finding Clinear complete inference systems,"J. ACM, vol. 19, pp, 496516, 1972.
[21] J. R. Slagle, Automated theorem proving with builtin theories,"J. ACM, vol. 19, pp. 120135, 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. 682688, 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. 4954, 1975.
[24] D. Brand, "Analytic resolution in theorem proving,"Artificial Intell., vol. 7, no. 4, pp. 285318, 1976.
[25] D. J. Lawrence and J. D. Starkey, "Experimental tests of resolutionbased 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. 341352, 1978.
[27] F. M. Brown, "Towards the automation of set theory and its logic,"Artificial Intell., vol. 10, no. 3, pp. 281316, 1978.
[28] D. A. Plaisted, "Theorem proving with abstraction,"Artificial Intell., vol. 16, no. 1, pp. 47108, 1981.
[29] M. E. Stickel, "A nonclausal connection graph resolution theorem proving program," inProc. Nat. Conf. Artificial Intelligence, Pittsburgh, PA, 1982, pp. 229233.
[30] N. V. Murray, "Completely nonclausal theorem proving,"Artificial Intell., vol. 18, pp. 6785, 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: SpringerVerlag, 1985, pp. 212224.
[32] J. Hsiang "Refutational theorem proving using termrewriting systems,"Artificial Intell., pp. 255300, 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. 19, 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: NorthHolland, 1963, pp. 3370.
[35] D. Kaplan, "Some completeness results in the mathematical theory of computation,"J. ACM, vol. 15, no. 1, pp. 124134, 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. 1932.