On termination of polynomial programs with equality conditions

DOI10.1016/J.IC.2026.105487MaRDI QIDQ7353770zbMATH OpenFDO

Authors Yangjia Li, Mingshuai Chen, Liangran Zhao, Naijun Zhan, Hui Lu, Guohua Wu, Joost-Pieter Katoen

Publication date 18 September 2026

Published in Information and Computation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/J.IC.2026.105487

Mathematics Subject Classification ID

Theory of computing (68Qxx)

Cites work

• A quantifier-elimination based heuristic for automatically generating inductive assertions for programs
• Alternation for termination
• An abstract interpretation framework for termination
• An algorithm for finding the basis elements of the residue class ring of a zero dimensional polynomial ideal
• Ascending chains of ideals in the polynomial ring
• Automata, Languages and Programming
• Automatic generation of polynomial invariants of bounded degree using abstract interpretation
• Computer Aided Verification
• Computing polynomial program invariants
• Constructive Proof of Hilbert's Theorem on Ascending Chains
• Deciding conditional termination
• Discovering Non-linear Ranking Functions by Solving Semi-algebraic Systems
• Discovering non-terminating inputs for multi-path polynomial programs
• Generating all polynomial invariants in simple loops
• Generating invariants for non-linear loops by linear algebraic methods
• Guarded commands, nondeterminacy and formal derivation of programs
• Hilbert's Tenth Problem is Unsolvable
• scientific article; zbMATH DE number 1701751 (Why is no real title available?)
• scientific article; zbMATH DE number 749580 (Why is no real title available?)
• scientific article; zbMATH DE number 3279238 (Why is no real title available?)
• scientific article; zbMATH DE number 3068536 (Why is no real title available?)
• Length of Polynomial Ascending Chains and Primitive Recursiveness.
• Membership in polynomial ideals over \(\mathcal{Q}\) is exponential space complete
• Non-linear loop invariant generation using Gröbner bases
• On computable numbers, with an application to the Entscheidungsproblem.
• On discrete-time polynomial systems
• On strongest algebraic program invariants
• On termination of integer linear loops
• On the Length of a Hilbert Ascending Chain
• Petri nets and large finite sets
• Polynomial automata: zeroness and applications
• Polynomial loops: beyond termination
• Proving Conditional Termination
• Proving non-termination
• Proving termination of nonlinear command sequences
• Ranking functions for linear-constraint loops
• Reasoning Algebraically About P-Solvable Loops
• Recent advances in program verification through computer algebra
• Reverse mathematical bounds for the termination theorem
• Some complexity results for polynomial ideals
• Some properties of enumeration in the theory of modular systems.
• Static Analysis
• Symbolic decision procedure for termination of linear programs
• Termination of Integer Linear Programs
• Termination of linear loops over the integers
• Termination of linear programs with nonlinear constraints
• Termination of nondeterministic quantum programs
• Termination of single-path polynomial loop programs
• Termination of triangular Integer loops is decidable
• Verification, Model Checking, and Abstract Interpretation
• Verification, Model Checking, and Abstract Interpretation
• Verification, Model Checking, and Abstract Interpretation
• What else is undecidable about loops?
• Über eine Schlußweise aus dem Endlichen ins Unendliche.

This page was built for publication: On termination of polynomial programs with equality conditions

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