A Symbolic Algorithm for the Case-Split Rule in String Constraint Solving
The result's identifiers
Result code in 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>
Result on the web
<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>
Alternative languages
Result language
angličtina
Original language name
A Symbolic Algorithm for the Case-Split Rule in String Constraint Solving
Original language description
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.
Czech name
—
Czech description
—
Classification
Type
D - Article in proceedings
CEP classification
—
OECD FORD branch
10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
Result continuities
Project
Result was created during the realization of more than one project. More information in the Projects tab.
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)
Others
Publication year
2020
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Article name in the collection
Proceedings of APLAS'20
ISBN
—
ISSN
0302-9743
e-ISSN
—
Number of pages
21
Pages from-to
343-363
Publisher name
Springer Verlag
Place of publication
Heidelberg
Event location
Fukuoka City
Event date
Nov 29, 2020
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
—