Přístupnostní navigace
E-application
Search Search Close
Publication detail
ABDULLA, P. ATIG, M. CHEN, Y. BUI PHI, D. HOLÍK, L. REZINE, A. RUMMER, P.
Original Title
Trau: SMT solver for string constraints
Type
conference paper
Language
English
Original 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
Authors
ABDULLA, P.; ATIG, M.; CHEN, Y.; BUI PHI, D.; HOLÍK, L.; REZINE, A.; RUMMER, P.
Released
18. 1. 2019
Publisher
FMCAD Inc.
Location
Austin
ISBN
978-0-9835678-8-2
Book
Proceedings of the 18th Conference on Formal Methods in Computer-Aided Design
Pages from
165
Pages to
169
Pages count
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" }