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 55 articles , 2 standard articles )
Showing results 1 to 20 of 55.
Sorted by year (- Sun, Xianbo; Wang, Na; Yu, Pei: The monotonicity of ratios of some abelian integrals (2021)
- Alvandi, Parisa; Ataei, Masoud; Kazemi, Mahsa; Moreno Maza, Marc: On the extended Hensel construction and its application to the computation of real limit points (2020)
- Boulier, François; Lemaire, François; Poteaux, Adrien; Moreno Maza, Marc: An equivalence theorem for regular differential chains (2019)
- Huang, Bo; Niu, Wei: Analysis of snapback repellers using methods of symbolic computation (2019)
- Verdière, N.; Orange, S.: A systematic approach for doing an a priori identifiability study of dynamical nonlinear models (2019)
- Vu, Tan Van; Hasegawa, Yoshihiko: An algebraic method to calculate parameter regions for constrained steady-state distribution in stochastic reaction networks (2019)
- Lu, Junjie; She, Zhikun; Ge, Shuzhi Sam; Jiang, Xin: Stability analysis of discrete-time switched systems via multi-step multiple Lyapunov-like functions (2018)
- Wu, Jinming; Zhu, Chungang: The maximum number and its distribution of singular points for parametric piecewise algebraic curves (2018)
- Liang, Quanyi; She, Zhikun; Wang, Lei; Chen, Michael Z. Q.; Wang, Qing-Guo: Characterizations and criteria for synchronization of heterogeneous networks to linear subspaces (2017)
- Li, Yi: Witness to non-termination of linear programs (2017)
- Wang, Qiuye; Li, Yangjia; Xia, Bican; Zhan, Naijun: Generating semi-algebraic invariants for non-autonomous polynomial hybrid systems (2017)
- Grozdev, Sava; Dekov, Deko: Computer discovered mathematics and applications in education (2016)
- Niu, Wei; Shi, Jian; Mou, Chenqi: Analysis of codimension 2 bifurcations for high-dimensional discrete systems using symbolic computation methods (2016)
- Xia, Bican; Yang, Lu: Automated inequality proving and discovering (2016)
- 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)
- Lin, Wang; Wu, Min; Yang, Zhengfeng; Zeng, Zhenbing: Proving total correctness and generating preconditions for loop programs via symbolic-numeric computation methods (2014)
- Liu, Jiang; Xu, Ming; Zhan, Naijun; Zhao, Hengjun: Discovering non-terminating inputs for multi-path polynomial programs (2014)