Automatic Generation of Polynomial Loop Invariants
DOI10.1145/1005285.1005324zbMATH Open1108.13310OpenAlexW1967845657MaRDI QIDQ4657335FDOQ4657335
Authors: Enric Rodríguez-Carbonell, Deepak Kapur 
Publication date: 14 March 2005
Published in: Proceedings of the 2004 international symposium on Symbolic and algebraic computation (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1145/1005285.1005324
Recommendations
Symbolic computation and algebraic computation (68W30) Gröbner bases; other bases for ideals and modules (e.g., Janet and border bases) (13P10) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)
Cited In (37)
- Automatic complexity analysis of integer programs via triangular weakly non-linear loops
- Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops
- Automatic generation of polynomial invariants of bounded degree using abstract interpretation
- A quantifier-elimination based heuristic for automatically generating inductive assertions for programs
- Inference of polynomial invariants for imperative programs: a farewell to Gröbner bases
- Invariant generation for multi-path loops with polynomial assignments
- Generating all polynomial invariants in simple loops
- A data driven approach for algebraic loop invariants
- Symbolic computation in automated program reasoning
- Invariant relations for affine loops
- Static Analysis
- Analysis of linear definite iterative loops
- Automatic generation of non-linear loop invariants
- Nonlinear invariants for linear loops and eigenpolynomials of linear operators
- Automatic Construction and Verification of Isotopy Invariants
- \textit{Theorema}: Towards computer-aided mathematical theory exploration
- Termination of polynomial loops
- Deciding properties of affine loops
- Algebra-Based Loop Synthesis
- Automatic Generation of Invariants for Circular Derivations in SUP(LA)
- From Polynomial Invariants to Linear Loops
- The structure of polynomial invariants of linear loops
- Efficient solution of a class of quantified constraints with quantifier prefix exists-forall
- Change-of-bases abstractions for non-linear hybrid systems
- Polynomial invariants by linear algebra
- Affine Loop Invariant Generation via Matrix Algebra
- Recent advances in program verification through computer algebra
- Constructing invariants for hybrid systems
- Algebra-Based Reasoning for Loop Synthesis
- A method of proving the invariance of linear inequalities for linear loops
- Solving invariant generation for unsolvable loops
- Targeting Completeness: Using Closed Forms for Size Bounds of Integer Programs
- Polynomial invariants for linear loops
- Elimination Techniques for Program Analysis
- A complete invariant generation approach for P-solvable loops
- Non-linear loop invariant generation using Gröbner bases
- Reasoning Algebraically About P-Solvable Loops
Uses Software
This page was built for publication: Automatic Generation of Polynomial Loop Invariants
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4657335)
