Chain-Free String Constraints

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F19%3APU134969" target="_blank" >RIV/00216305:26230/19:PU134969 - isvavai.cz</a>

Výsledek na webu

<a href="https://link.springer.com/chapter/10.1007/978-3-030-31784-3_16" target="_blank" >https://link.springer.com/chapter/10.1007/978-3-030-31784-3_16</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-030-31784-3_16" target="_blank" >10.1007/978-3-030-31784-3_16</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Chain-Free String Constraints

Popis výsledku v původním jazyce

We address the satisfiability problem for string constraints that combine relational constraints represented by transducers, word equations, and string length constraints. This problem is undecidable in general. Therefore, we propose a new decidable fragment of string constraints, called weakly chaining string constraints, for which we show that the satisfiability problem is decidable. This fragment pushes the borders of decidability of string constraints by generalising the existing straight-line as well as the acyclic fragment of the string logic. We have developed a prototype implementation of our new decision procedure, and integrated it into an existing framework that uses CEGAR with under-approximation of string constraints based on flattening. This has led to an improvement of the running times as well as accuracy of the framework. We have demonstrated the competitiveness of the entire framework on benchmarks from the literature.

Název v anglickém jazyce

Chain-Free String Constraints

Popis výsledku anglicky

We address the satisfiability problem for string constraints that combine relational constraints represented by transducers, word equations, and string length constraints. This problem is undecidable in general. Therefore, we propose a new decidable fragment of string constraints, called weakly chaining string constraints, for which we show that the satisfiability problem is decidable. This fragment pushes the borders of decidability of string constraints by generalising the existing straight-line as well as the acyclic fragment of the string logic. We have developed a prototype implementation of our new decision procedure, and integrated it into an existing framework that uses CEGAR with under-approximation of string constraints based on flattening. This has led to an improvement of the running times as well as accuracy of the framework. We have demonstrated the competitiveness of the entire framework on benchmarks from the literature.

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í

2019

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 ATVA'19

ISBN

978-3-030-31783-6

ISSN

—

e-ISSN

—

Počet stran výsledku

16

Strana od-do

277-293

Název nakladatele

Springer International Publishing

Místo vydání

Cham

Místo konání akce

Taipei

Datum konání akce

27. 10. 2019

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

WRD - Celosvětová akce

Kód UT WoS článku

000723515700016