Institutional Repository
| Solving Nonlinear SMT Problems Based on an Efficient Lazy Method | |
| Ji, Xiaohui; Ma, Feifei | |
| 2013 | |
| Source | JOURNAL OF INTERNET TECHNOLOGY
 |
| ISSN | 1607-9264 |
| Volume | 14Issue:3Pages:379-386 |
| English Abstract | 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. |
| Indexed Type | SCI |
| Keyword | Smt Nonlinear Numerical Constraints Iterative Optimization Interval Analysis |
| Department | [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. |
| Language | 英语 |
| WOS ID | WOS:000320291200004 |
| Citation statistics | |
| Content Type | 期刊论文 |
| URI | http://ir.iscas.ac.cn/handle/311060/16932 |
| Collection | 中国科学院软件研究所 |
| Recommended Citation 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. |
| Files in This Item: | There are no files associated with this item. | |||||
Items in the repository are protected by copyright, with all rights reserved, unless otherwise indicated.
Edit Comment