Termination of linear programs with nonlinear constraints

DOI10.1016/j.jsc.2010.06.006zbMath1208.68151OpenAlexW1976104755MaRDI QIDQ604395

Zhi-Hai Zhang, Bican Xia

Publication date: 10 November 2010

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

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

zbMATH Keywords

quantifier eliminationterminationcyclotomic polynomialsemi-algebraic systemrationally independent group

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (9)

Termination of Single-Path Polynomial Loop Programs ⋮ Recent advances in program verification through computer algebra ⋮ What else is undecidable about loops? ⋮ Termination of polynomial loops ⋮ Geometric Quantifier Elimination Heuristics for Automatically Generating Octagonal and Max-plus Invariants ⋮ Unnamed Item ⋮ O-Minimal Invariants for Discrete-Time Dynamical Systems ⋮ Discovering non-terminating inputs for multi-path polynomial programs ⋮ Witness to non-termination of linear programs

Uses Software

• QEPCAD
• REDLOG
• DISCOVERER

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Symbolic decision procedure for termination of linear programs
• Partial cylindrical algebraic decomposition for quantifier elimination
• Computing in the field of complex algebraic numbers
• Discovering Non-linear Ranking Functions by Solving Semi-algebraic Systems
• The size-change principle for program termination
• Computer Aided Verification
• Linear forms in the logarithms of algebraic numbers (IV)
• Verification, Model Checking, and Abstract Interpretation
• Termination of Integer Linear Programs
• Deciding stability and mortality of piecewise affine dynamical systems

This page was built for publication: Termination of linear programs with nonlinear constraints