Abstract
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.
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
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)
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)
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)
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)
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)
Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs (1976)
Everest, G., van der Poorten, A., Shparlinski, I., Ward, T.: Recurrence Sequences. Mathematical Surveys and Monographs, American Mathematical Society, 104 (2003)
German, S.M., Wegbreit, B.: A Synthesizer of Inductive Assertions. IEEE Transactions on Software Engineering 1, 68–75 (1975)
Gosper, R.W.: Decision Procedures for Indefinite Hypergeometric Summation. Journal of Symbolic Computation 75, 40–42 (1978)
Kaldewaij, A.: Programming. The Derivation of Algorithms. Prentince-Hall, Englewood Cliffs (1990)
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)
Karr, M.: Affine Relationships Among Variables of Programs. Acta Informatica 6, 133–151 (1976)
Kauers, M.: SumCracker: A Package for Manipulating Symbolic Sums and Related Objects. Journal of Symbolic Computation 41, 1039–1057 (2006)
Kauers, M., Zimmermann, B.: Computing the Algebraic Relations of C-finite Sequences and Multisequences. Technical Report 2006-24, SFB F013 (2006)
Kirchner, M.: Program Verification with the Mathematical Software System Theorema. Technical Report 99-16, RISC-Linz, Austria, Diplomaarbeit (1999)
Knuth, D.E.: The Art of Computer Programming, 3rd edn. vol. 2. Addison-Wesley, Reading (1998)
Kovács, L.: Automated Invariant Generation by Algebraic Techniques for Imperative Program Verification in Theorema. PhD thesis, RISC, Johannes Kepler University Linz (2007)
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)
Kovács, L., Popov, N., Jebelean, T.: Combining Logic and Algebraic Techniques for Program Verification in Theorema. In: Proc. of ISOLA 2006 (2006)
Manna, Z.: Mathematical Theory of Computation. McGraw-Hill Inc, New York (1974)
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)
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)
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)
Petter, M.: Berechnung von polynomiellen Invarianten. Master’s thesis, Technical University Münich, Germany (2004)
Rodriguez-Carbonell, E., Kapur, D.: Generating All Polynomial Invariants in Simple Loops. J. of Symbolic Computation 42(4), 443–476 (2007)
Sankaranaryanan, S., Sipma, H.B., Manna, Z.: Non-Linear Loop Invariant Generation using Gröbner Bases. In: Proc. of POPL 2004 (2004)
Wegbreit, B.: The Synthesis of Loop Predicates. Communication of the ACM 2(17), 102–112 (1974)
Zeilberger, D.: A Holonomic System Approach to Special Functions. Journal of Computational and Applied Mathematics 32, 321–368 (1990)
Zuse, K.: The Computer - My Life. Springer, Heidelberg (1993)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kovács, L. (2008). Reasoning Algebraically About P-Solvable Loops. In: Ramakrishnan, C.R., Rehof, J. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2008. Lecture Notes in Computer Science, vol 4963. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-78800-3_18
Download citation
DOI: https://doi.org/10.1007/978-3-540-78800-3_18
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-78799-0
Online ISBN: 978-3-540-78800-3
eBook Packages: Computer ScienceComputer Science (R0)