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 Jun Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
16:10 - 17:00: Verified ComputationPLDI Research Papers at Aula Master Chair(s): Alvin CheungUniversity of Washington | |||
16:10 - 16:35 Talk | A Formally Verified Compiler for Lustre PLDI Research Papers Timothy BourkeINRIA, Lélio BrunENS/Inria, Pierre-Evariste DagandLIP6/CNRS , Xavier LeroyInria, Marc PouzetÉcole normale supérieure, Lionel RiegCollège de France Media Attached | ||
16:35 - 17:00 Talk | Flatten and Conquer (A Framework for Efficient Analysis of String Constraints) PLDI Research Papers Parosh Aziz AbdullaUppsala University, Sweden, Mohamed Faouzi AtigUppsala University, Bui Phi DiepUppsala University, Yu-Fang Chen, Lukáš Holík, Ahmed Rezine, Philipp RuemmerUppsala University Media Attached |