Automatic generation of polynomial invariants of bounded degree using abstract interpretation
From MaRDI portal
Publication:859956
DOI10.1016/j.scico.2006.03.003zbMath1171.68555OpenAlexW2099629271MaRDI QIDQ859956
Deepak Kapur, Enric Rodríguez-Carbonell
Publication date: 22 January 2007
Published in: Science of Computer Programming (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.scico.2006.03.003
Gröbner bases; other bases for ideals and modules (e.g., Janet and border bases) (13P10) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60)
Related Items (17)
Mechanical inference of invariants for FOR-loops ⋮ When Is a Formula a Loop Invariant? ⋮ On invariant checking ⋮ The structure of polynomial invariants of linear loops ⋮ Proving correctness of imperative programs by linearizing constrained Horn clauses ⋮ Reusable contracts for safe integration of reinforcement learning in hybrid systems ⋮ Generating invariants for non-linear loops by linear algebraic methods ⋮ Analysing All Polynomial Equations in ${\mathbb Z_{2^w}}$ ⋮ Polynomial invariants for linear loops ⋮ Generating all polynomial invariants in simple loops ⋮ Algebra-based synthesis of loops and their invariants (invited paper) ⋮ An Iterative Method for Generating Loop Invariants ⋮ Elimination Techniques for Program Analysis ⋮ Unnamed Item ⋮ Degree and Dimension Estimates for Invariant Ideals of $$P$$ -Solvable Recurrences ⋮ Automatic proving or disproving equality loop invariants based on finite difference techniques ⋮ Endomorphisms for Non-trivial Non-linear Loop Invariant Generation
Uses Software
This page was built for publication: Automatic generation of polynomial invariants of bounded degree using abstract interpretation
