×

On invariant checking. (English) Zbl 1310.68147

Summary: Checking whether a given formula is an invariant at a given program location (especially, inside a loop) can be quite nontrivial even for simple loop programs, given that it is in general an undecidable property. This is especially the case if the given formula is not an inductive loop invariant, as most automated techniques can only check or generate inductive loop invariants. In this paper, conditions are identified on simple loops and formulas when this check can be performed automatically. A general theorem is proved which gives a necessary and sufficient condition for a formula to be an invariant under certain restrictions on a loop. As a byproduct of this analysis, a new kind of loop invariant inside the loop body, called inside-loop invariant, is proposed. Such an invariant is more general than an inductive loop invariant typically used in the Floyd-Hoare axiomatic approach to program verification. The use of such invariants for program debugging is explored; it is shown that such invariants can be more useful than traditional inductive loop invariants especially when one is interested in checking extreme/side conditions such as underflow, accessing array/collection data structures outside the range, divide by zero, etc.

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)

Software:

Daikon; QEPCAD
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Cousot P and Cousot R, Abstract interpretation: A unified lattice model for static analysis of program by construction or approximation of fixpoints, 4th POPL, 1977. · Zbl 1323.68356
[2] Floyd, R. W., Assigning meanings to programs, 19-37 (1967) · Zbl 0189.50204
[3] Hoare C A R, An axiomatic basis for computer programming, Communications of the ACM, 1969, 12(10): 576-585. · Zbl 0179.23105 · doi:10.1145/363235.363259
[4] Rodriguez-Carbonell E and Kapur D, Automatic generation of polynomial invariants of bounded degree using abstract interpretation, Science of Computer Programming, 2007, 64(1): 54-75 · Zbl 1171.68555 · doi:10.1016/j.scico.2006.03.003
[5] Cousot, P.; Halbwachs, N., Automatic Discovery of Linear Restraints among Variables of a Program, 84-97 (1978)
[6] Miné A, Weakly relational numerical abstract domains, PhD thesis, École Polytechnique, Paris, France, 2005.
[7] Rodriguez-Carbonell E and Kapur D, Generating all polynomial invariants in simple loops, Journal of Symbolic Computation, 2007, 42: 443-476. · Zbl 1121.13034 · doi:10.1016/j.jsc.2007.01.002
[8] Kapur D, A Quantifier Elimination based Heuristic for Automatically Generating Inductive Assertions for Programs, Journal of Systems Science and Complexity, 2006, 19(3): 307-330. · Zbl 1115.68051 · doi:10.1007/s11424-006-0307-x
[9] Bradley, A. R.; Manna, Z., Verification constraint problems with strengthening, 35-49 (2006) · Zbl 1168.68421
[10] Chen, Y.; Xia, B.; Yang, L.; Zhan, N., Generating polynomial invariants with DISCOVERER and QEPCAD, 67-82 (2007) · Zbl 1151.68366 · doi:10.1007/978-3-540-75221-9_4
[11] Colón, M.; Sankaranarayanan, S.; Sipma, H. B., inear invariant generation using non-linear constraint solving, 420-432 (2003) · Zbl 1278.68164
[12] Sankaranarayanan, S.; Sipma, H. B.; Manna, Z., Non-linear Loop Invariant Generation Using Grëobner Bases, 318-329 (2004) · Zbl 1325.68071
[13] Xia, B.; Yang, L.; Zhan, N., Program verification by reduction to semialgebraic systems solving, 277-291 (2008)
[14] Ernst M D, Perkins J H, Guo P J, McCamant S, Pacheco C, Tschantz M S, and Xiao C, The Daikon system for dynamic detection of likely invariants, Science of Computer Programming, 2007, 69(1-3): 35-45. · Zbl 1161.68390 · doi:10.1016/j.scico.2007.01.015
[15] Loeckx J and Sieber K, The Foundations of Program Verification, John Wiley & Sons Ltd. and B.G. Teubner, 1984. · Zbl 0625.68017
[16] Chen Y, Xia B, Yang L, Zhan N, and Zhou C, Discovering non-linear ranking functions by solving semi-algebraic systems, eds. by Jones C B, Liu Z, Woodcock J, Lecture Notes in Computer Science, 4711, Springer, 2007, 34-49. · Zbl 1147.68442
[17] Podelski A and Rybalchenko A, A complete method for the synthesis of linear ranking functions, VMCAI 2004: Verification, Model Checking, and Abstract Interpretation, Lecture Notes in Computer Science, 2937, Springer, 2004, 239-251. · Zbl 1202.68109 · doi:10.1007/978-3-540-24622-0_20
[18] Tiwari A, Termination of linear programs, CAV: International Conference on Computer Aided Verification, 2004. · Zbl 1103.68037
[19] Wu, B.; Shen, L.; Bi, Z.; Zeng, Z., Termination of a class of the programs with polynomial guards, 274-277 (2009)
[20] Xia, B.; Yang, L.; Zhan, N.; Zhang, Z., Symbolic decision procedure for termination of linear programs (2009)
[21] Kapur, D., Wu’s perspective on Theorem Proving with a recent application to Program Analysis (2009)
[22] Cousot P, Proving program invariance and termination by parametric abstraction, lagrangian relaxation and semidefinite programming. VMCAI 2005: Verification, Model Checking, and Abstract Interpretation, Lecture Notes in Computer Science, 3385, Springer, 2005. · Zbl 1111.68503
[23] Brown C W and QEPCAD B, a program for computing with semi-algebraic sets using CADs, ACM SIGSAM Bulletin, 2003, 37(4): 97-108. · Zbl 1083.68148 · doi:10.1145/968708.968710
[24] Bradley A R and Manna Z, Property-directed incremental invariant generation. Formal Aspects of Computing, 2008, 20(4-5): 379-405. · Zbl 1149.68402 · doi:10.1007/s00165-008-0080-9
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.