Norn: An SMT Solver for String Constraints

被引：63
|
作者：
Abdulla, Parosh Aziz [1 ]
Atig, Mohamed Faouzi [1 ]
Chen, Yu-Fang [2 ]
Holik, Lukas [3 ]
Rezine, Ahmed [4 ]
Rummer, Philipp [1 ]
Stenman, Jari [1 ]
机构：
[1] Uppsala Univ, Dept Informat Technol, Uppsala, Sweden
[2] Acad Sinica, Inst Informat Sci, Taipei, Taiwan
[3] Brno Univ Technol, Fac Informat Technol, CS-61090 Brno, Czech Republic
[4] Linkoping Univ, Dept Comp & Informat Sci, S-58183 Linkoping, Sweden
来源：
COMPUTER AIDED VERIFICATION, PT I | 2015年 / 9206卷
关键词：
D O I：
10.1007/978-3-319-21690-4_29
中图分类号：
TP3 [计算技术、计算机技术];
学科分类号：
0812 ;
摘要：
We present version 1.0 of the Norn SMT solver for string constraints. Norn is a solver for an expressive constraint language, including word equations, length constraints, and regular membership queries. As a feature distinguishing Norn from other SMT solvers, Norn is a decision procedure under the assumption of a set of acyclicity conditions on word equations, without any restrictions on the use of regular membership.
引用
收藏
页码：462 / 469
页数：8
相关论文
共 50 条
  • [1] TRAU : SMT solver for string constraints
    Abdulla, Parosh Aziz
    Atig, Mohamed Faouzi
    Chen, Yu-Fang
    Bui Phi Diep
    Holik, Lukas
    Rezine, Ahmed
    Rummer, Philipp
    PROCEEDINGS OF THE 2018 18TH CONFERENCE ON FORMAL METHODS IN COMPUTER AIDED DESIGN (FMCAD), 2018, : 165 - 169
  • [2] An efficient SMT solver for string constraints
    Tianyi Liang
    Andrew Reynolds
    Nestan Tsiskaridze
    Cesare Tinelli
    Clark Barrett
    Morgan Deters
    Formal Methods in System Design, 2016, 48 : 206 - 234
  • [3] An efficient SMT solver for string constraints
    Liang, Tianyi
    Reynolds, Andrew
    Tsiskaridze, Nestan
    Tinelli, Cesare
    Barrett, Clark
    Deters, Morgan
    FORMAL METHODS IN SYSTEM DESIGN, 2016, 48 (03) : 206 - 234
  • [4] raSAT: an SMT solver for polynomial constraints
    Vu Xuan Tung
    To Van Khanh
    Ogawa, Mizuhito
    FORMAL METHODS IN SYSTEM DESIGN, 2017, 51 (03) : 462 - 499
  • [5] raSAT: an SMT solver for polynomial constraints
    Vu Xuan Tung
    To Van Khanh
    Mizuhito Ogawa
    Formal Methods in System Design, 2017, 51 : 462 - 499
  • [6] raSAT: An SMT Solver for Polynomial Constraints
    Vu Xuan Tung
    To Van Khanh
    Ogawa, Mizuhito
    AUTOMATED REASONING (IJCAR 2016), 2016, 9706 : 228 - 237
  • [7] HAMPI: A Solver for String Constraints
    Kiezun, Adam
    Ganesh, Vijay
    Guo, Philip J.
    Hooimeijer, Pieter
    Ernst, Michael D.
    ISSTA 2009: INTERNATIONAL SYMPOSIUM ON SOFTWARE TESTING AND ANALYSIS, 2009, : 105 - 115
  • [8] Solving Hierarchical Soft Constraints with an SMT Solver
    Hosobe, Hiroshi
    PROCEEDINGS OF 2020 12TH INTERNATIONAL CONFERENCE ON COMPUTER AND AUTOMATION ENGINEERING (ICCAE 2020), 2020, : 42 - 46
  • [9] An Efficient Lazy SMT Solver for Nonlinear Numerical Constraints
    Ji, Xiaohui
    Ma, Feifei
    2012 IEEE 21ST INTERNATIONAL WORKSHOP ON ENABLING TECHNOLOGIES: INFRASTRUCTURE FOR COLLABORATIVE ENTERPRISES (WETICE), 2012, : 324 - 329
  • [10] An SMT Solver for Regular Expressions and Linear Arithmetic over String Length
    Berzish, Murphy
    Kulczynski, Mitja
    Mora, Federico
    Manea, Florin
    Day, Joel D.
    Nowotka, Dirk
    Ganesh, Vijay
    COMPUTER AIDED VERIFICATION, PT II, CAV 2021, 2021, 12760 : 289 - 312
12345