Linköping University: Students Alumni Trade and Industry/Society Internal Search
ahmre43_PLDI2017

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

Parosh Aziz Abdulla
 
Mohamed Faouzi Atig
Yu-Fang Chen
 
Bui Phi Diep
Lukas Holik
 
Ahmed Rezine
Philipp Rummer

PLDI 2017 Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation

ABSTRACT
We describe a uniform and efficient framework for check- ing the satisfiability of a large class of string constraints. The framework is based on the observation that both sat- isfiability 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 (CE- GAR) framework which contains both an under- and an over-approximation module. The flow of information be- tween the modules allows to increase the precision in an au- tomatic manner. We have implemented the framework as a tool and performed extensive experimentation that demon- strates both the generality and efficiency of our method.


[AFCP17] Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Bui Phi Diep, Lukas Holik, Ahmed Rezine, Philipp Rummer, "Flatten and conquer: a framework for efficient analysis of string constraints", PLDI 2017 Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation
( ! ) perl script by Giovanni Squillero with modifications from Gert Jervan   (v3.1, p5.2, September-2002-)