Solving Nonlinear SMT Problems Based on an Efficient Lazy Method

ISCAS OpenIR

	Solving Nonlinear SMT Problems Based on an Efficient Lazy Method
	Ji, Xiaohui; Ma, Feifei
	2013
发表期刊	JOURNAL OF INTERNET TECHNOLOGY
ISSN	1607-9264
卷号	14 期号:3 页码:379-386
摘要	Verification and testing for cyber-physical system may involve constraints that have both Boolean and nonlinear numerical expressions. Such constraints are undecidable, so efficiently giving out a solution whose error is within a given bound when the constraints are satisfiable or the answer that there are some contradicts in the constraints when the constraints are unsatisfiable is important. This paper presents an efficient method to solve Boolean combinations of nonlinear numerical constraints. Under the lazy SMT framework, this method combines an iterative optimization method and interval analysis together to solve numerical constraints. A prototype tool is implemented and some experiments were made. The experimental results show that our method is efficient and can solve many problems that other tools cannot.; Verification and testing for cyber-physical system may involve constraints that have both Boolean and nonlinear numerical expressions. Such constraints are undecidable, so efficiently giving out a solution whose error is within a given bound when the constraints are satisfiable or the answer that there are some contradicts in the constraints when the constraints are unsatisfiable is important. This paper presents an efficient method to solve Boolean combinations of nonlinear numerical constraints. Under the lazy SMT framework, this method combines an iterative optimization method and interval analysis together to solve numerical constraints. A prototype tool is implemented and some experiments were made. The experimental results show that our method is efficient and can solve many problems that other tools cannot.
收录类别	SCI
关键词	Smt Nonlinear Numerical Constraints Iterative Optimization Interval Analysis
部门归属	[Ji, Xiaohui] China Univ Geosci, Sch Informat Engn, Beijing, Peoples R China. [Ma, Feifei] Chinese Acad Sci, Inst Software, Comp Sci Lab, Beijing 100864, Peoples R China.
语种	英语
WOS记录号	WOS:000320291200004
引用统计
内容类型	期刊论文
URI标识	http://ir.iscas.ac.cn/handle/311060/16932
专题	中国科学院软件研究所
推荐引用方式 GB/T 7714	Ji, Xiaohui,Ma, Feifei. Solving Nonlinear SMT Problems Based on an Efficient Lazy Method[J]. JOURNAL OF INTERNET TECHNOLOGY,2013,14(3):379-386.
APA	Ji, Xiaohui,&Ma, Feifei.(2013).Solving Nonlinear SMT Problems Based on an Efficient Lazy Method.JOURNAL OF INTERNET TECHNOLOGY,14(3),379-386.
MLA	Ji, Xiaohui,et al."Solving Nonlinear SMT Problems Based on an Efficient Lazy Method".JOURNAL OF INTERNET TECHNOLOGY 14.3(2013):379-386.