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 条

[21] Semantic Subtyping with an SMT Solver
Bierman, Gavin M.
Gordon, Andrew D.
Hritcu, Catalin
Langworthy, David
ICFP 2010: PROCEEDINGS OF THE 2010 ACM SIGPLAN INTERNATIONAL CONFERENCE ON FUNCTIONAL PROGRAMMING, 2010, : 105 - 116
[22] SyGuS Techniques in the Core of an SMT Solver
Reynolds, Andrew
Tinelli, Cesare
ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2017, (260): : 81 - 96
[23] The MathSAT5 SMT Solver
Cimatti, Alessandro
Griggio, Alberto
Schaafsma, Bastiaan Joost
Sebastiani, Roberto
TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, TACAS 2013, 2013, 7795 : 93 - 107
[24] 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
[25] Predicting SMT Solver Performance for Software Verification
Healy, Andrew
Monahan, Rosemary
Power, James F.
ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2017, (240): : 20 - 37
[26] Z3: An efficient SMT solver
de Moura, Leonardo
Bjorner, Nikolaj
TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, 2008, 4963 : 337 - 340
[27] 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
[28] 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
[29] CertiStr: A Certified String Solver
Kan, Shuanglong
Lin, Anthony Widjaja
Rummer, Philipp
Schrader, Micha
PROCEEDINGS OF THE 11TH ACM SIGPLAN INTERNATIONAL CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS (CPP '22), 2022, : 210 - 224
[30] 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

← 1 2 3 4 5 →