Non-linear loop invariant generation using Gröbner bases
DOI10.1145/964001.964028zbMATH Open1325.68071OpenAlexW2098045685MaRDI QIDQ3452270FDOQ3452270
Authors: Sriram Sankaranarayanan, Henny B. Sipma, Zohar Manna 
Publication date: 11 November 2015
Published in: Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)
Full work available at URL: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.137.9536
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
verificationconstraint programmingidealssymbolic computationprogram analysisinvariant generationGröbner bases
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) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19)
Cited In (46)
- On invariant checking
- A deductive approach towards reasoning about algebraic transition systems
- Inferring Loop Invariants Using Postconditions
- Combining Model Checking and Data-Flow Analysis
- 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
- 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)
- An iterative method for generating loop invariants
- Analysis of linear definite iterative loops
- 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
- Algebra, Coalgebra, and Minimization in Polynomial Differential Equations
- Transformation-Enabled Precondition Inference
- Analysing All Polynomial Equations in ${\mathbb Z_{2^w}}$
- Mathematics for reasoning about loop functions
- Endomorphisms for Non-trivial Non-linear Loop Invariant Generation
- The structure of polynomial invariants of linear loops
- Generalized homogeneous polynomials for efficient template-based nonlinear invariant synthesis
- Resource-usage-aware configuration in software product lines
- Local Search For Satisfiability Modulo Integer Arithmetic Theories
- Automatic pre- and postconditions for partial differential equations
- Change-of-bases abstractions for non-linear hybrid systems
- Generating invariants for non-linear loops by linear algebraic methods
- 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
- Products, polynomials and differential equations in the stream calculus
- Computing polynomial program invariants
- Geometric Quantifier Elimination Heuristics for Automatically Generating Octagonal and Max-plus Invariants
- Polynomial invariants for linear loops
- Elimination Techniques for Program Analysis
- Proving total correctness and generating preconditions for loop programs via symbolic-numeric computation methods
- O-Minimal Invariants for Discrete-Time Dynamical Systems
- 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
- Synthesizing switching controllers for hybrid systems by generating invariants
- Reasoning Algebraically About P-Solvable 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)
