Discovering Non-linear Ranking Functions by Solving Semi-algebraic Systems

DOI10.1007/978-3-540-75292-9_3zbMath1147.68442OpenAlexW1597204268MaRDI QIDQ3525073

Naijun Zhan, Bican Xia, Lu Yang, Chaochen Zhou, Yinghua Chen

Publication date: 17 September 2008

Published in: Theoretical Aspects of Computing – ICTAC 2007 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-75292-9_3

zbMATH Keywords

computer algebraranking functionprogram verificationpolynomial programsloop terminationsemi-algebraic systemsDISCOVERERQEPCAD

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (10)

Termination of Single-Path Polynomial Loop Programs ⋮ Recent advances in program verification through computer algebra ⋮ Termination of linear programs with nonlinear constraints ⋮ Generating exact nonlinear ranking functions by symbolic-numeric hybrid method ⋮ On invariant checking ⋮ Proving total correctness and generating preconditions for loop programs via symbolic-numeric computation methods ⋮ Unnamed Item ⋮ Synthesizing ranking functions for loop programs via SVM ⋮ Discovering non-terminating inputs for multi-path polynomial programs ⋮ Witness to non-termination of linear programs

Uses Software

• QEPCAD
• REDLOG
• DISCOVERER

This page was built for publication: Discovering Non-linear Ranking Functions by Solving Semi-algebraic Systems