Faculty of Information Technology, BUT

Publication Details

Flatten and conquer: a framework for efficient analysis of string constraints

ABDULLA Parosh A., ATIG Mohamed F., BUI Phi Diep, HOLÍK Lukáš, CHEN Yu-Fang, REZINE Ahmed and RUMMER Philipp. Flatten and conquer: a framework for efficient analysis of string constraints. In: Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation. ACM. New York: Association for Computing Machinery, 2017, pp. 602-617. ISBN 978-1-4503-4988-8. Available from: https://dl.acm.org/citation.cfm?doid=3062341.3062384
Czech title
Rozplácni a panuj: efektivní analýza ř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
Automata Theory, Formal Verification, String Equation
Abstract
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.
Published
2017
Pages
602-617
Proceedings
Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation
Series
ACM
Conference
ACM SIGPLAN Conference on Programming Language Design and Implementation, Barcelona, ES
ISBN
978-1-4503-4988-8
Publisher
Association for Computing Machinery
Place
New York, US
DOI
BibTeX
@INPROCEEDINGS{FITPUB11577,
   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 = "Flatten and conquer: a framework for efficient analysis of string constraints",
   pages = "602--617",
   booktitle = "Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation",
   series = "ACM",
   year = 2017,
   location = "New York, US",
   publisher = "Association for Computing Machinery",
   ISBN = "978-1-4503-4988-8",
   doi = "10.1145/3062341.3062384",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/11577"
}
Back to top