Algebra-Based Reasoning for Loop Synthesis

TL;DR

This paper introduces an algorithm that synthesizes loops satisfying polynomial invariants by transforming the problem into a polynomial constraint, enabling correct-by-design program construction and verification.

Contribution

It presents a novel polynomial constraint-based method for synthesizing loops with polynomial invariants, including proofs of soundness and completeness within fixed bounds.

Findings

Algorithm successfully synthesizes loops with polynomial invariants.

Implementation with Absynth demonstrates practical viability.

Method applies to program verification and algebraic sequence generation.

Abstract

Provably correct software is one of the key challenges of our software-driven society. Program synthesis -- the task of constructing a program satisfying a given specification -- is one strategy for achieving this. The result of this task is then a program which is correct by design. As in the domain of program verification, handling loops is one of the main ingredients to a successful synthesis procedure. We present an algorithm for synthesizing loops satisfying a given polynomial loop invariant. The class of loops we are considering can be modeled by a system of algebraic recurrence equations with constant coefficients, encoding thus program loops with affine operations among program variables. We turn the task of loop synthesis into a polynomial constraint problem, by precisely characterizing the set of all loops satisfying the given invariant. We prove soundness of our approach, as well as its completeness with respect to an a priori fixed upper bound on the number of program variables. Our work has applications towards synthesizing loops satisfying a given polynomial loop invariant, program verification, as well as generating number sequences from algebraic relations. To understand viability of the methodology and heuristics for synthesizing loops, we implement and evaluate the method using the Absynth tool.