Publication Details

Negated String Containment is Decidable

HAVLENA Vojtěch, HEčKO Michal, HOLíK Lukáš and LENGáL Ondřej. Negated String Containment is Decidable. In: 50th International Symposium on Mathematical Foundations of Computer Science. Dagstuhl: Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 2025. ISSN 1868-8969.
Czech title
Negované obsažení řetězce je rozhodnutelné
Type
conference paper
Language
english
Authors
Havlena Vojtěch, Ing., Ph.D. (DITS FIT BUT)
Hečko Michal, Ing. (DITS FIT BUT)
Holík Lukáš, doc. Mgr., Ph.D. (DITS FIT BUT)
Lengál Ondřej, Ing., Ph.D. (DITS FIT BUT)
Keywords

not contains,regular languages,string constraints,combinatorics on words

Abstract

We provide a positive answer to a long-standing open question of the decidability of the not-contains string predicate. Not-contains is practically relevant, for instance in symbolic execution of string manipulating programs. Particularly, we show that the predicate Contains(x1...xn,y1...ym), where x1...xn and y1...ym are sequences of string variables constrained by regular languages, is decidable. Decidability of a not-contains predicate combined with chain-free word equations and regular membership constraints follows.

Published
2025 (in print)
Journal
Leibniz International Proceedings in Informatics (LIPIcs), ISSN 1868-8969
Proceedings
50th International Symposium on Mathematical Foundations of Computer Science
Conference
Mathematical Foundations of Computer Science 2025, Varšava, PL
Publisher
Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik
Place
Dagstuhl, DE
BibTeX 
@INPROCEEDINGS{FITPUB13548,
   author = "Vojt\v{e}ch Havlena and Michal He\v{c}ko and Luk\'{a}\v{s} Hol\'{i}k and Ond\v{r}ej Leng\'{a}l",
   title = "Negated String Containment is Decidable",
   booktitle = "50th International Symposium on  Mathematical Foundations of Computer Science",
   journal = "Leibniz International Proceedings in Informatics (LIPIcs)",
   year = 2025,
   location = "Dagstuhl, DE",
   publisher = "Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik",
   ISSN = "1868-8969",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/13548"
}
Back to top