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

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F17%3APU127288" target="_blank" >RIV/00216305:26230/17:PU127288 - isvavai.cz</a>

Výsledek na webu

<a href="https://dl.acm.org/citation.cfm?doid=3062341.3062384" target="_blank" >https://dl.acm.org/citation.cfm?doid=3062341.3062384</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1145/3062341.3062384" target="_blank" >10.1145/3062341.3062384</a>

Jazyk výsledku

angličtina

Název v původním jazyce

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

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

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

Popis výsledku anglicky

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.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Projekt

Výsledek vznikl pri realizaci vícero projektů. Více informací v záložce Projekty.

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Rok uplatnění

2017

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation

ISBN

978-1-4503-4988-8

ISSN

—

e-ISSN

—

Počet stran výsledku

16

Strana od-do

602-617

Název nakladatele

Association for Computing Machinery

Místo vydání

New York

Místo konání akce

Barcelona

Datum konání akce

18. 6. 2017

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

000414334200041