Write a Blog >>
Tue 20 Jun 2017 16:35 - 17:00 at Aula Master - Verified Computation Chair(s): Alvin Cheung

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

16:10 - 17:00: PLDI Research Papers - Verified Computation at Aula Master
Chair(s): Alvin CheungUniversity of Washington
pldi-2017-papers149796780000016:10 - 16:35
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
pldi-2017-papers149796930000016:35 - 17:00
Parosh Aziz AbdullaUppsala University, Sweden, Mohamed Faouzi AtigUppsala University, Phi-Diep BuiUppsala University, Yu-Fang Chen, Lukas Holik, Ahmed Rezine, Philipp RuemmerUppsala University
Media Attached