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 interpretationinvariantideal of polynomialsGröbner basis

Mathematics Subject Classification ID

Gröbner bases; other bases for ideals and modules (e.g., Janet and border bases) (13P10) Specification and verification (program logics, model checking, etc.) (68Q60) Semantics in the theory of computing (68Q55)

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

(23)

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

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)