uu.seUppsala University Publications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Trau: SMT solver for string constraints
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
Show others and affiliations
2018 (English)In: Proceedings of the 2018 18th Conference on Formal Methods in Computer Aided Design (FMCAD), IEEE, 2018Conference paper, Published paper (Refereed)
Abstract [en]

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.

Place, publisher, year, edition, pages
IEEE, 2018.
National Category
Computer Sciences
Identifiers
URN: urn:nbn:se:uu:diva-367967DOI: 10.23919/FMCAD.2018.8602997ISI: 000493916300025ISBN: 978-0-9835678-8-2 (electronic)OAI: oai:DiVA.org:uu-367967DiVA, id: diva2:1267288
Conference
18th Conference on Formal Methods in Computer-Aided Design (FMCAD), October 30-November 2, 2018, Austin, USA
Funder
Swedish Research Council, 2014-5484Swedish Foundation for Strategic Research , RIT17-0011Available from: 2018-11-30 Created: 2018-11-30 Last updated: 2019-12-06Bibliographically approved

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full texthttps://www.cs.utexas.edu/users/hunt/FMCAD/FMCAD18/

Authority records BETA

Abdulla, Parosh AzizAtig, Mohamed FaouziBui, Phi DiepRümmer, Philipp

Search in DiVA

By author/editor
Abdulla, Parosh AzizAtig, Mohamed FaouziBui, Phi DiepRümmer, Philipp
By organisation
Computer Systems
Computer Sciences

Search outside of DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetric score

doi
isbn
urn-nbn
Total: 710 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf