Faculty of Information Technology, BUT

Publication Details

Trau: SMT solver for string constraints

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: https://www.cs.utexas.edu/users/hunt/FMCAD/FMCAD18/fmcad2018_proceedings.pdf
Czech title
Trau: řešič řetězcových omezení
Type
conference paper
Language
english
Authors
Abdulla Parosh A. (Uppsala)
Atig Mohamed F. (Uppsala)
Bui Phi Diep (Uppsala)
Holík Lukáš, Mgr., Ph.D. (DITS FIT BUT)
Chen Yu-Fang (ASIN)
Rezine Ahmed (LIU)
Rummer Philipp (Uppsala)
URL
Keywords
security, web applications, string constraint, automata, flat languages, abstraction, over-under approximation
Abstract
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.
Published
2019
Pages
1-5
Proceedings
Proceedings of the 18th Conference on Formal Methods in Computer-Aided Design
Conference
Formal Methods in Computer-Aided Design, Austin, Texas, US
ISBN
978-0-9835678-8-2
Publisher
FMCAD Inc.
Place
Austin, US
DOI
BibTeX
@INPROCEEDINGS{FITPUB11906,
   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 = "https://www.fit.vut.cz/research/publication/11906"
}
Back to top