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

Volume

2

fYear

2009

fDate

25-26 July 2009

Firstpage

15

Lastpage

18

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;

fLanguage

English

Publisher

ieee

Conference_Titel

Information Technology and Computer Science, 2009. ITCS 2009. International Conference on

Conference_Location

Kiev

Print_ISBN

978-0-7695-3688-0

Type

conf

DOI

10.1109/ITCS.2009.277

Filename

5190171