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

Displayed 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
25m
Talk
A Formally Verified Compiler for Lustre
PLDI Research Papers
Timothy Bourke INRIA, Lélio 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
25m
Talk
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