Generating all polynomial invariants in simple loops

DOI10.1016/j.jsc.2007.01.002zbMath1121.13034OpenAlexW1971043610MaRDI QIDQ2457430

Deepak Kapur, Enric Rodríguez-Carbonell

Publication date: 23 October 2007

Published in: Journal of Symbolic Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jsc.2007.01.002

zbMATH Keywords

Gröbner basisloop invariantideal of polynomials

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Gröbner bases; other bases for ideals and modules (e.g., Janet and border bases) (13P10)

Related Items (26)

Recent advances in program verification through computer algebra ⋮ When Is a Formula a Loop Invariant? ⋮ On invariant checking ⋮ Proving total correctness and generating preconditions for loop programs via symbolic-numeric computation methods ⋮ Proving correctness of imperative programs by linearizing constrained Horn clauses ⋮ Analyzing ultimate positivity for solvable systems ⋮ Solving invariant generation for unsolvable loops ⋮ Generating invariants for non-linear loops by linear algebraic methods ⋮ Acceleration of the abstract fixpoint computation in numerical program analysis ⋮ Algebra, Coalgebra, and Minimization in Polynomial Differential Equations ⋮ Aligator: A Mathematica Package for Invariant Generation (System Description) ⋮ Termination of polynomial loops ⋮ Algebra-based synthesis of loops and their invariants (invited paper) ⋮ An Iterative Method for Generating Loop Invariants ⋮ Elimination Techniques for Program Analysis ⋮ Inferring Loop Invariants Using Postconditions ⋮ Unnamed Item ⋮ Generalized homogeneous polynomials for efficient template-based nonlinear invariant synthesis ⋮ Automatic proving or disproving equality loop invariants based on finite difference techniques ⋮ Reasoning Algebraically About P-Solvable Loops ⋮ Abstract Fixpoint Computations with Numerical Acceleration Methods ⋮ O-Minimal Invariants for Discrete-Time Dynamical Systems ⋮ Endomorphisms for Non-trivial Non-linear Loop Invariant Generation ⋮ Discovering non-terminating inputs for multi-path polynomial programs ⋮ A multi-domain incremental analysis engine and its application to incremental resource analysis ⋮ Some decidable results on reachability of solvable systems

Uses Software

• Maple

Cites Work

• Automatic generation of polynomial invariants of bounded degree using abstract interpretation
• Affine relationships among variables of a program
• Computing polynomial program invariants
• Non-linear loop invariant generation using Gröbner bases
• Precise interprocedural analysis through linear algebra
• Inference Rules for Program Annotation
• Logical analysis of programs
• Automatic Generation of Polynomial Loop Invariants
• The synthesis of loop predicates
• Precise interprocedural analysis using random interpretation
• Automata, Languages and Programming
• Static Analysis
• Static Analysis
• Theoretical Aspects of Computing - ICTAC 2004
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Generating all polynomial invariants in simple loops