Automatic generation of polynomial invariants of bounded degree using abstract interpretation

DOI10.1016/J.SCICO.2006.03.003zbMATH Open1171.68555OpenAlexW2099629271MaRDI QIDQ859956FDOQ859956

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

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

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)

Cited In (23)

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

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)