Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

(Un)Solvable Loop Analysis

Daneshvar Amrollahi, Ezio Bartocci, George Kenison, Laura Kovács, Marcel Moosbrugger, Miroslav Stankovič

TL;DR

This paper establishes a technique for invariant synthesis for loops that are not solvable, termed unsolvable loops and presents a novel technique that automatically synthesises polynomials from defective monomials, that admit closed-form solutions and thus lead to polynomial loop invariants.

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íguez-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. Herein we consider the following two applications. First, we present a novel technique that automatically synthesises polynomials from defective monomials, that admit closed-form solutions and thus lead to polynomial loop invariants. Second, given an unsolvable loop, we synthesise solvable loops with the following property: the invariant polynomials of the solvable loops are all invariants of the given unsolvable loop. Our implementation and experiments demonstrate both the feasibility and applicability of our approach to both deterministic and probabilistic programs.

(Un)Solvable Loop Analysis

TL;DR

This paper establishes a technique for invariant synthesis for loops that are not solvable, termed unsolvable loops and presents a novel technique that automatically synthesises polynomials from defective monomials, that admit closed-form solutions and thus lead to polynomial loop invariants.

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íguez-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. Herein we consider the following two applications. First, we present a novel technique that automatically synthesises polynomials from defective monomials, that admit closed-form solutions and thus lead to polynomial loop invariants. Second, given an unsolvable loop, we synthesise solvable loops with the following property: the invariant polynomials of the solvable loops are all invariants of the given unsolvable loop. Our implementation and experiments demonstrate both the feasibility and applicability of our approach to both deterministic and probabilistic programs.
Paper Structure (26 sections, 8 theorems, 34 equations, 2 figures, 2 tables, 2 algorithms)

This paper contains 26 sections, 8 theorems, 34 equations, 2 figures, 2 tables, 2 algorithms.

Table of Contents

  1. Introduction
  2. Background and Motivation
  3. Related Work
  4. Our Contributions
  5. Beyond Invariant Generation
  6. Structure and Summary of Results
  7. Preliminaries
  8. Notation
  9. C-finite recurrences
  10. Invariants
  11. Polynomial Invariants and Invariant Ideals
  12. From Loops to Recurrences
  13. Recurrence Operators
  14. Solvable Operators
  15. Defective Variables
  16. ...and 11 more sections

Key Result

Corollary 10

Given any effective variable $x\in E(\mathcal{P})$, the recurrence relation $\mathcal{R}[x]$ is a polynomial in effective variables.

Figures (2)

  • Figure 1: Two running examples with unsolvable recurrence operators. Nevertheless, $\mathcal{P}_\square$ admits a closed-form for combinations of variables and $\mathcal{P}_\textrm{SC}$ admits a polynomial invariant. Herein we use $\star$ (rather than a loop guard or true) as loop termination is not our focus. For the avoidance of doubt, in this paper we consider standard mathematical arithmetic (e.g. mathematical integers) rather than machine floating-point and finite precision arithmetic.
  • Figure 2: The dependency graphs for $\mathcal{P}_\textrm{SC}$ and $\mathcal{P}_\square$ from Figure \ref{['fig:running-examples']}.

Theorems & Definitions (50)

  • Example 1
  • Definition 2: Recurrence Operator
  • Example 3
  • Definition 4: Solvable Operators Rodriguez04Oliveira16
  • Example 5
  • Definition 6: Variable Dependency
  • Definition 7: Dependency Graph
  • Definition 8: Effective-Defective
  • Example 9
  • Corollary 10
  • ...and 40 more