Termination of linear programs with nonlinear constraints

DOI10.1016/J.JSC.2010.06.006MaRDI QIDQ604395zbMATH OpenOpenAlexFDO

Authors Bican Xia, Zhi-Hai Zhang

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

cyclotomic polynomialterminationquantifier eliminationsemi-algebraic systemrationally independent group

Mathematics Subject Classification ID

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

Recommendations

• Termination of Integer Linear Programs
• A recursive decision method for termination of linear programs
• Computer Aided Verification
• Witness to non-termination of linear programs
• Termination analysis of linear loop programs

Cites work

• scientific article; zbMATH DE number 1701751 (Why is no real title available?)
• scientific article; zbMATH DE number 3497890 (Why is no real title available?)
• scientific article; zbMATH DE number 1033382 (Why is no real title available?)
• scientific article; zbMATH DE number 1467843 (Why is no real title available?)
• scientific article; zbMATH DE number 3998137 (Why is no real title available?)
• scientific article; zbMATH DE number 3068536 (Why is no real title available?)
• Computer Aided Verification
• Computing in the field of complex algebraic numbers
• Deciding stability and mortality of piecewise affine dynamical systems
• Discovering Non-linear Ranking Functions by Solving Semi-algebraic Systems
• Linear forms in the logarithms of algebraic numbers (IV)
• Partial cylindrical algebraic decomposition for quantifier elimination
• Symbolic decision procedure for termination of linear programs
• Termination of Integer Linear Programs
• The size-change principle for program termination
• Verification, Model Checking, and Abstract Interpretation

Cited in

(20)

• Termination of single-path polynomial loop programs
• Termination of semi-algebraic loop programs
• Discovering non-terminating inputs for multi-path polynomial programs
• Recurrence with affine level mappings is P-time decidable for CLP
• Signature-based method of deciding program~termination
• Witness to non-termination of linear programs
• On termination of integer linear loops
• A recursive decision method for termination of linear programs
• What else is undecidable about loops?
• On the termination of integer loops
• Termination of polynomial loops
• scientific article; zbMATH DE number 7559471 (Why is no real title available?)
• Recent advances in program verification through computer algebra
• Symbolic decision procedure for termination of linear programs
• Termination analysis of linear loop programs
• Termination of Integer Linear Programs
• Geometric Quantifier Elimination Heuristics for Automatically Generating Octagonal and Max-plus Invariants
• Deciding conditional termination
• Computer Aided Verification
• Deciding conditional termination

Describes a project that uses

Uses Software

• DISCOVERER
• REDLOG
• QEPCAD

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

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