Non-linear loop invariant generation using Gröbner bases
From MaRDI portal
Publication:3452270
Recommendations
- Generating invariants for non-linear loops by linear algebraic methods
- Endomorphisms for Non-trivial Non-linear Loop Invariant Generation
- Automated generation of non-linear loop invariants utilizing hypergeometric sequences
- Automatic Generation of Polynomial Loop Invariants
- Automatic generation of non-linear loop invariants
- From Polynomial Invariants to Linear Loops
- Invariant generation for multi-path loops with polynomial assignments
- Solving invariant generation for unsolvable loops
- An iterative method for generating loop invariants
- Gröbner bases and solving nonlinear polynomial systems
Cited in
(44)- Algebra-based synthesis of loops and their invariants (invited paper)
- Geometric Quantifier Elimination Heuristics for Automatically Generating Octagonal and Max-plus Invariants
- Invariant Synthesis for Combined Theories
- On invariant checking
- Transformation-Enabled Precondition Inference
- Elimination Techniques for Program Analysis
- SAT modulo linear arithmetic for solving polynomial constraints
- Counterexample- and simulation-guided floating-point loop invariant synthesis
- Products, polynomials and differential equations in the stream calculus
- Inferring Loop Invariants Using Postconditions
- A deductive approach towards reasoning about algebraic transition systems
- Change-of-bases abstractions for non-linear hybrid systems
- Generating invariants for non-linear loops by linear algebraic methods
- On the Coalgebra of Partial Differential Equations
- Polynomial invariants for linear loops
- Generating semi-algebraic invariants for non-autonomous polynomial hybrid systems
- Recent advances in program verification through computer algebra
- Automatic generation of non-linear loop invariants
- Generating all polynomial invariants in simple loops
- Endomorphisms for Non-trivial Non-linear Loop Invariant Generation
- Automated generation of non-linear loop invariants utilizing hypergeometric sequences
- Toward automatic verification of quantum programs
- A quantifier-elimination based heuristic for automatically generating inductive assertions for programs
- Resource-usage-aware configuration in software product lines
- Synthesizing switching controllers for hybrid systems by generating invariants
- Analysing All Polynomial Equations in ${\mathbb Z_{2^w}}$
- Inference of polynomial invariants for imperative programs: a farewell to Gröbner bases
- An iterative method for generating loop invariants
- Formal modelling, analysis and verification of hybrid systems
- Mathematics for reasoning about loop functions
- Proving total correctness and generating preconditions for loop programs via symbolic-numeric computation methods
- A Numerical Abstract Domain Based on Expression Abstraction and Max Operator with Application in Timing Analysis
- Reasoning Algebraically About P-Solvable Loops
- Formal verification and quantitative metrics of MPSoC data dynamics
- Discovering non-terminating inputs for multi-path polynomial programs
- Combining model checking and data-flow analysis
- A method of proving the invariance of linear inequalities for linear loops
- Local Search For Satisfiability Modulo Integer Arithmetic Theories
- Computing polynomial program invariants
- Constructing invariants for hybrid systems
- Analysis of linear definite iterative loops
- Loop invariants: analysis, classification, and examples
- Automatic pre- and postconditions for partial differential equations
- The structure of polynomial invariants of linear loops
This page was built for publication: Non-linear loop invariant generation using Gröbner bases
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3452270)
