Algebraic and algorithmic methods for computing polynomial loop invariants

DOI10.1016/J.JSC.2025.102551MaRDI QIDQ7289920zbMATH OpenFDO

Authors Erdenebayar Bayarmagnai, Fatemeh Mohammadi

Publication date 6 July 2026

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

Full work available at URL https://doi.org/10.1016/J.JSC.2025.102551

Mathematics Subject Classification ID

Computational aspects and applications of commutative rings (13Pxx) Theory of software (68Nxx) Algorithms in computer science (68Wxx)

Cites work

• (Un)solvable loop analysis
• A survey on signature-based algorithms for computing Gröbner bases
• Affine relationships among variables of a program
• Algebra-Based Loop Analysis
• Algebraic tools for computing polynomial loop invariants
• Algorithms in real algebraic geometry
• An algorithm for solving parametric linear systems
• Ascending chains of ideals in the polynomial ring
• Automata, Languages and Programming
• Automatic generation of polynomial invariants of bounded degree using abstract interpretation
• Automatic Generation of Polynomial Loop Invariants
• Computations in algebraic geometry with Macaulay 2
• Computing polynomial program invariants
• Constructive Proof of Hilbert's Theorem on Ascending Chains
• Generating all polynomial invariants in simple loops
• scientific article; zbMATH DE number 52945 (Why is no real title available?)
• scientific article; zbMATH DE number 1201576 (Why is no real title available?)
• scientific article; zbMATH DE number 527343 (Why is no real title available?)
• Ideals, varieties, and algorithms. An introduction to computational algebraic geometry and commutative algebra
• Invariant generation for multi-path loops with polynomial assignments
• Length of Polynomial Ascending Chains and Primitive Recursiveness.
• Logical analysis of programs
• Modern computer algebra
• msolve. A library for solving polynomial systems
• Non-linear loop invariant generation using Gröbner bases
• On strongest algebraic program invariants
• On the bit-complexity of sparse polynomial and series multiplication
• On the computation of the Zariski closure of finitely generated groups of matrices
• Polynomial automata: zeroness and applications
• Polynomial invariants by linear algebra
• Polynomial Invariants for Affine Programs
• Reasoning Algebraically About P-Solvable Loops
• Sharp Effective Nullstellensatz
• Solving invariant generation for unsolvable loops
• Synthesizing invariants by solving solvable loops
• The complexity of the word problems for commutative semigroups and polynomial ideals
• Trajectories of polynomial vector fields and ascending chains of polynomial ideals

This page was built for publication: Algebraic and algorithmic methods for computing polynomial loop invariants

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