Title :
Detecting Unsatisfiability of Nonlinear Constraints Using DISCOVERER
Author :
Wu, Bin ; Hu, Yingwu ; Bi, Zhongqin
Author_Institution :
Shanghai Key Lab. of Trustworthy Comput., East China Normal Univ., Shanghai, China
Abstract :
Recent advances in program verification indicate that various verification problems can be reduced to semialgebraic system (SAS for short) solving. An SAS consists of polynomial equations and polynomial inequalities. L.Yang invented new theories and algorithms for SAS solving and partly implemented them as a real symbolic computation tool in Maple named discoverer. In this paper, we first introduce the tool discoverer on solving SASs, and then we describe a method how to apply the techniques on solving semi-algebraic systems to detecting unsatisfiability of conjunction of nonlinear equalities and inequalities.
Keywords :
mathematics computing; polynomials; program verification; software tools; Maple; discoverer tool; nonlinear constraint; polynomial equation; polynomial inequalities; program verification; semialgebraic system; Computer science; Constraint theory; Educational institutions; Equations; Hybrid power systems; Information technology; Laboratories; Polynomials; Safety; Synthetic aperture sonar; DISCOVERER; program verification semi-algebraic system;
Conference_Titel :
Information Technology and Computer Science, 2009. ITCS 2009. International Conference on
Conference_Location :
Kiev
Print_ISBN :
978-0-7695-3688-0
DOI :
10.1109/ITCS.2009.277
