raSAT: an SMT solver for polynomial constraints

被引：12

作者：

Vu Xuan Tung ^{[1
]}

To Van Khanh ^{[2
]}

Ogawa, Mizuhito ^{[1
]}

机构：

[1] Japan Adv Inst Sci & Technol, Nomi, Japan

[2] Vietnam Natl Univ, Univ Engn & Technol, Hanoi, Vietnam

来源：

FORMAL METHODS IN SYSTEM DESIGN | 2017年 / 51卷 / 03期

关键词：

SMT solving; Polynomial constraints; Interval arithmetic; Interval constraint propagation; Testing; Intermediate value theorem;

D O I：

10.1007/s10703-017-0284-9

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

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.

引用

页码：462 / 499

页数：38

共 50 条

[21] From simplification to a partial theory solver for non-linear real polynomial constraints
Brown, Christopher W.
Vale-Enriquez, Fernando
JOURNAL OF SYMBOLIC COMPUTATION, 2020, 100 : 72 - 101
[22] PolyAR: A Highly Parallelizable Solver For Polynomial Inequality Constraints Using Convex Abstraction Refinement
Fatnassi, Wael
Shoukry, Yasser
IFAC PAPERSONLINE, 2021, 54 (05): : 43 - 48
[23] Skeletal Approximation Enumeration for SMT Solver Testing
Yao, Peisen
Huang, Heqing
Tang, Wensheng
Shi, Qingkai
Wu, Rongxin
Zhang, Charles
PROCEEDINGS OF THE 29TH ACM JOINT MEETING ON EUROPEAN SOFTWARE ENGINEERING CONFERENCE AND SYMPOSIUM ON THE FOUNDATIONS OF SOFTWARE ENGINEERING (ESEC/FSE '21), 2021, : 1141 - 1153
[24] Predicting SMT Solver Performance for Software Verification
Healy, Andrew
Monahan, Rosemary
Power, James F.
ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2017, (240): : 20 - 37
[25] Z3: An efficient SMT solver
de Moura, Leonardo
Bjorner, Nikolaj
TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, 2008, 4963 : 337 - 340
[26] Learning SMT(LRA) Constraints using SMT Solvers
Kolb, Samuel
Teso, Stefano
Passerini, Andrea
De Raedt, Luc
PROCEEDINGS OF THE TWENTY-SEVENTH INTERNATIONAL JOINT CONFERENCE ON ARTIFICIAL INTELLIGENCE, 2018, : 2333 - 2340
[27] Validation of Derived Features and Well-Formedness Constraints in DSLs By Mapping Graph Queries to an SMT-Solver
Semerath, Oszkar
Horvath, Akos
Varro, Daniel
MODEL-DRIVEN ENGINEERING LANGUAGES AND SYSTEMS, 2013, 8107 : 538 - 554
[28] SMT Solver Testing with Type and Grammar Based Mutation
Park, Jiwon
PROCEEDINGS OF THE 29TH ACM JOINT MEETING ON EUROPEAN SOFTWARE ENGINEERING CONFERENCE AND SYMPOSIUM ON THE FOUNDATIONS OF SOFTWARE ENGINEERING (ESEC/FSE '21), 2021, : 1675 - 1676
[29] veriT: An Open, Trustable and Efficient SMT-Solver
Bouton, Thomas
de Oliveira, Diego Caminha B.
Deharbe, David
Fontaine, Pascal
AUTOMATED DEDUCTION - CADE-22, 2009, 5663 : 151 - +
[30] An Approach for Detecting Infeasible Paths Based on a SMT Solver
Jiang, Shujuan
Wang, Hongyang
Zhang, Yanmei
Xue, Meng
Qian, Junyan
Zhang, Miao
IEEE ACCESS, 2019, 7 : 68058 - 68069

← 1 2 3 4 5 →