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

PA Abdulla, MF Atig, YF Chen, BP Diep, L Holík… - ACM SIGPLAN …, 2017 - dl.acm.org
ACM SIGPLAN Notices, 2017dl.acm.org
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 …
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.
ACM Digital Library
以上显示的是最相近的搜索结果。 查看全部搜索结果