DISCOVERER
DISCOVERER: a tool for solving semi-algebraic systems; Program Verification by Using DISCOVERER. Recent advances in program verification indicate that various verification problems can be reduced to semi-algebraic system (SAS for short) solving. An SAS consists of polynomial equations and polynomial inequalities. Algorithms for quantifier elimination of real closed fields are the general method for those problems. But the general method usually has low efficiency for specific problems. To overcome the bottleneck of program verification with a symbolic approach, one has to combine special techniques with the general method. Based on the work of complete discrimination systems of polynomials [33,31],, we invented new theories and algorithms [32,30,35] for SAS solving and partly implemented them as a real symbolic computation tool in Maple named DISCOVERER. In this paper, we first summarize the results that we have done so far both on SAS-solving and program verification with DISCOVERER, and then discuss the future work in this direction, including SAS-solving itself, termination analysis and invariant generation of programs, and reachability computation of hybrid systems etc.
Keywords for this software
References in zbMATH (referenced in 23 articles )
Showing results 1 to 20 of 23.
Sorted by year (- Chen, Zhenghong; Tang, Xiaoxian; Xia, Bican: Generic regular decompositions for parametric polynomial systems (2015)
- Hong, Hoon; Tang, Xiaoxian; Xia, Bican: Special algorithm for stability analysis of multistable biological regulatory systems (2015)
- Wu, Jinming; Wang, Renhong; Zhang, Xiaolei: Real root classification of parametric spline functions (2015)
- Lin, Wang; Wu, Min; Yang, Zhengfeng; Zeng, Zhenbing: Exact safety verification of hybrid systems using sums-of-squares representation (2014)
- Liu, Jiang; Xu, Ming; Zhan, Naijun; Zhao, Hengjun: Discovering non-terminating inputs for multi-path polynomial programs (2014)
- Li, Yaohui; Song, Yuqing; Wu, Zhifeng: Signature-based method of deciding program termination (2014)
- Shen, Fei; Wu, Wenyuan; Xia, Bican: Real root isolation of polynomial equations based on hybrid computation (2014)
- Shen, Liyong; Wu, Min; Yang, Zhengfeng; Zeng, Zhenbing: Generating exact nonlinear ranking functions by symbolic-numeric hybrid method (2013)
- She, Zhikun; Li, Haoyang; Xue, Bai; Zheng, Zhiming; Xia, Bican: Discovering polynomial Lyapunov functions for continuous dynamical systems (2013)
- Wu, Min; Yang, Zhengfeng; Lin, Wang: Exact asymptotic stability analysis and region-of-attraction estimation for nonlinear systems (2013)
- Liu, Jiang; Zhan, Naijun; Zhao, Hengjun: Automatically discovering relaxed Lyapunov functions for polynomial dynamical systems (2012)
- Boulier, François; Lemaire, François; Petitot, Michel; Sedoglavic, Alexandre: Chemical reaction systems, computer algebra and systems biology. (Invited talk) (2011)
- Chen, Ying; Shen, Li-Yong; Yuan, Chun-Ming: Collision and intersection detection of two ruled surfaces using bracket method (2011)
- Lai, Yisheng; Wang, Renhong; Wu, Jinming: Solving parametric piecewise polynomial systems (2011)
- Li, Xiaoliang; Mou, Chenqi; Niu, Wei; Wang, Dongming: Stability analysis for discrete biological models using algebraic methods (2011)
- Xia, Bican; Yang, Lu; Zhan, Naijun; Zhang, Zhihai: Symbolic decision procedure for termination of linear programs (2011)
- Zhang, ZhiHai; Fang, Tian; Xia, BiCan: Real solution isolation with multiplicity of zero-dimensional triangular systems (2011)
- Xia, Bican; Zhang, Zhihai: Termination of linear programs with nonlinear constraints (2010)
- Yang, Lu; Zhou, Chaochen; Zhan, Naijun; Xia, Bican: Recent advances in program verification through computer algebra (2010)
- Yang, Lu; Zhan, Naijun; Xia, Bican; Zhou, Chaochen: Program verification by using DISCOVERER (2008)