Solving Invariant Generation for Unsolvable Loops

TL;DR

This paper introduces a novel method for generating invariants in loops that are not solvable, by identifying defective variables and synthesizing polynomial invariants, applicable to both deterministic and probabilistic programs.

Contribution

It presents a new technique for invariant synthesis in unsolvable loops, including variable partitioning, defect detection, and polynomial invariant generation.

Findings

Effective invariant synthesis for unsolvable loops demonstrated

Applicable to probabilistic and deterministic programs

Feasibility shown through implementation and experiments

Abstract

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.