Many challenges of fully automated verification of recursive programs are rooted in the hardness of generating appropriate invariants (relations among variables that hold throughout program execution). This work focuses on algebraic invariants of simple linear loops (branch-free loop programs with a single linear update). Whilst this model is elementary, even the most natural verification problems (such as termination and reachability) are arguably difficult in this setting, see Ouaknine and Worrell, https://doi.org/10.1145/2766189.2766191. As a crucial step to understanding possible relations among variables of a simple linear loop, we present a polynomial-space algorithm to compute a representation of the strongest algebraic invariant of a given loop. This set comprises all invariant polynomial equalities. We further discuss the complexity of verifying whether a given algebraic relation, that is, a collection of polynomial equalities in loop variables, is a loop invariant. Finally, we turn to synthesising simple linear loops from desired relations. Specifically, we ask whether there exists a simple linear loop that possesses a given algebraic invariant. Notably, this problem is as hard as Hilbert's Tenth Problem and thus undecidable over the integers, while decidability is open over the rationals. To this end, we explore the complexity landscape for bit-bounded loop synthesis, where the bound on the number of bits used to describe the loop is an input parameter. We show that this problem admits a polynomial-space algorithm.

The material in this presentation is based on the work undertaken in https://arxiv.org/abs/2407.09154.