Publication result detail

Chain-Free String Constraints

ABDULLA, P.; ATIG, M.; BUI PHI, D.; HOLÍK, L.; JANKŮ, P.

Original Title

Chain-Free String Constraints

English Title

Chain-Free String Constraints

Type

Paper in proceedings (conference paper)

Original Abstract

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.

English abstract

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.

Keywords

Satisfiability modulo theories,
String constraint solving,
Program verification

Key words in English

Satisfiability modulo theories,
String constraint solving,
Program verification

Authors

ABDULLA, P.; ATIG, M.; BUI PHI, D.; HOLÍK, L.; JANKŮ, P.

RIV year

2020

Released

21.10.2019

Publisher

Springer International Publishing

Location

Cham

ISBN

978-3-030-31783-6

Book

Proceedings of ATVA'19

Edition

Lecture Notes in Computer Science

Volume

11781

Pages from

277

Pages to

293

Pages count

16

URL

https://link.springer.com/chapter/10.1007/978-3-030-31784-3_16

BibTex

@inproceedings{BUT161469,
  author="Parosh {Abdulla} and Mohamed {Atig} and Diep {Bui Phi} and Lukáš {Holík} and Petr {Janků}",
  title="Chain-Free String Constraints",
  booktitle="Proceedings of ATVA'19",
  year="2019",
  series="Lecture Notes in Computer Science",
  volume="11781",
  pages="277--293",
  publisher="Springer International Publishing",
  address="Cham",
  doi="10.1007/978-3-030-31784-3\{_}16",
  isbn="978-3-030-31783-6",
  url="https://link.springer.com/chapter/10.1007/978-3-030-31784-3_16"
}

Documents

ChainFreeStringConstraints_clanek
ChainFreeStringConstraints_popis
atva19