2026-07-23T03:52:06Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:24163 2025-11-12T13:33:54Z ddc:004 open_access

Negated String Containment Is Decidable Havlena, Vojtěch Hečko, Michal Holík, Lukáš Lengál, Ondřej not-contains string constraints word combinatorics primitive word 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Vojtěch Havlena and Michal Hečko and Lukáš Holík and Ondřej Lengál 2025 Is Part Of LIPIcs, Volume 345, 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.MFCS.2025.56 urn:nbn:de:0030-drops-241631 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2025.56 eng https://creativecommons.org/licenses/by/4.0/legalcode