Abstract
Invariant properties at various program locations play a critical role in enhancing confidence in the reliability of software. A procedure for checking whether a given set of formulas associated with various program locations is an invariant or not is proposed. The procedure attempts to check whether the formulas are preserved by various program paths, in which case it declares the formulas to be invariant; otherwise, it attempts to strengthen them based on verification conditions generated from the program paths that did not preserve the formulas. This iterative process is continued until a verification condition along some path cannot be satisfied or an initial state of the program violates the formulas strengthened thus far. It is shown that under certain conditions, for certain theories including conjunctions of polynomial equalities, the procedure terminates, either declaring the input set of formulas to be not invariant, or generating a strengthened set of inductive invariant formulas. For other theories including Presburger arithmetic, the procedure may not terminate in general; heuristics are proposed for such cases for approximating strengthening of formulas to ensure termination. There is a direct relationship between this approach for checking formulas to be invariant and the k-induction approach for verifying properties to be k-inductive. This relationship is explored in depth.
Dedicated to José Meseguer on his \(65^{th}\) birthday.
Preliminary results reported in this paper were first presented at International Conference on Mathematics Mechanization–in Honor of Prof. Wen-Tsun Wu’s \(90^{th}\) birthday (ICMM), 2009, Beijing, China, and also at the Dagstuhl Seminar Deduction and Arithmetic, October 2013. This research has been partially supported by the NSF awards CCFf-1248069 and DMS-1217054 as well as a grant for Visiting Professorship for Senior International Scientists, the Chinese Academy of Sciences.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsNotes
- 1.
Provided a sufficiently expressive theory is used.
- 2.
Here, \(\mathbf {v}\) extends to terms in the usual way.
- 3.
What approximations are necessary and in what cases they must be performed depends on the manipulation needed to compute \(\uppsi \) in the strengthening procedure.
- 4.
Strictly speaking, Gröbner basis of the radical ideal of the polynomials is computed for satisfiability check, since \(x^2 = 0 \implies x = 0\) is valid.
- 5.
It would also be possible to let \(\uppsi \) be a conjunction of such atoms.
- 6.
We thank John Cochran for bringing that paper to our attention and collaborating with us during the initial stages of this research activity.
- 7.
- 8.
It is shown in [3] how a template based approach for generating linear inequalities can be augmented to generate strengthings from counter-examples. Using this extension, it is possible to Example 18.
- 9.
All other examples in [3] can also be successfully done using Strategy IV.
References
Bjørner, N., Gurfinkel, A.: Property directed polyhedral abstraction. In: D’Souza, D., Lal, A., Larsen, K.G. (eds.) VMCAI 2015. LNCS, vol. 8931, pp. 263–281. Springer, Heidelberg (2015)
Bradley, A.R.: SAT-based model checking without unrolling. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 70–87. Springer, Heidelberg (2011)
Bradley, A.R.: Understanding IC3. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 1–14. Springer, Heidelberg (2012)
Bradley, A.R., Manna, Z.: Verification constraint problems with strengthening. In: Barkaoui, K., Cavalcanti, A., Cerone, A. (eds.) ICTAC 2006. LNCS, vol. 4281, pp. 35–49. Springer, Heidelberg (2006)
Bradley, A.R., Manna, Z.: Property-directed incremental invariant generation. Formal Aspects Comput. 20(4–5), 379–405 (2008)
Buchberger, B.: Gröbner bases: an algorithmic method in polynomial ideal theory. In: Bose, N.K. (ed.) Multidimensional Systems Theory-progress, Directions And Open Problems In Multidimensional Systems, pp. 184–232. Reidel Publishing Co, Holland (1985)
Cimatti, A., Griggio, A.: Software model checking via IC3. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 277–293. Springer, Heidelberg (2012)
Little, J., Cox, D., O’Shea, D.: Ideals, Varieties, and Algorithms: an Introduction to Computational Algebraic Geometry and Commutative algebra, 2nd edn. Springer, New York (1997)
Dillig, I., Dillig, T., Li, B., McMillan, K.: Inductive invariant generation via abductive inference. In: Lopes, C.V. (ed.) Proceedings of the 2013 ACM SIGPLAN International Conference on Object Oriented Programming Systems Languages and Applications. ACM (2013)
Hoder, K., Bjørner, N.: Generalized property directed reachability. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 157–171. Springer, Heidelberg (2012)
Stuckey, P.J., Jaffar, J., Maher, M.J., Yap, R.H.C.: Beyond finite domains. In: Borning, Alan (ed.) PPCP 1994. LNCS, vol. 874. Springer, Heidelberg (1994)
Kapur, D.: A refutational approach to geometry theorem proving. Artif. Intell. J. 37(1), 61–93 (1988)
Kapur, D.: Automatically generating loop invariants using quantifier elimination. Technical report TR-CS-2003-58, Department of Computer Science, University of New Mexico, Albuquerque, NM, USA, (2003)
Kapur, D.: A quantifier-elimination based heuristic for automatically generating inductive assertions for programs. J. Syst. Sci. Complexity 19(3), 307–330 (2006)
Kapur, D., Narendran, P.: An Equational Approach to Theorem Proving in First-Order Predicate Calculus. General Electric Corporate Research and Development, Los Angeles (1985)
Manna, Z., Pnueli, A.: Temporal verification of reactive systems:safety. Technical report, ISBN 0-387-94459-1, Springer-Verlag, New York (1995)
Heizmann, M., Hoenicke, J., Leike, J., Podelski, A.: Linear ranking for linear lasso programs. In: Van Hung, D., Ogawa, M. (eds.) ATVA 2013. LNCS, vol. 8172, pp. 365–380. Springer, Heidelberg (2013)
Miné, A.: Weakly relational numerical abstract domains. Ph.D. thesis, Ecole Polytechnique X, France (2004)
Mishchenko, A., Eén, N., Brayton, R.K.: Efficient implementation of property directed reachability. In: Bjesse, P., Slobodová, A. (ed.) Proceedings of the 11th International Conference on Formal Methods in Computer-Aided (FMCAD 2011), pp. 125–134. IEEE (2011)
Păsăreanu, C.S., Visser, W.: Verification of Java programs using symbolic execution and invariant generation. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol. 2989, pp. 164–181. Springer, Heidelberg (2004)
Rodríguez-Carbonell, E., Kapur, D.: Automatic generation of polynomial invariants of bounded degree using abstract interpretation. Sci. Comput. Program. 64(1), 54–75 (2007)
Rodríguez-Carbonell, E., Kapur, D.: Generating all polynomial invariants in simple loops. J. Symbolic Comput. 42(4), 443–476 (2007)
Zhang, Z., Kapur, D.: On invariant checking. J. Syst. Sci. Complexity 26(3), 470–482 (2013)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this chapter
Cite this chapter
Falke, S., Kapur, D. (2015). When Is a Formula a Loop Invariant?. In: Martí-Oliet, N., Ölveczky, P., Talcott, C. (eds) Logic, Rewriting, and Concurrency. Lecture Notes in Computer Science(), vol 9200. Springer, Cham. https://doi.org/10.1007/978-3-319-23165-5_13
Download citation
DOI: https://doi.org/10.1007/978-3-319-23165-5_13
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-23164-8
Online ISBN: 978-3-319-23165-5
eBook Packages: Computer ScienceComputer Science (R0)