Algebra-based synthesis of loops and their invariants (invited paper)
From MaRDI portal
(Redirected from Publication:2234055)
Abstract: Provably correct software is one of the key challenges in our softwaredriven 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 optimisation and generating number sequences from algebraic relations. This is a preprint that was invited for publication at VMCAI 2021.
Recommendations
Cites work
- A data driven approach for algebraic loop invariants
- A Deductive Approach to Program Synthesis
- Affine relationships among variables of a program
- Algebra-based synthesis of loops and their invariants (invited paper)
- Aligator.jl -- a Julia package for loop invariant generation
- An axiomatic basis for computer programming
- Automata, Languages and Programming
- Automated generation of non-linear loop invariants utilizing hypergeometric sequences
- Automatic generation of polynomial invariants of bounded degree using abstract interpretation
- Automating string processing in spreadsheets using input-output examples
- Bruno Buchberger's PhD thesis 1965: An algorithm for finding the basis elements of the residue class ring of a zero dimensional polynomial ideal. Translation from the German
- Computing polynomial program invariants
- From program verification to program synthesis
- Generating all polynomial invariants in simple loops
- scientific article; zbMATH DE number 3870578 (Why is no real title available?)
- Inference of polynomial invariants for imperative programs: a farewell to Gröbner bases
- Invariant generation for multi-path loops with polynomial assignments
- Non-linear loop invariant generation using Gröbner bases
- Polynomial invariants by linear algebra
- Polynomial Invariants for Affine Programs
- Reasoning Algebraically About P-Solvable Loops
- The concrete tetrahedron. Symbolic sums, recurrence equations, generating functions, asymptotic estimates
Cited in
(8)- Algebra-based synthesis of loops and their invariants (invited paper)
- Proving total correctness and generating preconditions for loop programs via symbolic-numeric computation methods
- Synthesizing invariants by solving solvable loops
- Algebra-Based Loop Analysis
- Algebra-Based Reasoning for Loop Synthesis
- Affine Loop Invariant Generation via Matrix Algebra
- Algebra-Based Loop Synthesis
- Termination of triangular polynomial loops
This page was built for publication: Algebra-based synthesis of loops and their invariants (invited paper)
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2234055)
