Conference paper

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. 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
Publication language:english
Original title:Flatten and conquer: a framework for efficient analysis of string constraints
Title (cs):Rozplácni a panuj: efektivní analýza řetězcových omezení
Pages:602-617
Proceedings:Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation
Conference:ACM SIGPLAN Conference on Programming Language Design and Implementation
Series:ACM
Place:New York, US
Year:2017
URL:https://dl.acm.org/citation.cfm?doid=3062341.3062384
ISBN:978-1-4503-4988-8
DOI:10.1145/3062341.3062384
Publisher:Association for Computing Machinery
Keywords
Automata Theory, Formal Verification, String Equation
Annotation
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.
BibTeX:
@INPROCEEDINGS{
   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 = {http://www.fit.vutbr.cz/research/view_pub.php?id=11577}
}

Your IPv4 address: 54.227.157.163