Publication result detail

Negated String Containment is Decidable

HAVLENA, V.; HEČKO, M.; HOLÍK, L.; LENGÁL, O.

Original Title

Negated String Containment is Decidable

English Title

Negated String Containment is Decidable

Type

Paper in proceedings outside WoS and Scopus

Original 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.

English 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.

Keywords

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

Key words in English

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

Authors

HAVLENA, V.; HEČKO, M.; HOLÍK, L.; LENGÁL, O.

Released

20.08.2025

Publisher

Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik

Location

Dagstuhl

Book

50th International Symposium on Mathematical Foundations of Computer Science

ISBN

1868-8969

Periodical

Leibniz International Proceedings in Informatics, LIPIcs

Number

345

State

unknown

Pages from

1

Pages to

20

Pages count

20

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",
  number="345",
  pages="1--20",
  publisher="Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik",
  address="Dagstuhl",
  doi="10.4230/LIPIcs.MFCS.2025.56",
  issn="1868-8969"
}