Publication Details

Norn: An SMT Solver for String Constraints

ABDULLA Parosh A., ATIG Mohamed F., HOLÍK Lukáš, CHEN Yu-Fang, REZINE Ahmed, RUMMER Philipp and STENMAN Jari. Norn: An SMT Solver for String Constraints. In: Computer Aided Verification. Lecture Notes in Computer Science Volume 9206. Cham: Springer International Publishing, 2015, pp. 462-469. ISBN 978-3-319-21689-8.
Czech title
Norn: SMT řešič pro řetzcová omezení
Type
conference paper
Language
english
Authors
Abdulla Parosh A. (Uppsala)
Atig Mohamed F. (Uppsala)
Holík Lukáš, doc. Mgr., Ph.D. (DITS FIT BUT)
Chen Yu-Fang (ASIN)
Rezine Ahmed, Assoc. Prof. (LIU)
Rummer Philipp (Uppsala)
Stenman Jari (Uppsala)
Keywords

string contraints
SMT
finite automata
Presburger
vulnerability
verification
string equations

Abstract

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.

Annotation

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.

Published
2015
Pages
462-469
Proceedings
Computer Aided Verification
Series
Lecture Notes in Computer Science Volume 9206
Conference
27th International Conference on Computer Aided Verification, San Francisco, California, US
ISBN
978-3-319-21689-8
Publisher
Springer International Publishing
Place
Cham, CH
DOI
10.1007/978-3-319-21690-4_29
UT WoS
000364182900029
EID Scopus
2-s2.0-84951055435
BibTeX 
@INPROCEEDINGS{FITPUB10878,
   author = "A. Parosh Abdulla and F. Mohamed Atig and Luk\'{a}\v{s} Hol\'{i}k and Yu-Fang Chen and Ahmed Rezine and Philipp Rummer and Jari Stenman",
   title = "Norn: An SMT Solver for String Constraints",
   pages = "462--469",
   booktitle = "Computer Aided Verification",
   series = "Lecture Notes in Computer Science Volume 9206",
   year = 2015,
   location = "Cham, CH",
   publisher = "Springer International Publishing",
   ISBN = "978-3-319-21689-8",
   doi = "10.1007/978-3-319-21690-4\_29",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/10878"
}
Back to top