Přístupnostní navigace
E-přihláška
Vyhledávání Vyhledat Zavřít
Detail publikace
ABDULLA, P. ATIG, M. BUI PHI, D. HOLÍK, L. JANKŮ, P.
Originální název
Chain-Free String Constraints
Typ
článek ve sborníku ve WoS nebo Scopus
Jazyk
angličtina
Originální abstrakt
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.
Klíčová slova
Satisfiability modulo theories, String constraint solving, Program verification
Autoři
ABDULLA, P.; ATIG, M.; BUI PHI, D.; HOLÍK, L.; JANKŮ, P.
Vydáno
21. 10. 2019
Nakladatel
Springer International Publishing
Místo
Cham
ISBN
978-3-030-31783-6
Kniha
Proceedings of ATVA'19
Edice
Lecture Notes in Computer Science
Strany od
277
Strany do
293
Strany počet
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" }