Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Simple Linear Loops: Algebraic Invariants and Applications

Rida Ait El Manssour, George Kenison, Mahsa Shirmohammadi, Anton Varonka

TL;DR

A polynomial-space algorithm is developed that computes the strongest algebraic invariant for simple linear loops, generating all polynomial equations that hold among program variables across all reachable states.

Abstract

The automatic generation of loop invariants is a fundamental challenge in software verification. While this task is undecidable in general, it is decidable for certain restricted classes of programs. This work focuses on invariant generation for (branching-free) loops with a single linear update. Our primary contribution is a polynomial-space algorithm that computes the strongest algebraic invariant for simple linear loops, generating all polynomial equations that hold among program variables across all reachable states. The key to achieving our complexity bounds lies in mitigating the blowup associated with variable elimination and Gröbner basis computation, as seen in prior works. Our procedure runs in polynomial time when the number of program variables is fixed. We examine various applications of our results on invariant generation, focusing on invariant verification and loop synthesis. The invariant verification problem investigates whether a polynomial ideal defining an algebraic set serves as an invariant for a given linear loop. We show that this problem is coNP-complete and lies in PSPACE when the input ideal is given in dense or sparse representations, respectively. In the context of loop synthesis, we aim to construct a loop with an infinite set of reachable states that upholds a specified algebraic property as an invariant. The strong synthesis variant of this problem requires the construction of loops for which the given property is the strongest invariant. In terms of hardness, synthesising loops over integers (or rationals) is as hard as Hilbert's Tenth problem (or its analogue over the rationals). When the constants of the output are constrained to bit-bounded rational numbers, we demonstrate that loop synthesis and its strong variant are both decidable in PSPACE, and in NP when the number of program variables is fixed.

Simple Linear Loops: Algebraic Invariants and Applications

TL;DR

A polynomial-space algorithm is developed that computes the strongest algebraic invariant for simple linear loops, generating all polynomial equations that hold among program variables across all reachable states.

Abstract

The automatic generation of loop invariants is a fundamental challenge in software verification. While this task is undecidable in general, it is decidable for certain restricted classes of programs. This work focuses on invariant generation for (branching-free) loops with a single linear update. Our primary contribution is a polynomial-space algorithm that computes the strongest algebraic invariant for simple linear loops, generating all polynomial equations that hold among program variables across all reachable states. The key to achieving our complexity bounds lies in mitigating the blowup associated with variable elimination and Gröbner basis computation, as seen in prior works. Our procedure runs in polynomial time when the number of program variables is fixed. We examine various applications of our results on invariant generation, focusing on invariant verification and loop synthesis. The invariant verification problem investigates whether a polynomial ideal defining an algebraic set serves as an invariant for a given linear loop. We show that this problem is coNP-complete and lies in PSPACE when the input ideal is given in dense or sparse representations, respectively. In the context of loop synthesis, we aim to construct a loop with an infinite set of reachable states that upholds a specified algebraic property as an invariant. The strong synthesis variant of this problem requires the construction of loops for which the given property is the strongest invariant. In terms of hardness, synthesising loops over integers (or rationals) is as hard as Hilbert's Tenth problem (or its analogue over the rationals). When the constants of the output are constrained to bit-bounded rational numbers, we demonstrate that loop synthesis and its strong variant are both decidable in PSPACE, and in NP when the number of program variables is fixed.
Paper Structure (18 sections, 17 theorems, 43 equations, 2 figures)

This paper contains 18 sections, 17 theorems, 43 equations, 2 figures.

Table of Contents

  1. Introduction
  2. Overview of Main Results
  3. Algebraic Invariant Generation
  4. Invariant Verification
  5. Weak and Strong Loop Synthesis
  6. Algebraic Closure of Linear Loops
  7. A Convenient Jordan Block Decomposition
  8. Computing the Strongest Algebraic Invariant
  9. Computational Complexity
  10. Worked Examples
  11. Invariant Verification
  12. Bit-bounded Synthesis
  13. Further Discussion
  14. Extended Background
  15. Complexity Theory
  16. ...and 3 more sections

Key Result

theorem 1

Let $\langle M,\boldsymbol{\alpha}\rangle$ be a rational loop with orbit $\mathcal{O}$. A set of polynomials defining ${\overline{\mathcal{O}}}\newline$ is computable in $\PSPACE$. For all fixed $d\in \mathbb{N}$, the computation of ${\overline{\mathcal{O}}}\newline$ for $d$-dimensional loops is in

Figures (2)

  • Figure 1: Summary of our main results (see \ref{['sec-overview']} for a comprehensive overview).
  • Figure 2: Fibonacci simple loop program

Theorems & Definitions (18)

  • theorem 1
  • proposition 1
  • proposition 2
  • lemma 1
  • proposition 3
  • proposition 4
  • lemma 2
  • Claim 2
  • theorem 2
  • proposition 4
  • ...and 8 more