DISCOVERER swMATH ID: 7719 Software Authors: Xia B Description: 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. Homepage: http://rd.springer.com/chapter/10.1007/978-3-540-69149-5_58 Related Software: QEPCAD; Maple; REDLOG; Sostools; YALMIP; ISOLATE; RAGlib; SeDuMi; RegularChains; BOTTEMA; RSOLVER; Kronecker; PGB; Epsilon; SYNRAC; Benchmarks; HSolver; ParametricSystemTools; ConstructibleSetTools; PENBMI Cited in: 57 Publications Standard Articles 2 Publications describing the Software, including 2 Publications in zbMATH Year A complete algorithm for automated discovering of a class of inequality-type theorems. Zbl 1125.68406Yang, Lu; Hou, Xiaorong; Xia, Bican 2001 Automated discovering and proving for geometric inequalities. Zbl 0947.03017Yang, Lu; Hou, Xiaorong; Xia, Bican 1999 all top 5 Cited by 91 Authors 19 Xia, Bican 10 Yang, Lu 8 Zhan, Naijun 5 Yang, Zhengfeng 4 Lin, Wang 4 Moreno Maza, Marc 4 Wu, Jinming 4 Zeng, Zhenbing 3 Hou, Xiaorong 3 Li, Xiaoliang 3 Niu, Wei 3 She, Zhikun 3 Tang, Xiaoxian 3 Wang, Renhong 3 Zhang, Zhihai 3 Zhao, Hengjun 2 Boulier, François 2 Chen, Yinghua 2 Chen, Zhenghong 2 Lai, Yisheng 2 Lemaire, François 2 Liu, Jiang 2 Mou, Chenqi 2 Poteaux, Adrien 2 Shen, Liyong 2 Sun, Xianbo 2 Wang, Dongming 2 Yu, Pei 2 Yu, Zhiheng 2 Zhou, Chaochen 1 Alvandi, Parisa 1 Ataei, Masoud 1 Chen, Changbo 1 Chen, Michael Z. Q. 1 Chen, Zhanbo 1 Cheng, Wanyou 1 Dekov, Deko V. 1 Fang, Tian 1 Feng, Yong 1 Ge, Shuzhi Sam 1 Grozdev, Sava I. 1 Guan, Qiang 1 Hasegawa, Yoshihiko 1 Hong, Hoon 1 Huang, Bo 1 Huang, Yanli 1 Jiang, Jianguo 1 Jiang, Xin 1 Kazemi, Mahsa 1 Le, Huu Phuoc 1 Li, Haoyang 1 Li, Lin 1 Li, Yangjia 1 Li, Yaohui 1 Li, Yi 1 Liang, Quanyi 1 Lu, Junjie 1 Montes, Antonio 1 Orange, Sébastien 1 Petitot, Michel 1 Safey El Din, Mohab 1 Schost, Éric 1 Sedoglavic, Alexandre 1 Shen, Fei 1 Shi, Jian 1 Song, Yuqing 1 Verdière, Nathalie 1 Vu, Tan-Van 1 Wang, Lei 1 Wang, Long 1 Wang, Na 1 Wang, Qingguo 1 Wang, Qiuye 1 Wang, Shuling 1 Wibmer, Michael 1 Wu, Wenyuan 1 Wu, Zhifeng 1 Xiao, Rong 1 Xu, Ming 1 Xue, Bai 1 Yao, Yong 1 Yu, Wensheng 1 Yuan, Chunming 1 Zeng, Yingying 1 Zhang, Jingzhong 1 Zhang, Wenmeng 1 Zhang, Xiaolei 1 Zheng, Zewei 1 Zheng, Zhiming 1 Zhong, Jiyu 1 Zhu, Chungang all top 5 Cited in 29 Serials 9 Journal of Symbolic Computation 5 Journal of Systems Science and Complexity 3 Mathematics in Computer Science 3 Science China. Information Sciences 2 Applied Mathematics and Computation 2 Journal of Computational and Applied Mathematics 2 Science in China. Series A 2 Science in China. Series F 1 Computers & Mathematics with Applications 1 Journal of Mathematical Analysis and Applications 1 Mathematical Biosciences 1 Journal of Mathematical Economics 1 SIAM Journal on Control and Optimization 1 Theoretical Computer Science 1 Computer Aided Geometric Design 1 Formal Aspects of Computing 1 Matematichki Bilten 1 International Journal of Bifurcation and Chaos in Applied Sciences and Engineering 1 Computational Complexity 1 Bulletin des Sciences Mathématiques 1 Journal of Difference Equations and Applications 1 Abstract and Applied Analysis 1 Chaos 1 Communications in Nonlinear Science and Numerical Simulation 1 Discrete and Continuous Dynamical Systems. Series B 1 Nonlinear Analysis. Hybrid Systems 1 Frontiers of Computer Science in China 1 Frontiers of Computer Science 1 East Asian Journal on Applied Mathematics all top 5 Cited in 20 Fields 28 Computer science (68-XX) 11 Commutative algebra (13-XX) 9 Numerical analysis (65-XX) 9 Systems theory; control (93-XX) 7 Algebraic geometry (14-XX) 7 Dynamical systems and ergodic theory (37-XX) 6 Mathematical logic and foundations (03-XX) 5 Biology and other natural sciences (92-XX) 4 Field theory and polynomials (12-XX) 4 Ordinary differential equations (34-XX) 4 Operations research, mathematical programming (90-XX) 3 Approximations and expansions (41-XX) 2 Real functions (26-XX) 2 Difference and functional equations (39-XX) 2 Geometry (51-XX) 1 Functions of a complex variable (30-XX) 1 Calculus of variations and optimal control; optimization (49-XX) 1 Mechanics of particles and systems (70-XX) 1 Game theory, economics, finance, and other social and behavioral sciences (91-XX) 1 Mathematics education (97-XX) Citations by Year