Solving invariant generation for unsolvable loops
From MaRDI portal
(Redirected from Publication:6164420)
Abstract: Automatically generating invariants, key to computer-aided analysis of probabilistic and deterministic programs and compiler optimisation, is a challenging open problem. Whilst the problem is in general undecidable, the goal is settled for restricted classes of loops. For the class of solvable loops, introduced by Kapur and Rodr'iguez-Carbonell in 2004, one can automatically compute invariants from closed-form solutions of recurrence equations that model the loop behaviour. In this paper we establish a technique for invariant synthesis for loops that are not solvable, termed unsolvable loops. Our approach automatically partitions the program variables and identifies the so-called defective variables that characterise unsolvability. We further present a novel technique that automatically synthesises polynomials, in the defective variables, that admit closed-form solutions and thus lead to polynomial loop invariants. Our implementation and experiments demonstrate both the feasibility and applicability of our approach to both deterministic and probabilistic programs.
Recommendations
Cites work
- Aligator.jl -- a Julia package for loop invariant generation
- An axiomatic basis for computer programming
- Analysis of Bayesian networks via prob-solvable loops
- Automated generation of non-linear loop invariants utilizing hypergeometric sequences
- Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops
- Automatic Generation of Polynomial Loop Invariants
- Computing polynomial program invariants
- Computing the algebraic relations of \(C\)-finite sequences and multisequences
- Deductive proofs of almost sure persistence and recurrence properties
- Generating all polynomial invariants in simple loops
- scientific article; zbMATH DE number 1973372 (Why is no real title available?)
- scientific article; zbMATH DE number 3420251 (Why is no real title available?)
- Invariant generation for multi-path loops with polynomial assignments
- Logical analysis of programs
- Parallelotope Bundles for Polynomial Reachability
- Polynomial invariants by linear algebra
- Polynomial Invariants for Affine Programs
- Reasoning Algebraically About P-Solvable Loops
- Termination of polynomial loops
- The concrete tetrahedron. Symbolic sums, recurrence equations, generating functions, asymptotic estimates
- Weakest precondition reasoning for expected run-times of probabilistic programs
Cited in
(11)- Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops
- Non-linear loop invariant generation using Gröbner bases
- Loop Invariants from Counterexamples
- Symbolic computation in automated program reasoning
- Exact and approximate moment derivation for probabilistic loops with non-polynomial assignments
- Regular path clauses and their application in solving loops
- (Un)solvable loop analysis
- Preface of the special issue on the static analysis symposium 2020 and 2022
- Algebraic tools for computing polynomial loop invariants
- Targeting completeness: automated complexity analysis of integer programs
- Algebraic and algorithmic methods for computing polynomial loop invariants
This page was built for publication: Solving invariant generation for unsolvable loops
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6164420)
