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
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