Algebraic Synthesis of Loops and their Invariants

  • Laura Kovacs (TU Wien, Austria)
E1 05 (Leibniz-Saal)


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.

Saskia Gutzschebauch

Max Planck Institute for Mathematics in the Sciences Contact via Mail

Rida Ait El Manssour

Max Planck Institute for Mathematics in the Sciences

Marc Härkönen

Georgia Institute of Technology

Bernd Sturmfels

Max Planck Institute for Mathematics in the Sciences