Invariant generation for multi-path loops with polynomial assignments
From MaRDI portal
Abstract: Program analysis requires the generation of program properties expressing conditions to hold at intermediate program locations. When it comes to programs with loops, these properties are typically expressed as loop invariants. In this paper we study a class of multi-path program loops with numeric variables, in particular nested loops with conditionals, where assignments to program variables are polynomial expressions over program variables. We call this class of loops extended P-solvable and introduce an algorithm for generating all polynomial invariants of such loops. By an iterative procedure employing Gr"obner basis computation, our approach computes the polynomial ideal of the polynomial invariants of each program path and combines these ideals sequentially until a fixed point is reached. This fixed point represents the polynomial ideal of all polynomial invariants of the given extended P-solvable loop. We prove termination of our method and show that the maximal number of iterations for reaching the fixed point depends linearly on the number of program variables and the number of inner loops. In particular, for a loop with m program variables and r conditional branches we prove an upper bound of m*r iterations. We implemented our approach in the Aligator software package. Furthermore, we evaluated it on 18 programs with polynomial arithmetic and compared it to existing methods in invariant generation. The results show the efficiency of our approach.
Recommendations
Cited in
(29)- Counterexample-guided polynomial loop invariant generation by Lagrange interpolation
- Termination of polynomial loops
- Algebra-based synthesis of loops and their invariants (invited paper)
- A complete invariant generation approach for P-solvable loops
- Non-linear loop invariant generation using Gröbner bases
- Invariant Generation for P-Solvable Loops with Assignments
- Finding polynomial loop invariants for probabilistic programs
- Automated generation of non-linear loop invariants utilizing hypergeometric sequences
- Polynomial invariants generation of programs
- Static Analysis
- Algebra-Based Loop Analysis
- Logic for reasoning about bugs in loops over data sequences (IFIL)
- From Polynomial Invariants to Linear Loops
- Moment-based invariants for probabilistic loops with non-polynomial assignments
- Solving invariant generation for unsolvable loops
- What else is undecidable about loops?
- Symbolic computation in automated program reasoning
- Affine Loop Invariant Generation via Matrix Algebra
- Targeting Completeness: Using Closed Forms for Size Bounds of Integer Programs
- Invariant relations for affine loops
- Regular path clauses and their application in solving loops
- Positivity proofs for linear recurrences through contracted cones
- (Un)solvable loop analysis
- Polynomial loops: beyond termination
- On strongest algebraic program invariants
- Targeting completeness: automated complexity analysis of integer programs
- Positivity proofs for linear recurrences with several dominant eigenvalues
- Algebraic and algorithmic methods for computing polynomial loop invariants
- Porous invariants
This page was built for publication: Invariant generation for multi-path loops with polynomial assignments
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3296330)
