Conference paper

ABDULLA Parosh A., ATIG Mohamed F., BUI Phi Diep, HOLÍK Lukáš, CHEN Yu-Fang, REZINE Ahmed and RUMMER Philipp. Trau: SMT solver for string constraints. In: Proceedings of the 18th Conference on Formal Methods in Computer-Aided Design. Austin: FMCAD Inc., 2019, pp. 1-5. ISBN 978-0-9835678-8-2. Available from:
Publication language:english
Original title:Trau: SMT solver for string constraints
Title (cs):Trau: řešič řetězcových omezení
Proceedings:Proceedings of the 18th Conference on Formal Methods in Computer-Aided Design
Conference:Formal Methods in Computer-Aided Design
Place:Austin, US
Publisher:FMCAD Inc.
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.
   author = {A. Parosh Abdulla and F. Mohamed Atig and Diep Phi
	Bui and Luk{\'{a}}{\v{s}} Hol{\'{i}}k and Yu-Fang
	Chen and Ahmed Rezine and Philipp Rummer},
   title = {Trau: SMT solver for string constraints},
   pages = {1--5},
   booktitle = {Proceedings of the 18th Conference on Formal Methods in
	Computer-Aided Design},
   year = {2019},
   location = {Austin, US},
   publisher = {FMCAD Inc.},
   ISBN = {978-0-9835678-8-2},
   doi = {10.23919/FMCAD.2018.8602997},
   language = {english},
   url = {}

Your IPv4 address:
Switch to https

DNSSEC [dnssec]