Algebraic Reasoning for (Un)Solvable Loops (Invited Talk)

Author Laura Kovács

Thumbnail PDF


  • Filesize: 377 kB
  • 2 pages

Document Identifiers

Author Details

Laura Kovács
  • TU Wien, Austria


This talk is based on joint works with a number of authors, including Daneshvar Amrollahi (TU Wien alumni), Ezio Bartocci (TU Wien), George Kenison (TU Wien), Marcel Moosbrugger (TU Wien), Julian Müllner (TU Wien), Miroslav Stankovic (TU Wien), and Anton Varonka (TU Wien).

Cite AsGet BibTex

Laura Kovács. Algebraic Reasoning for (Un)Solvable Loops (Invited Talk). In 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 272, pp. 4:1-4:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


Loop invariants describe valid program properties that hold before and after every loop iteration. As such, loop invariants are the workhorses in formalizing loop semantics and automating the formal analysis and verification of programs with loops. While automatically synthesizing loop invariants is, in general, an uncomputable problem, when considering only single-path loops with linear updates (linear loops), the strongest polynomial invariant is in fact computable [Michael Karr, 1976; Markus Müller-Olm and Helmut Seidl, 2004; Laura Kovács, 2008; Ehud Hrushovski et al., 2018]. Yet, already for loops with "only" polynomial updates, computing the strongest invariant has been an open challenge since 2004 [Markus Müller-Olm and Helmut Seidl, 2004]. In this invited talk, we first present computability results on polynomial invariant synthesis for restricted polynomial loops, called solvable loops [Rodríguez-Carbonell and Kapur, 2004]. Key to solvable loops is that one can automatically compute invariants from closed-form solutions of algebraic recurrence equations that model the loop behaviour [Laura Kovács, 2008; Andreas Humenberger et al., 2017]. We also establish a technique for invariant synthesis for classes of loops that are not solvable, termed unsolvable loops [Daneshvar Amrollahi et al., 2022]. We next study the limits of computability in deriving the (strongest) polynomial invariants for arbitrary polynomial loops. We prove that computing the strongest polynomial invariant of arbitrary, single-path polynomial loops is very hard [Julian Müllner, 2023] - namely, it is at least as hard as the Skolem problem [Graham Everest et al., 2003; Terrence Tao, 2008], a prominent algebraic problem in the theory of linear recurrences. Going beyond single-path loops, we show that the strongest polynomial invariant is uncomputable already for multi-path polynomial loops with arbitrary quadratic polynomial updates [Laura Kovács and Anton Varonka, 2023].

Subject Classification

ACM Subject Classification
  • Theory of computation → Invariants
  • Theory of computation → Program verification
  • Theory of computation → Algebraic semantics
  • Symbolic Computation
  • Formal Methods
  • Loop Analysis
  • Polynomial Invariants


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. Daneshvar Amrollahi, Ezio Bartocci, George Kenison, Laura Kovács, Marcel Moosbrugger, and Miroslav Stankovic. Solving Invariant Generation for Unsolvable Loops. In Proc. of SAS, 2022. URL:
  2. Graham Everest, Alfred J. van der Poorten, Igor E. Shparlinski, and Thomas Ward. Recurrence Sequences. Mathematical Surveys and Monographs. American Mathematical Society, 2003. Google Scholar
  3. Ehud Hrushovski, Joël Ouaknine, Amaury Pouly, and James Worrell. Polynomial Invariants for Affine Programs. In Proc. of LICS, 2018. URL:
  4. Andreas Humenberger, Maximilian Jaroschek, and Laura Kovács. Automated Generation of Non-Linear Loop Invariants Utilizing Hypergeometric Sequences. In Proc. of ISSAC, 2017. URL:
  5. Michael Karr. Affine Relationships Among Variables of a Program. Acta Inform., 1976. URL:
  6. Laura Kovács. Reasoning Algebraically About P-Solvable Loops. In Proc. of TACAS, 2008. URL:
  7. Laura Kovács and Anton Varonka. What Else is Undecidable About Loops? In Proc. of RAMiCS, 2023. URL:
  8. Markus Müller-Olm and Helmut Seidl. A Note on Karr’s Algorithm. In Proc. of ICALP, 2004. URL:
  9. Markus Müller-Olm and Helmut Seidl. Computing Polynomial Program Invariants. Inf. Process. Lett., 2004. URL:
  10. Julian Müllner. Exact Inference for Probabilistic Loops. Master’s thesis, TU Wien, 2023. Google Scholar
  11. Enric Rodríguez-Carbonell and Deepak Kapur. Automatic Generation of Polynomial Loop Invariants: Algebraic Foundations. In Proc. of ISSAC, 2004. URL:
  12. Terrence Tao. Structure and Randomness. American Mathematical Society, 2008. Google Scholar
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail