Publication Details

Negated String Containment is Decidable

HAVLENA, V.; HEČKO, M.; HOLÍK, L.; LENGÁL, O. Negated String Containment is Decidable. 50th International Symposium on Mathematical Foundations of Computer Science. Leibniz International Proceedings in Informatics, LIPIcs. 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)
Hečko Michal, Ing. (DITS)
Holík Lukáš, doc. Mgr., Ph.D. (DITS)
Lengál Ondřej, Ing., Ph.D. (DITS)
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
BibTeX 
@inproceedings{BUT198408,
  author="Vojtěch {Havlena} and Michal {Hečko} and Lukáš {Holík} and Ondřej {Lengál}",
  title="Negated String Containment is Decidable",
  booktitle="50th International Symposium on  Mathematical Foundations of Computer Science",
  year="2025",
  journal="Leibniz International Proceedings in Informatics, LIPIcs",
  publisher="Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik",
  address="Dagstuhl",
  issn="1868-8969"
}
Back to top