Algebraic Synthesis of Loops and their Invariants

Provably correct software is one of the key challenges in our software-driven society. While formal verification establishes the correctness of a given program, the result of program synthesis is a program which is correct by construction. In this talk I overview some of our results for both of these scenarios when analysing programs with loops. The class of loops we consider can be modelled by a system of algebraic recurrence equations, importantly with constant coefficients. I first describe an algorithmic approach for synthesising all polynomial equality invariants of such non-deterministic numeric single-path loops. By reverse engineering invariant synthesis, I then present an automated method for synthesising program loops satisfying a given set of polynomial loop invariants. Our results have applications towards proving partial correctness of programs, compiler optimisation and generating number sequences from algebraic relations.