Publication result 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

English Title

Norn: An SMT Solver for String Constraints

Type

Paper in proceedings (conference paper)

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.

English 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

Key words in English

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

2016

Released

27.04.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"
}