Publication Details

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

HAVLENA, V.; LENGÁL, O.; CHEN, Y.; TURRINI, A. A Symbolic Algorithm for the Case-Split Rule in String Constraint Solving. In Proceedings of APLAS'20. Lecture Notes in Computer Science. Heidelberg: Springer Verlag, 2020. p. 343-363. ISSN: 0302-9743.
Czech title
Symbolický algoritmus pro pravidlo "Case-Split" při řešení omezení nad řetězci
Type
conference paper
Language
English
Authors
Havlena Vojtěch, Ing., Ph.D. (DITS)
Lengál Ondřej, Ing., Ph.D. (DITS)
Chen Yu-Fang
TURRINI, A.
Keywords

string solving regular model checking Nielsen transformation symbolic encoding

Abstract

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.

Published
2020
Pages
343–363
Journal
Lecture Notes in Computer Science, no. 12470, ISSN 0302-9743
Proceedings
Proceedings of APLAS'20
Publisher
Springer Verlag
Place
Heidelberg
DOI
UT WoS
000916297300018
EID Scopus
BibTeX
@inproceedings{BUT168141,
  author="HAVLENA, V. and LENGÁL, O. and CHEN, Y. and TURRINI, A.",
  title="A Symbolic Algorithm for the Case-Split Rule in String Constraint Solving",
  booktitle="Proceedings of APLAS'20",
  year="2020",
  journal="Lecture Notes in Computer Science",
  number="12470",
  pages="343--363",
  publisher="Springer Verlag",
  address="Heidelberg",
  doi="10.1007/978-3-030-64437-6\{_}18",
  issn="0302-9743",
  url="https://www.fit.vut.cz/research/publication/12347/"
}
Back to top