Detail publikačního výsledku

Trau : SMT solver for string constraints

ABDULLA, P.; ATIG, M.; CHEN, Y.; BUI PHI, D.; HOLÍK, L.; REZINE, A.; RUMMER, P.

Originální název

Trau : SMT solver for string constraints

Anglický název

Trau : SMT solver for string constraints

Druh

Stať ve sborníku v databázi WoS či Scopus

Originální abstrakt

We introduce TRAU, an SMT solver for an expressive constraint language, including word equations, length constraints, context-free membership queries, and transducer constraints. The satisfiability problem for such a class of constraints is in general undecidable. The key idea behind TRAU is a technique called flattening, which searches for satisfying assignments that follow simple patterns. TRAU implements a Counter-Example Guided Abstraction Refinement (CEGAR) framework which contains both an under- and an over-approximation module. The approximations are refined in an automatic manner by information flow between the two modules. The technique implemented by TRAU can handle a rich class of string constraints and has better performance than state-of-the-art string solvers.

Anglický abstrakt

We introduce TRAU, an SMT solver for an expressive constraint language, including word equations, length constraints, context-free membership queries, and transducer constraints. The satisfiability problem for such a class of constraints is in general undecidable. The key idea behind TRAU is a technique called flattening, which searches for satisfying assignments that follow simple patterns. TRAU implements a Counter-Example Guided Abstraction Refinement (CEGAR) framework which contains both an under- and an over-approximation module. The approximations are refined in an automatic manner by information flow between the two modules. The technique implemented by TRAU can handle a rich class of string constraints and has better performance than state-of-the-art string solvers.

Klíčová slova

security, web applications, string constraint, automata, flat languages, abstraction, over-under approximation

Klíčová slova v angličtině

security, web applications, string constraint, automata, flat languages, abstraction, over-under approximation

Autoři

ABDULLA, P.; ATIG, M.; CHEN, Y.; BUI PHI, D.; HOLÍK, L.; REZINE, A.; RUMMER, P.

Rok RIV

2019

Vydáno

18.01.2019

Nakladatel

FMCAD Inc.

Místo

Austin

ISBN

978-0-9835678-8-2

Kniha

Proceedings of the 18th Conference on Formal Methods in Computer-Aided Design

Strany od

165

Strany do

169

Strany počet

5

URL

https://www.cs.utexas.edu/users/hunt/FMCAD/FMCAD18/fmcad2018_proceedings.pdf

BibTex

@inproceedings{BUT155122,
  author="Parosh {Abdulla} and Mohamed {Atig} and Yu-Fang {Chen} and Diep {Bui Phi} and Lukáš {Holík} and Ahmed {Rezine} and Philipp {Rummer}",
  title="Trau : SMT solver for string constraints",
  booktitle="Proceedings of the 18th Conference on Formal Methods in Computer-Aided Design",
  year="2019",
  pages="165--169",
  publisher="FMCAD Inc.",
  address="Austin",
  doi="10.23919/FMCAD.2018.8602997",
  isbn="978-0-9835678-8-2",
  url="https://www.cs.utexas.edu/users/hunt/FMCAD/FMCAD18/fmcad2018_proceedings.pdf"
}

Dokumenty

fmcad