Result Details

Trau : SMT solver for string constraints

ABDULLA, P.; ATIG, M.; CHEN, Y.; BUI PHI, D.; HOLÍK, L.; REZINE, A.; RUMMER, P. Trau : SMT solver for string constraints. In Proceedings of the 18th Conference on Formal Methods in Computer-Aided Design. Austin: FMCAD Inc., 2019. p. 165-169. ISBN: 978-0-9835678-8-2.
Type
conference paper
Language
English
Authors
Abdulla Parosh
Atig Mohamed, FIT (FIT)
Chen Yu-Fang
Bui Phi Diep, FIT (FIT)
Holík Lukáš, doc. Mgr., Ph.D., DITS (FIT)
Rezine Ahmed, Assoc. Prof.
Rummer Philipp
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.

Keywords

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

URL
Published
2019
Pages
165–169
Proceedings
Proceedings of the 18th Conference on Formal Methods in Computer-Aided Design
Conference
Formal Methods in Computer-Aided Design
ISBN
978-0-9835678-8-2
Publisher
FMCAD Inc.
Place
Austin
DOI
UT WoS
000493916300025
EID Scopus
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"
}
Files
Projects
Bezpečné a spolehlivé počítačové systémy, BUT, Vnitřní projekty VUT, FIT-S-17-4014, start: 2017-03-01, end: 2020-02-29, completed
Efficient Automata Techniques for Formal Reasoning, GACR, Juniorské granty, GJ16-24707Y, start: 2016-01-01, end: 2018-12-31, completed
IT4Innovations excellence in science, MŠMT, Národní program udržitelnosti II, LQ1602, start: 2016-01-01, end: 2020-12-31, completed
Research groups
Departments
Back to top