A Symbolic Algorithm for the Case-Split Rule in String Constraint Solving

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F20%3APU138632" target="_blank" >RIV/00216305:26230/20:PU138632 - isvavai.cz</a>

Výsledek na webu

<a href="https://www.fit.vut.cz/research/publication/12347/" target="_blank" >https://www.fit.vut.cz/research/publication/12347/</a>

DOI - Digital Object Identifier

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

Jazyk výsledku

angličtina

Název v původním jazyce

A Symbolic Algorithm for the Case-Split Rule in String Constraint Solving

Popis výsledku v původním jazyce

Case split is a core proof rule in current decision procedures for the theory of string constraints. Its use is the primary cause of the state space explosion in string constraint solving, since it is the only rule that creates branches in the proof tree. Moreover, explicit handling of the case split rule may cause recomputation of the same tasks in multiple branches of the proof tree. In this paper, we propose a symbolic algorithm that significantly reduces such a redundancy. In particular, we encode a string constraint as a regular language and proof rules as rational transducers. This allows to perform similar steps in the proof tree only once, alleviating the state space explosion. In our preliminary experimental results, we validated that our technique (implemented in a Python prototype) works in many practical cases where other state-of-the-art solvers, such as CVC4 or Z3 fail to provide an answer.

Název v anglickém jazyce

A Symbolic Algorithm for the Case-Split Rule in String Constraint Solving

Popis výsledku anglicky

Case split is a core proof rule in current decision procedures for the theory of string constraints. Its use is the primary cause of the state space explosion in string constraint solving, since it is the only rule that creates branches in the proof tree. Moreover, explicit handling of the case split rule may cause recomputation of the same tasks in multiple branches of the proof tree. In this paper, we propose a symbolic algorithm that significantly reduces such a redundancy. In particular, we encode a string constraint as a regular language and proof rules as rational transducers. This allows to perform similar steps in the proof tree only once, alleviating the state space explosion. In our preliminary experimental results, we validated that our technique (implemented in a Python prototype) works in many practical cases where other state-of-the-art solvers, such as CVC4 or Z3 fail to provide an answer.

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í

2020

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 APLAS'20

ISBN

—

ISSN

0302-9743

e-ISSN

—

Počet stran výsledku

21

Strana od-do

343-363

Název nakladatele

Springer Verlag

Místo vydání

Heidelberg

Místo konání akce

Fukuoka City

Datum konání akce

29. 11. 2020

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

WRD - Celosvětová akce

Kód UT WoS článku

—