Publication Details

Chain-Free String Constraints

ABDULLA Parosh A., ATIG Mohamed F., BUI Phi Diep, HOLÍK Lukáš and JANKŮ Petr. Chain-Free String Constraints. In: Proceedings of ATVA'19. Lecture Notes in Computer Science, vol. 11781. Cham: Springer International Publishing, 2019, pp. 277-293. ISBN 978-3-030-31783-6. Available from: https://link.springer.com/chapter/10.1007/978-3-030-31784-3_16
Czech title
Řetězová omezení bez cyklů
Type
conference paper
Language
english
Authors
Abdulla Parosh A. (Uppsala)
Atig Mohamed F. (Uppsala)
Bui Phi Diep (Uppsala)
Holík Lukáš, doc. Mgr., Ph.D. (DITS FIT BUT)
Janků Petr, Ing. (DITS FIT BUT)
URL
Keywords

Satisfiability modulo theories,
String constraint solving,
Program verification

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.

Published
2019
Pages
277-293
Proceedings
Proceedings of ATVA'19
Series
Lecture Notes in Computer Science
Volume
11781
Conference
17th International Symposium on Automated Technology for Verification and Analysis, Taipei, TW
ISBN
978-3-030-31783-6
Publisher
Springer International Publishing
Place
Cham, CH
DOI
UT WoS
000723515700016
EID Scopus
BibTeX
@INPROCEEDINGS{FITPUB12134,
   author = "A. Parosh Abdulla and F. Mohamed Atig and Diep Phi Bui and Luk\'{a}\v{s} Hol\'{i}k and Petr Jank\r{u}",
   title = "Chain-Free String Constraints",
   pages = "277--293",
   booktitle = "Proceedings of ATVA'19",
   series = "Lecture Notes in Computer Science",
   volume = 11781,
   year = 2019,
   location = "Cham, CH",
   publisher = "Springer International Publishing",
   ISBN = "978-3-030-31783-6",
   doi = "10.1007/978-3-030-31784-3\_16",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/12134"
}
Back to top