Publication Details
Trau : SMT solver for string constraints
Atig Mohamed
Chen Yu-Fang
Bui Phi Diep
Holík Lukáš, doc. Mgr., Ph.D. (DITS)
Rezine Ahmed, Assoc. Prof.
Rummer Philipp
security, web applications, string constraint, automata, flat languages,
abstraction, over-under approximation
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.
@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"
}