Detail publikačního výsledku

Negated String Containment is Decidable

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

Originální název

Negated String Containment is Decidable

Anglický název

Negated String Containment is Decidable

Druh

Stať ve sborníku mimo WoS a Scopus

Originální abstrakt

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.

Anglický abstrakt

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.

Klíčová slova

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

Klíčová slova v angličtině

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

Autoři

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

Vydáno

20.08.2025

Nakladatel

Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik

Místo

Dagstuhl

Kniha

50th International Symposium on Mathematical Foundations of Computer Science

ISSN

1868-8969

Periodikum

Leibniz International Proceedings in Informatics, LIPIcs

Číslo

345

Stát

neuvedeno

Strany od

1

Strany do

20

Strany počet

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"
}

Dokumenty

LIPIcs.MFCS.2025.56