Publication detail

Norn: An SMT Solver for String Constraints

HOLÍK, L. CHEN, Y. REZINE, A. RUMMER, P. STENMAN, J. ABDULLA, P. ATIG, M.

Original Title

Norn: An SMT Solver for String Constraints

Type

conference paper

Language

English

Original 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.

Keywords

string contraints
SMT
finite automata
Presburger
vulnerability
verification
string equations

Authors

HOLÍK, L.; CHEN, Y.; REZINE, A.; RUMMER, P.; STENMAN, J.; ABDULLA, P.; ATIG, M.

RIV year

2015

Released

27. 4. 2015

Publisher

Springer International Publishing

Location

Cham

ISBN

978-3-319-21689-8

Book

Computer Aided Verification

Edition

Lecture Notes in Computer Science Volume 9206

Pages from

462

Pages to

469

Pages count

7

BibTex

@inproceedings{BUT120376,
  author="Lukáš {Holík} and Yu-Fang {Chen} and Ahmed {Rezine} and Philipp {Rummer} and Jari {Stenman} and Parosh {Abdulla} and Mohamed {Atig}",
  title="Norn: An SMT Solver for String Constraints",
  booktitle="Computer Aided Verification",
  year="2015",
  series="Lecture Notes in Computer Science Volume 9206",
  pages="462--469",
  publisher="Springer International Publishing",
  address="Cham",
  doi="10.1007/978-3-319-21690-4\{_}29",
  isbn="978-3-319-21689-8"
}