liu.seSearch for publications in DiVA
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • oxford
  • 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
Flatten and Conquer A Framework for Efficient Analysis of String Constraints
Uppsala University, Sweden.
Uppsala University, Sweden.
Academic Sinica, Taiwan.
Uppsala University, Sweden.
Show others and affiliations
2017 (English)In: ACM SIGPLAN NOTICES, ASSOC COMPUTING MACHINERY , 2017, Vol. 52, no 6, 602-617 p.Conference paper, Published paper (Refereed)
Abstract [en]

We describe a uniform and efficient framework for checking the satisfiability of a large class of string constraints. The framework is based on the observation that both satisfiability and unsatisfiability of common constraints can be demonstrated through witnesses with simple patterns. These patterns are captured using flat automata each of which consists of a sequence of simple loops. We build a Counter-Example Guided Abstraction Refinement (CEGAR) framework which contains both an under-and an over-approximation module. The flow of information between the modules allows to increase the precision in an automatic manner. We have implemented the framework as a tool and performed extensive experimentation that demonstrates both the generality and efficiency of our method.

Place, publisher, year, edition, pages
ASSOC COMPUTING MACHINERY , 2017. Vol. 52, no 6, 602-617 p.
Keyword [en]
String Equation; Formal Verification; Automata Theory
National Category
Computer Sciences
Identifiers
URN: urn:nbn:se:liu:diva-143106DOI: 10.1145/3062341.3062384ISI: 000414334200041OAI: oai:DiVA.org:liu-143106DiVA: diva2:1159386
Conference
38th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)
Note

Funding Agencies|Swedish Research Council; Uppsala Programming for Multicore Architectures Research Center (UPMARC); CENIIT research organization [12.04]; MOST [103-2221-E-001 -019 -MY3]; Czech Science Foundation [16-24707Y]; IT4IXS: IT4Innovations Excellence in Science project [LQ1602]

Available from: 2017-11-22 Created: 2017-11-22 Last updated: 2017-11-22

Open Access in DiVA

No full text

Other links

Publisher's full text

Search in DiVA

By author/editor
Rezine, Ahmed
By organisation
Software and SystemsFaculty of Science & Engineering
Computer Sciences

Search outside of DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric score

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

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • oxford
  • 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