Abstract
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 singlepath loops with linear updates (linear loops), the strongest polynomial invariant is in fact computable [Michael Karr, 1976; Markus MüllerOlm 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üllerOlm 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íguezCarbonell and Kapur, 2004]. Key to solvable loops is that one can automatically compute invariants from closedform 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, singlepath 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 singlepath loops, we show that the strongest polynomial invariant is uncomputable already for multipath polynomial loops with arbitrary quadratic polynomial updates [Laura Kovács and Anton Varonka, 2023].
BibTeX  Entry
@InProceedings{kovacs:LIPIcs.MFCS.2023.4,
author = {Kov\'{a}cs, Laura},
title = {{Algebraic Reasoning for (Un)Solvable Loops}},
booktitle = {48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)},
pages = {4:14:2},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783959772921},
ISSN = {18688969},
year = {2023},
volume = {272},
editor = {Leroux, J\'{e}r\^{o}me and Lombardy, Sylvain and Peleg, David},
publisher = {Schloss Dagstuhl  LeibnizZentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2023/18538},
URN = {urn:nbn:de:0030drops185385},
doi = {10.4230/LIPIcs.MFCS.2023.4},
annote = {Keywords: Symbolic Computation, Formal Methods, Loop Analysis, Polynomial Invariants}
}
Keywords: 

Symbolic Computation, Formal Methods, Loop Analysis, Polynomial Invariants 
Collection: 

48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023) 
Issue Date: 

2023 
Date of publication: 

21.08.2023 