Automatic Generation of Polynomial Loop Invariants
From MaRDI portal
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) Symbolic computation and algebraic computation (68W30)
Recommendations
Cited in
(44)- Polynomial invariants by linear algebra
- Automatic complexity analysis of integer programs via triangular weakly non-linear loops
- Termination of polynomial loops
- A method of proving the invariance of linear inequalities for linear loops
- Polynomial invariants for linear loops
- Generating all polynomial invariants in simple loops
- Constructing invariants for hybrid systems
- Automatic Generation of Invariants for Circular Derivations in SUP(LA)
- Analysis of linear definite iterative loops
- Invariant generation for multi-path loops with polynomial assignments
- Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops
- A complete invariant generation approach for P-solvable loops
- Non-linear loop invariant generation using Gröbner bases
- Recent advances in program verification through computer algebra
- Deciding properties of affine loops
- Automatic Construction and Verification of Isotopy Invariants
- Automatic generation of non-linear loop invariants
- Inference of polynomial invariants for imperative programs: a farewell to Gröbner bases
- Nonlinear invariants for linear loops and eigenpolynomials of linear operators
- Efficient solution of a class of quantified constraints with quantifier prefix exists-forall
- Elimination Techniques for Program Analysis
- A data driven approach for algebraic loop invariants
- Reasoning Algebraically About P-Solvable Loops
- Static Analysis
- From Polynomial Invariants to Linear Loops
- Solving invariant generation for unsolvable loops
- Symbolic computation in automated program reasoning
- Algebra-Based Reasoning for Loop Synthesis
- Affine Loop Invariant Generation via Matrix Algebra
- Algebra-Based Loop Synthesis
- Targeting Completeness: Using Closed Forms for Size Bounds of Integer Programs
- Invariant relations for affine loops
- (Un)solvable loop analysis
- Termination of triangular polynomial loops
- Polynomial loops: beyond termination
- Algebraic tools for computing polynomial loop invariants
- Targeting completeness: automated complexity analysis of integer programs
- Algebraic and algorithmic methods for computing polynomial loop invariants
- Deciding termination of simple randomized loops
- Automatic generation of polynomial invariants of bounded degree using abstract interpretation
- \textit{Theorema}: Towards computer-aided mathematical theory exploration
- A quantifier-elimination based heuristic for automatically generating inductive assertions for programs
- The structure of polynomial invariants of linear loops
- Change-of-bases abstractions for non-linear hybrid systems
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)
