Download PDFOpen PDF in browser

Algebra-based Synthesis of Loops and their Invariants

EasyChair Preprint 4946

12 pagesDate: January 31, 2021

Abstract

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 paper we 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 linear recurrence equations with constant coefficients, called C-finite recurrences. We first describe an algorithmic approach for synthesising all polynomial equality invariants of such non-deterministic numeric single-path loops. By reverse engineering invariant synthesis, we then describe 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 optimisationand generating number sequences from algebraic relations.

This paper is a pre-print of its invited paper version at VMCAI 2021.

Keyphrases: Algebraic Recurrences, Optimization, formal verification, loop invariants, loop synthesis, symbolic computation

BibTeX entry
BibTeX does not have the right entry for preprints. This is a hack for producing the correct reference:
@booklet{EasyChair:4946,
  author    = {Andreas Humenberger and Laura Kovács},
  title     = {Algebra-based Synthesis of Loops and their Invariants},
  howpublished = {EasyChair Preprint 4946},
  year      = {EasyChair, 2021}}
Download PDFOpen PDF in browser