Automatic Generation of Polynomial Loop Invariants

DOI10.1145/1005285.1005324MaRDI QIDQ4657335zbMATH OpenOpenAlexFDO

Authors Enric Rodríguez-Carbonell, Deepak Kapur

Publication date 14 March 2005

Published in Proceedings of the 2004 international symposium on Symbolic and algebraic computation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/1005285.1005324

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) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Generating all polynomial invariants in simple loops
• Theoretical Aspects of Computing - ICTAC 2004
• The structure of polynomial invariants of linear loops
• A complete invariant generation approach for P-solvable loops
• Polynomial invariants by linear algebra

Cited in

(37)

• Reasoning Algebraically About P-Solvable Loops
• Automatic complexity analysis of integer programs via triangular weakly non-linear loops
• Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops
• Automatic generation of polynomial invariants of bounded degree using abstract interpretation
• A quantifier-elimination based heuristic for automatically generating inductive assertions for programs
• Inference of polynomial invariants for imperative programs: a farewell to Gröbner bases
• Invariant generation for multi-path loops with polynomial assignments
• Generating all polynomial invariants in simple loops
• A data driven approach for algebraic loop invariants
• Symbolic computation in automated program reasoning
• Analysis of linear definite iterative loops
• Invariant relations for affine loops
• Static Analysis
• Automatic generation of non-linear loop invariants
• Nonlinear invariants for linear loops and eigenpolynomials of linear operators
• Automatic Construction and Verification of Isotopy Invariants
• \textit{Theorema}: Towards computer-aided mathematical theory exploration
• Termination of polynomial loops
• Deciding properties of affine loops
• Algebra-Based Loop Synthesis
• The structure of polynomial invariants of linear loops
• Automatic Generation of Invariants for Circular Derivations in SUP(LA)
• From Polynomial Invariants to Linear Loops
• Efficient solution of a class of quantified constraints with quantifier prefix exists-forall
• Change-of-bases abstractions for non-linear hybrid systems
• Polynomial invariants by linear algebra
• Recent advances in program verification through computer algebra
• Constructing invariants for hybrid systems
• Affine Loop Invariant Generation via Matrix Algebra
• Algebra-Based Reasoning for Loop Synthesis
• A method of proving the invariance of linear inequalities for linear loops
• Solving invariant generation for unsolvable loops
• Targeting Completeness: Using Closed Forms for Size Bounds of Integer Programs
• Polynomial invariants for linear loops
• Elimination Techniques for Program Analysis
• A complete invariant generation approach for P-solvable loops
• Non-linear loop invariant generation using Gröbner bases

Describes a project that uses

Uses Software

• Groebner
• Maple

This page was built for publication: Automatic Generation of Polynomial Loop Invariants

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