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 条
  • [31] 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 - +
  • [32] 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
  • [33] SMT Solver-Based Cryptanalysis of Block Ciphers
    Sahu H.K.
    Pillai N.R.
    Gupta I.
    Sharma R.K.
    SN Computer Science, 2020, 1 (3)
  • [34] Separation Logic Verification of C Programs with an SMT Solver
    Botincan, Matko
    Parkinson, Matthew
    Schulte, Wolfram
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2009, 254 (5-23) : 5 - 23
  • [35] The VeriFast program verifier and its SMT solver interaction
    Jacobs, Bart
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2015, (186): : 2 - 2
  • [36] Smt-Switch: A Solver-Agnostic C plus plus API for SMT Solving
    Mann, Makai
    Wilson, Amalee
    Zohar, Yoni
    Stuntz, Lindsey
    Irfan, Ahmed
    Brown, Kristopher
    Donovick, Caleb
    Guman, Allison
    Tinelli, Cesare
    Barrett, Clark
    THEORY AND APPLICATIONS OF SATISFIABILITY TESTING, SAT 2021, 2021, 12831 : 377 - 386
  • [37] SMT for Polynomial Constraints on Real Numbers
    To Van Khanh
    Ogawa, Mizuhito
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2012, 289 : 27 - 40
  • [38] Constraints decomposition for RTL verification by SMT
    Zhao, Yanni
    Bian, Jinian
    Deng, Shujun
    Jisuanji Fuzhu Sheji Yu Tuxingxue Xuebao/Journal of Computer-Aided Design and Computer Graphics, 2010, 22 (02): : 234 - 239
  • [39] Lemma learning in SMT on linear constraints
    Yu, Yinlei
    Malik, Sharad
    THEORY AND APPLICATIONS OF SATISFIABILITY TESTING - SAT 2006, PROCEEDINGS, 2006, 4121 : 142 - 155
  • [40] Applying an SMT Solver to Coverage-Driven Design Verification
    Hamaguchi, Kiyoharu
    IEICE TRANSACTIONS ON FUNDAMENTALS OF ELECTRONICS COMMUNICATIONS AND COMPUTER SCIENCES, 2018, E101A (07): : 1053 - 1056
12345