Automatic Generation of Polynomial Loop Invariants

DOI10.1145/1005285.1005324zbMath1108.13310OpenAlexW1967845657MaRDI QIDQ4657335

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

Related Items (18)

Analysis of linear definite iterative loops ⋮ Recent advances in program verification through computer algebra ⋮ \textit{Theorema}: Towards computer-aided mathematical theory exploration ⋮ A quantifier-elimination based heuristic for automatically generating inductive assertions for programs ⋮ The structure of polynomial invariants of linear loops ⋮ From Polynomial Invariants to Linear Loops ⋮ Change-of-bases abstractions for non-linear hybrid systems ⋮ Solving invariant generation for unsolvable loops ⋮ Symbolic computation in automated program reasoning ⋮ Nonlinear invariants for linear loops and eigenpolynomials of linear operators ⋮ Polynomial invariants for linear loops ⋮ Efficient solution of a class of quantified constraints with quantifier prefix exists-forall ⋮ Generating all polynomial invariants in simple loops ⋮ Termination of polynomial loops ⋮ Constructing invariants for hybrid systems ⋮ Elimination Techniques for Program Analysis ⋮ A method of proving the invariance of linear inequalities for linear loops ⋮ Automatic complexity analysis of integer programs via triangular weakly non-linear loops

Uses Software

• Maple
• Groebner

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