Flatten and Conquer (A Framework for Efficient Analysis of String Constraints)
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 {\it 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.
Tue 20 JunDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
16:10 - 17:00 | Verified ComputationPLDI Research Papers at Aula Master Chair(s): Alvin Cheung University of Washington | ||
16:10 25mTalk | A Formally Verified Compiler for Lustre PLDI Research Papers Timothy Bourke INRIA, Lelio Brun ENS/Inria, Pierre-Evariste Dagand LIP6/CNRS , Xavier Leroy Inria, Marc Pouzet École normale supérieure, Lionel Rieg Collège de France Media Attached | ||
16:35 25mTalk | Flatten and Conquer (A Framework for Efficient Analysis of String Constraints) PLDI Research Papers Parosh Aziz Abdulla Uppsala University, Sweden, Mohamed Faouzi Atig Uppsala University, Bui Phi Diep Uppsala University, Yu-Fang Chen , Lukáš Holík , Ahmed Rezine , Philipp Ruemmer Uppsala University Media Attached |