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(x₁ … x_n, y₁ … y_m), where x₁ … x_n and y₁ … y_m 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(x₁ … x_n, y₁ … y_m), where x₁ … x_n and y₁ … y_m 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.

Rok RIV

2026

Vydáno

20.08.2025

Nakladatel

Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik

Místo

Dagstuhl

Periodikum

Leibniz International Proceedings in Informatics

Stát

Spolková republika Německo

Strany od

1

Strany do

20

Strany počet

20

URL

https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2025.56

Plný text v Digitální knihovně

http://hdl.handle.net/11012/255730

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",
  year="2025",
  journal="Leibniz International Proceedings in Informatics",
  pages="1--20",
  publisher="Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik",
  address="Dagstuhl",
  doi="10.4230/LIPIcs.MFCS.2025.56",
  url="https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2025.56"
}