Publication Details
Chain-Free String Constraints
Atig Mohamed
Bui Phi Diep
Holík Lukáš, doc. Mgr., Ph.D. (DITS)
Janků Petr, Ing. (RG VERIFIT)
Satisfiability modulo theories, String constraint solving, Program verification
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.
@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"
}