Patent
1997-04-25
1999-10-05
Hafiz, Tariq R.
395701, 395707, 395708, G06F 944
Patent
active
059637390
ABSTRACT:
A computer-implemented method, apparatus, and article of manufacture for verifying the total correctness of a computer program with mutually recursive procedures. A computer program is received into the computer as a series of source statements, wherein the source statements include annotations indicating the intended behavior of the source statements. The source statements are translated into an abstract syntax tree and a call graph of the program in the computer, wherein the call graph includes nodes representing procedures and directed arcs between the nodes representing procedure calls. The abstract syntax tree and call graph are analyzed for correctness by invoking a Verification Condition Generator in the computer to generate a set of verification conditions from the abstract syntax tree and call graph. The set of verification conditions are outputted as conditions to be proven to complete a proof of total correctness of the program. The set of verification conditions are verified in the computer and a theorem is outputted showing that the program is totally proven to be totally correct with respect to its specification based on the set of verification conditions.
REFERENCES:
patent: 4860203 (1989-08-01), Corrigan et al.
patent: 5481717 (1996-01-01), Gaboury
"Task dependence and Termination in Ada", Dillon ACM Trans. on Soft. Engg. and Methodology, vol. 6, No.1, pp. 80-110, Jan. 1997.
Kurshan, "The Complexity of Verification", STOC '94 Proc. of the twenty-sixth annual ACM Symp. on Theory of Computer, pp. 365-371, May 1994.
Rosenblum, "Towards a Method of Programming with Assertions",ICSE '92, pp. 92-104, 1992.
Hungar, "Complexity bounds of Hoare-style Proof Systems", LICS '91, IEEE, pp. 120-126, Jul. 1991.
Mills, "Certifying the Correctness of Software", IEEE, pp. 373-381, Jan. 1992.
Lindsay et al. "Using CARE to Constant Verified Software", Proc. First IEEE Int'l Conf. on Format Engg. Methods, pp. 122-131, Apr. 1997.
"Proof of a Program: FIND", C. A. R. Hoare, Communications of the ACM, vol. 14, No. 1, Jan. 1971, pp. 39-45.
"Proof of a recursive program: Quicksort," M. Foley et al., The Computer Journal, vol. 14, No. 4, Jan. 1971, pp. 391-395.
"A Pedagogical Verification Condition Generator", D. Gray, The Computer Journal, vol. 30, No. 3, Jun. 1987, pp. 239-248.
"Automatic Program Verification I: A Logical Basis and Its Implementation", Shigeru Igarashi et al., Acta Informatica 4, 1975, pp. 145-182.
"Experience with embedding hardware description languages in HOL", Richard Boulton et al., Theorem Provers in Circuit Design, edited by V. Stavridou et all., Elsevier Science Publishes B V. (North Holland), 1992, 129-156.
"Total Correctness for Procedures", Stefan Sokolowski, Proceedings of 6th Symposium on Mathematical Foundations of Computer Science, Tatranska Lomnica, Sep. 5-9, 1977, pub. in Lecture Notes in Computer Science 53, edited by G. Goos et al., 1977, pp. 475-483.
"Ten years of Hoare's Logic: A Survey--Part I", K. R. Apt, ACM Transactions on Programming Languages and Systems, vol. 3, No. 4, Oct. 1981, pp. 431-483.
"Proving Total Correctness of Recursive Procedures", P. America et al., Information and Computation, vol. 84, No. 2, Feb. 1990, pp. 129-162.
"A Structure-directed Total Correctness Proof Rule for Recursive Procedure Calls", P. Pandya et al., The Computer Journal, vol. 29, No. 6, 1986, pp. 531-537.
"A Mechanically Verified Verification Condition Generator", P. Homeier et al., The Computer Journal, vol. 38, No. 2, 1995, pp. 1-11.
"Mechanical Verification of Mutually Recursive Procedures", P. Homeier et al., Proceedings of the 13th International Conference on Automated Deduction (CADE-13), eds. M.A. McRobbie et al., Rutgers University, New Brunswick, NJ, USA, Jul. 30-Aug. 3, 1996, Lecture Notes in Artificial Intelligence vol. 1104, Springer-Verlag, pp. 201-215.
"Automated Verification Condition Generation using Intermittent Assertions", D. Smallberg, M.S. thesis, Department of Computer Science, University of California at Los Angeles, 1978.
Winskel, Glynn, The Formal Semantics of Programming Languages, An Introduction, MIT Press, Cambridge, Massachusetts, 1993, 361 pages ISBN 0-262-23169-7.
Apt, Krzysztof R. and Olderog, Ernst-Rudiger, Verification of Sequential and Concurrent Programs, Second Edition, Springer-Verlag, New York, 1997. 364 pages, ISBN 0-387-94896-1.
Gordon, M.J.C., and Melham, T.F., Introduction to HOL, A Theorem Proving Environment for Higher Order Logic, Cambridge University Press, 1993, 472 pages, ISBN 0-521-44189-7.
Chaki Kakali
Hafiz Tariq R.
Homeier Peter V.
LandOfFree
Method for verifying the total correctness of a program with mut does not yet have a rating. At this time, there are no reviews or comments for this patent.
If you have personal experience with Method for verifying the total correctness of a program with mut, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Method for verifying the total correctness of a program with mut will most certainly appreciate the feedback.
Profile ID: LFUS-PAI-O-1181781