raSAT: an SMT solver for polynomial constraints |
| |
Authors: | Vu Xuan Tung To Van Khanh Mizuhito Ogawa |
| |
Affiliation: | 1.Japan Advanced Institute of Science and Technology,Nomi,Japan;2.University of Engineering and Technology, Vietnam National University,Hanoi,Vietnam |
| |
Abstract: | This paper presents raSAT SMT solver, which is aimed to handle polynomial constraints over both reals and integers with simple unified methodologies. Its three main features are (1) a raSAT loop for inequalities, which adds testing to interval constraint propagation to accelerate SAT detection, (2) a non-constructive reasoning for equations over reals based on the generalized intermediate value theorem, and (3) soundness of floating-point arithmetic that is guaranteed by (a) rounding up/down over-approximations of intervals, and (b) confirmation of a satisfying instance detected by testing using the iRRAM package, which guarantees error bounds. |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|