Generating exact nonlinear ranking functions by symbolic-numeric hybrid method

DOI10.1007/S11424-013-1004-1MaRDI QIDQ394460zbMATH OpenOpenAlexDBLPWikidataFDO

Authors Li-Yong Shen, Min Wu, Zhengfeng Yang, Zhenbing Zeng

Publication date 27 January 2014

Published in Journal of Systems Science and Complexity (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s11424-013-1004-1

zbMATH Keywords

semidefinite programmingranking functionprogram verificationsymbolic-numeric hybrid method

Mathematics Subject Classification ID

Semidefinite programming (90C22)

Recommendations

• Detection of ranking functions of polynomial loop programs
• Discovering Non-linear Ranking Functions by Solving Semi-algebraic Systems
• Proving total correctness and generating preconditions for loop programs via symbolic-numeric computation methods
• A new look at the automatic synthesis of linear ranking functions
• Automata, Languages and Programming

Cites work

• scientific article; zbMATH DE number 1701751 (Why is no real title available?)
• scientific article; zbMATH DE number 527343 (Why is no real title available?)
• scientific article; zbMATH DE number 1903370 (Why is no real title available?)
• CONCUR 2005 – Concurrency Theory
• Computer Aided Verification
• Discovering Non-linear Ranking Functions by Solving Semi-algebraic Systems
• Exact certification in global polynomial optimization via sums-of-squares of rational functions with rational coefficients
• On Computable Numbers, with an Application to the Entscheidungsproblem
• On the complexity of Putinar's Positivstellensatz
• Recent advances in program verification through computer algebra
• Termination of Integer Linear Programs
• The Computational Complexity of Simultaneous Diophantine Approximation Problems
• Using SeDuMi 1.02, A Matlab toolbox for optimization over symmetric cones
• Verification, Model Checking, and Abstract Interpretation
• Verification, Model Checking, and Abstract Interpretation
• Verification, Model Checking, and Abstract Interpretation

Cited in

(5)

• A new look at the automatic synthesis of linear ranking functions
• Discovering Non-linear Ranking Functions by Solving Semi-algebraic Systems
• Reachable set estimation and safety verification of nonlinear systems via iterative sums of squares programming
• Proving total correctness and generating preconditions for loop programs via symbolic-numeric computation methods
• Synthesizing ranking functions for loop programs via SVM

Describes a project that uses

Uses Software

• DISCOVERER
• YALMIP
• SeDuMi
• Sostools
• RAGlib

This page was built for publication: Generating exact nonlinear ranking functions by symbolic-numeric hybrid method

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