×

On the mechanical derivation of loop invariants. (English) Zbl 0804.68129

Summary: We describe an iterative algorithm for mechanically deriving loop invariants for the purpose of proving the partial correctness of programs. The algorithm is based on resolution and a novel unskolemization technique for deriving logical consequences of first- order formulas. Our method is complete in the sense that if a loop invariant exists for a loop in a given first-order language relative to a given finite set of first-order axioms, then the algorithm produces a loop invariant for that loop which can be used for proving the partial correctness of the program. Existing techniques in the literature are not complete.

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
03B35 Mechanization of proofs and logical operations
68Q60 Specification and verification (program logics, model checking, etc.)
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Caplain, M., Finding invariant assertions for proving programs, (Proc. Intl. Conf. on Reliable Software (1975)), 165-171
[2] Chadha, R., Applications of Unskolemization, Ph.D. dissertation, Dept. of Computer Science, Univ. of North Carolina, Chapel Hill NC 27599-3175 (1991), TR91-027
[3] Chang, C.-L.; Lee, R., Symbolic Logic and Mechanical Theorem Proving (1973), Academic Press: Academic Press New York · Zbl 0263.68046
[4] Cook, S. A., Soundness and completeness of an axiom system for program verification, SIAM J. on Computing, 7, 1, 70-90 (1978) · Zbl 0374.68009
[5] Cooper, D. C., Programs for Mechanical Program Verification, Machine Intelligence, 6, 43-59 (1971) · Zbl 0261.68023
[6] Cousot, P.; Cousot, R., Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, (Fourth ACM Symposium on Principles of Programming (1977)), 238-252
[7] Cox, P. T.; Pietrzykowski, T., A complete, nonredundant algorithm for reversed skolemization, Theoretical Computer Science, 28, 239-261 (1984) · Zbl 0566.03005
[8] Deutsch, L. P., An Interactive Program Verifier, Ph.D. dissertation, Univ. of California at Berkeley (1973)
[9] Dijkstra, E. W., Invariance and non-determinacy, (Hoare, C. A.R.; Shepherdson, J. C., Mathematical Logic and Programming Languages (1985), Prentice-Hall), 157-165 · Zbl 0544.68011
[10] Floyd, R. W., Assigning meanings to programs, (Proceedings of the Symposium on Applied Mathematics. Proceedings of the Symposium on Applied Mathematics, American Mathematical Society, 19 (1967)), 19-32 · Zbl 0189.50204
[11] German, S. M.; Wegbreit, B., A Synthesizer of Inductive Assertions, IEEE Transactions on Software Engg., Vol. SE-1, 1, 68-75 (1975)
[12] Good, D. I.; London, R. L.; Bledsoe, W. W., An Interactive Program Verification System, IEEE Transactions on Software Engg., Vol. SE-1, 1 (1975)
[13] Good, D. I., Mechanical proofs about computer programs, (Hoare, C. A.R.; Shepherdson, J. C., Mathematical Logic and Programming Languages (1985), Prentice-Hall), 55-75 · Zbl 0544.68012
[14] Gries, D., The Science of Programming (1981), Springer-Verlag · Zbl 0472.68003
[15] Katz, S. M.; Manna, Z., A heuristic approach to program verification, (Third Intl. Joint Conf. on Artificial Intelligence (1973)), 500-512
[16] Manna, Z., Mathematical Theory of Computation (1974), McGraw-Hill: McGraw-Hill New York · Zbl 0353.68066
[17] King, J. C., A Program Verifier, Ph.D. dissertation, Carnegie-Mellon University (1969)
[18] Lee, S.-J., CLIN : An Automated Reasoning System Using Clause Linking, Ph.D. dissertation, Dept. of Computer Science, Univ. of North Carolina, Chapel Hill (1990)
[19] Loeckx, J.; Sieber, K., The Foundations of Program Verification (1987), John Wiley and Sons, Ltd. · Zbl 0625.68017
[20] Loveland, D., Automated Theorem Proving, A Logical Basis (1978), North-Holland Publishing Co. · Zbl 0364.68082
[21] McCune, W. W., Un-Skolemizing clause sets, (Information Processing Letters (1988)), 257-263 · Zbl 0709.03007
[22] Robinson, J. A., Machine-oriented Logic based on the Resolution Principle, Journal of the ACM, 12, 1, 23-41 (1965) · Zbl 0139.12303
[23] Seiichiro, D.; Yamaguchi, T., Program Verification System with Synthesizer of Invariant Assertions, Systems and Computers in Japan, 20, 1, 1-13 (1989)
[24] Wand, M., A new incompleteness result for Hoare’s system, Journal of the ACM, 25, 168-175 (1978) · Zbl 0364.68008
[25] Wegbreit, B., Heuristic Methods for Mechanically Deriving Inductive Assertions, (Third Intl. Joint Conf. on Artificial Intelligence (1973))
[26] Wegbreit, B., Property Extraction in Well-Founded Property Sets, IEEE Transactions on Software Engineering, Vol. SE-1, 3, 270-285 (1975)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.