Publication detail

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

HAVLENA, V. LENGÁL, O. CHEN, Y. TURRINI, A.

Original Title

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

English Title

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

Type

conference paper

Language

en

Original 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.

English 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.

Keywords

string solving regular model checking Nielsen transformation symbolic encoding

Released

29.11.2020

Publisher

Springer Verlag

Location

Heidelberg

ISBN

0302-9743

Periodical

Lecture Notes in Computer Science

Year of study

NEUVEDEN

Number

12470

State

DE

Pages from

343

Pages to

363

Pages count

21

URL

Documents

BibTex


@inproceedings{BUT168141,
  author="Vojtěch {Havlena} and Ondřej {Lengál} and Yu-Fang {Chen}",
  title="A Symbolic Algorithm for the Case-Split Rule in String Constraint Solving",
  annote="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.",
  address="Springer Verlag",
  booktitle="Proceedings of APLAS'20",
  chapter="168141",
  doi="10.1007/978-3-030-64437-6_18",
  edition="NEUVEDEN",
  howpublished="print",
  institution="Springer Verlag",
  number="12470",
  year="2020",
  month="november",
  pages="343--363",
  publisher="Springer Verlag",
  type="conference paper"
}