We present a method for generating polynomial invariants for a subfamily of imperative loops operating on numbers, called the P-solvable loops. The method uses algorithmic combinatorics and algebraic techniques. The approach is shown to be complete for some special cases. By completeness we mean that it generates a set of polynomial invariants from which, under additional assumptions, any polynomial invariant can be derived. These techniques are implemented in a new software package Aligator written in Mathematica and successfully tried on many programs implementing interesting algorithms working on numbers.


Outer Loop Polynomial Identity Loop Variable Loop Counter Invariant Generation 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    Buchberger, B.: Gröbner-Bases: An Algorithmic Method in Polynomial Ideal Theory. In: Multidimensional Systems Theory - Progress, Directions and Open Problems in Multidimensional Systems, pp. 184–232 (1985)Google Scholar
  2. 2.
    Buchberger, B., Craciun, A., Jebelean, T., Kovacs, L., Kutsia, T., Nakagawa, K., Piroi, F., Popov, N., Robu, J., Rosenkranz, M., Windsteiger, W.: Theorema: Towards Computer-Aided Mathematical Theory Exploration. Journal of Applied Logic 4(4), 470–504 (2006)zbMATHCrossRefMathSciNetGoogle Scholar
  3. 3.
    Collins, G.E.: Quantifier Elimination for the Elementary Theory of Real Closed Fields by Cylindrical Algebraic Decomposition. In: Brakhage, H. (ed.) GI-Fachtagung 1975. LNCS, vol. 33, pp. 134–183. Springer, Heidelberg (1975)Google Scholar
  4. 4.
    Cousot, P., Halbwachs, N.: Automatic Discovery of Linear Restraints among Variables of a Program. In: ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 84–97 (1978)Google Scholar
  5. 5.
    Cox, D., Little, J., O’Shea, D.: Ideal, Varieties, and Algorithms. An Introduction to Computational Algebraic Geometry and Commutative Algebra, 2nd edn. Springer, Heidelberg (1998)Google Scholar
  6. 6.
    Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs (1976)zbMATHGoogle Scholar
  7. 7.
    Everest, G., van der Poorten, A., Shparlinski, I., Ward, T.: Recurrence Sequences. Mathematical Surveys and Monographs, American Mathematical Society, 104 (2003)Google Scholar
  8. 8.
    German, S.M., Wegbreit, B.: A Synthesizer of Inductive Assertions. IEEE Transactions on Software Engineering 1, 68–75 (1975)Google Scholar
  9. 9.
    Gosper, R.W.: Decision Procedures for Indefinite Hypergeometric Summation. Journal of Symbolic Computation 75, 40–42 (1978)zbMATHMathSciNetGoogle Scholar
  10. 10.
    Kaldewaij, A.: Programming. The Derivation of Algorithms. Prentince-Hall, Englewood Cliffs (1990)Google Scholar
  11. 11.
    Kapur, D.: A Quantifier Elimination based Heuristic for Automatically Generating Inductive Assertions for Programs. Journal of Systems Science and Complexity 19(3), 307–330 (2006)zbMATHCrossRefMathSciNetGoogle Scholar
  12. 12.
    Karr, M.: Affine Relationships Among Variables of Programs. Acta Informatica 6, 133–151 (1976)zbMATHCrossRefMathSciNetGoogle Scholar
  13. 13.
    Kauers, M.: SumCracker: A Package for Manipulating Symbolic Sums and Related Objects. Journal of Symbolic Computation 41, 1039–1057 (2006)zbMATHCrossRefMathSciNetGoogle Scholar
  14. 14.
    Kauers, M., Zimmermann, B.: Computing the Algebraic Relations of C-finite Sequences and Multisequences. Technical Report 2006-24, SFB F013 (2006)Google Scholar
  15. 15.
    Kirchner, M.: Program Verification with the Mathematical Software System Theorema. Technical Report 99-16, RISC-Linz, Austria, Diplomaarbeit (1999)Google Scholar
  16. 16.
    Knuth, D.E.: The Art of Computer Programming, 3rd edn. vol. 2. Addison-Wesley, Reading (1998)Google Scholar
  17. 17.
    Kovács, L.: Automated Invariant Generation by Algebraic Techniques for Imperative Program Verification in Theorema. PhD thesis, RISC, Johannes Kepler University Linz (2007)Google Scholar
  18. 18.
    Kovács, L., Jebelean, T.: Finding Polynomial Invariants for Imperative Loops in the Theorema System. In: Proc. of Verify 2006, FLoC 2006, pp. 52–67 (2006)Google Scholar
  19. 19.
    Kovács, L., Popov, N., Jebelean, T.: Combining Logic and Algebraic Techniques for Program Verification in Theorema. In: Proc. of ISOLA 2006 (2006)Google Scholar
  20. 20.
    Manna, Z.: Mathematical Theory of Computation. McGraw-Hill Inc, New York (1974)zbMATHGoogle Scholar
  21. 21.
    Müller-Olm, M., Seidl, H., Petter, M.: Interprocedurally Analyzing Polynomial Identities. In: Durand, B., Thomas, W. (eds.) STACS 2006. LNCS, vol. 3884, pp. 50–67. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  22. 22.
    Müller-Olm, M., Seidl, H.: Polynomial Constants Are Decidable. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol. 2477, pp. 4–19. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  23. 23.
    Paule, P., Schorn, M.: A Mathematica Version of Zeilberger’s Algorithm for Proving Binomial Coefficient Identities. Journal of Symbolic Computation 20(5-6), 673–698 (1995)zbMATHCrossRefMathSciNetGoogle Scholar
  24. 24.
    Petter, M.: Berechnung von polynomiellen Invarianten. Master’s thesis, Technical University Münich, Germany (2004)Google Scholar
  25. 25.
    Rodriguez-Carbonell, E., Kapur, D.: Generating All Polynomial Invariants in Simple Loops. J. of Symbolic Computation 42(4), 443–476 (2007)zbMATHCrossRefMathSciNetGoogle Scholar
  26. 26.
    Sankaranaryanan, S., Sipma, H.B., Manna, Z.: Non-Linear Loop Invariant Generation using Gröbner Bases. In: Proc. of POPL 2004 (2004)Google Scholar
  27. 27.
    Wegbreit, B.: The Synthesis of Loop Predicates. Communication of the ACM 2(17), 102–112 (1974)CrossRefMathSciNetGoogle Scholar
  28. 28.
    Zeilberger, D.: A Holonomic System Approach to Special Functions. Journal of Computational and Applied Mathematics 32, 321–368 (1990)zbMATHCrossRefMathSciNetGoogle Scholar
  29. 29.
    Zuse, K.: The Computer - My Life. Springer, Heidelberg (1993)zbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2008

Authors and Affiliations

  • Laura Kovács
    • 1
  1. 1.EPFLSwitzerland

Personalised recommendations