Norn: An SMT Solver for String Constraints

被引：64

作者：

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

共 14 条

[1] Abdulla PA, 2014, LECT NOTES COMPUT SC, V8559, P150, DOI 10.1007/978-3-319-08867-9_10
[2] [Anonymous], 2010, NDSS
[3] Bjorner N., 2013, EPIC SERIES, V20, P77
[4] Griggio A., 2012, Journal on Satisfiability, Boolean Modeling and Computation, V8, P1
[5] Kausler Scott., 2014, Proceedings of the 29th ACM/IEEE International Conference on Automated Software Engineering, ASE '14, P259
[6] Kiezun A, 2009, ISSTA 2009: INTERNATIONAL SYMPOSIUM ON SOFTWARE TESTING AND ANALYSIS, P105
[7] Liang TY, 2014, LECT NOTES COMPUT SC, V8559, P646, DOI 10.1007/978-3-319-08867-9_43
[8] S3: A Symbolic String Solver for Vulnerability Detection in Web Applications
Minh-Thai Trinh
Duc-Hiep Chu
Jaffar, Joxan
[J]. CCS'14: PROCEEDINGS OF THE 21ST ACM CONFERENCE ON COMPUTER AND COMMUNICATIONS SECURITY, 2014, : 1232 - 1243
[9] Moller A., 2010, DK BRICS AUTOMATON F
[10] Solving SAT and SAT modulo theories:: From an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T)
Nieuwenhuis, Robert
Oliveras, Albert
Tinelli, Cesare
[J]. JOURNAL OF THE ACM, 2006, 53 (06) : 937 - 977

← 1 2 →