# Solving Invariant Generation for Unsolvable Loops

arXiv: https://arxiv.org/abs/2206.06943 · HTML: https://mlsanity.com/paper/2206.06943/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 14 Jun 2022.

## Built on by (most cited first, 1 of 1)

- [A Machine Learning-based Approach for Solving Recurrence Relations and its use in Cost Analysis of Logic Programs](https://mlsanity.com/paper/2405.06972/) (2024)

## Abstract (arXiv)

Automatically generating invariants, key to computer-aided analysis of probabilistic and deterministic programs and compiler optimisation, is a challenging open problem. Whilst the problem is in general undecidable, the goal is settled for restricted classes of loops. For the class of solvable loops, introduced by Kapur and Rodr'iguez-Carbonell in 2004, one can automatically compute invariants from closed-form solutions of recurrence equations that model the loop behaviour. In this paper we establish a technique for invariant synthesis for loops that are not solvable, termed unsolvable loops. Our approach automatically partitions the program variables and identifies the so-called defective variables that characterise unsolvability. We further present a novel technique that automatically synthesises polynomials, in the defective variables, that admit closed-form solutions and thus lead to polynomial loop invariants. Our implementation and experiments demonstrate both the feasibility and applicability of our approach to both deterministic and probabilistic programs.