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

DOI10.1007/978-3-540-75292-9_3MaRDI QIDQ3525073zbMATH OpenOpenAlexFDO

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

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 algebraDISCOVERERloop terminationpolynomial programsprogram verificationQEPCADranking functionsemi-algebraic systems

Mathematics Subject Classification ID

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

Recommendations

• Generating exact nonlinear ranking functions by symbolic-numeric hybrid method
• Generating Polynomial Invariants with DISCOVERER and QEPCAD
• Recent advances in program verification through computer algebra
• Detection of ranking functions of polynomial loop programs
• scientific article; zbMATH DE number 1701751

Cited in

(11)

• Synthesizing ranking functions for loop programs via SVM
• Discovering non-terminating inputs for multi-path polynomial programs
• Witness to non-termination of linear programs
• Proving total correctness and generating preconditions for loop programs via symbolic-numeric computation methods
• Termination of single-path polynomial loop programs
• Recent advances in program verification through computer algebra
• Generating exact nonlinear ranking functions by symbolic-numeric hybrid method
• On invariant checking
• scientific article; zbMATH DE number 7559471 (Why is no real title available?)
• Termination of linear programs with nonlinear constraints
• A new look at the automatic synthesis of linear ranking functions

Describes a project that uses

Uses Software

• QEPCAD
• REDLOG
• DISCOVERER

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

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