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)- Synthesizing switching controllers for hybrid systems by generating invariants
- On invariant checking
- A deductive approach towards reasoning about algebraic transition systems
- Reasoning Algebraically About P-Solvable Loops
- Inferring Loop Invariants Using Postconditions
- 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
- Generating semi-algebraic invariants for non-autonomous polynomial hybrid systems
- Formal modelling, analysis and verification of hybrid systems
- Automated generation of non-linear loop invariants utilizing hypergeometric sequences
- Generating all polynomial invariants in simple loops
- Discovering non-terminating inputs for multi-path polynomial programs
- On the Coalgebra of Partial Differential Equations
- Algebra-based synthesis of loops and their invariants (invited paper)
- Analysis of linear definite iterative loops
- An iterative method for generating loop invariants
- SAT modulo linear arithmetic for solving polynomial constraints
- Automatic generation of non-linear loop invariants
- Invariant Synthesis for Combined Theories
- Counterexample- and simulation-guided floating-point loop invariant synthesis
- Loop invariants: analysis, classification, and examples
- Analysing All Polynomial Equations in ${\mathbb Z_{2^w}}$
- Transformation-Enabled Precondition Inference
- Mathematics for reasoning about loop functions
- The structure of polynomial invariants of linear loops
- Endomorphisms for Non-trivial Non-linear Loop Invariant Generation
- Resource-usage-aware configuration in software product lines
- Local Search For Satisfiability Modulo Integer Arithmetic Theories
- Change-of-bases abstractions for non-linear hybrid systems
- Generating invariants for non-linear loops by linear algebraic methods
- Automatic pre- and postconditions for partial differential equations
- Recent advances in program verification through computer algebra
- Constructing invariants for hybrid systems
- A method of proving the invariance of linear inequalities for linear loops
- Computing polynomial program invariants
- Combining model checking and data-flow analysis
- Products, polynomials and differential equations in the stream calculus
- Polynomial invariants for linear loops
- Geometric Quantifier Elimination Heuristics for Automatically Generating Octagonal and Max-plus Invariants
- Elimination Techniques for Program Analysis
- Proving total correctness and generating preconditions for loop programs via symbolic-numeric computation methods
- Toward automatic verification of quantum programs
- Formal verification and quantitative metrics of MPSoC data dynamics
- A Numerical Abstract Domain Based on Expression Abstraction and Max Operator with Application in Timing Analysis
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)
