Automatic generation of polynomial invariants of bounded degree using abstract interpretation

DOI10.1016/J.SCICO.2006.03.003MaRDI QIDQ859956zbMATH OpenOpenAlexFDO

Authors 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

zbMATH Keywords

abstract interpretationGröbner basisideal of polynomialsinvariant

Mathematics Subject Classification ID

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)

Recommendations

• Static Analysis
• Generating all polynomial invariants in simple loops
• An iterative method for generating loop invariants
• Automatic Generation of Polynomial Loop Invariants
• Polynomial invariants generation of programs

Cited in

(28)

• Algebra-based synthesis of loops and their invariants (invited paper)
• Polynomial invariants for linear loops
• Generating all polynomial invariants in simple loops
• Automatic proving or disproving equality loop invariants based on finite difference techniques
• Degree and dimension estimates for invariant ideals of P-solvable recurrences
• Automatic Generation of Invariants for Circular Derivations in SUP(LA)
• When is a formula a loop invariant?
• An iterative method for generating loop invariants
• Analysing All Polynomial Equations in ${\mathbb Z_{2^w}}$
• On invariant checking
• Proving correctness of imperative programs by linearizing constrained Horn clauses
• Elimination Techniques for Program Analysis
• scientific article; zbMATH DE number 7559488 (Why is no real title available?)
• Polynomial invariants generation of programs
• Static Analysis
• Endomorphisms for Non-trivial Non-linear Loop Invariant Generation
• Static Analysis
• Mechanical inference of invariants for FOR-loops
• Reusable contracts for safe integration of reinforcement learning in hybrid systems
• Affine Loop Invariant Generation via Matrix Algebra
• MDPs as distribution transformers: affine invariant synthesis for safety objectives
• On strongest algebraic program invariants
• Algebraic tools for computing polynomial loop invariants
• An abstract fixed-point theorem for Horn formula equations
• Algebraic and algorithmic methods for computing polynomial loop invariants
• On termination of polynomial programs with equality conditions
• The structure of polynomial invariants of linear loops
• Generating invariants for non-linear loops by linear algebraic methods

Describes a project that uses

Uses Software

• Macaulay2

This page was built for publication: Automatic generation of polynomial invariants of bounded degree using abstract interpretation

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q859956)