raSAT: an SMT solver for polynomial constraints

被引：0
|
作者：
Vu Xuan Tung
To Van Khanh
Mizuhito Ogawa
机构：
[1] Japan Advanced Institute of Science and Technology,
[2] University of Engineering and Technology,undefined
[3] Vietnam National University,undefined
来源：
Formal Methods in System Design | 2017年 / 51卷
关键词：
SMT solving; Polynomial constraints; Interval arithmetic; Interval constraint propagation; Testing; Intermediate value theorem;
D O I：
暂无
中图分类号：
学科分类号：
摘要：
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 raSATloop 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
页数：37
相关论文
共 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
12345