Detail výsledku

Negated String Containment is Decidable

HAVLENA, V.; HEČKO, M.; HOLÍK, L.; LENGÁL, O. Negated String Containment is Decidable. Leibniz International Proceedings in Informatics. Dagstuhl: Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 2025. p. 1.
Typ
článek ve sborníku konference
Jazyk
angličtina
Autoři
Havlena Vojtěch, Ing., Ph.D., UITS (FIT)
Hečko Michal, Ing., UITS (FIT)
Holík Lukáš, doc. Mgr., Ph.D., UITS (FIT)
Lengál Ondřej, doc. Ing., Ph.D., UITS (FIT)
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

URL
Rok
2025
Strany
1–20
Časopis
Leibniz International Proceedings in Informatics, ISSN
Konference
Mathematical Foundations of Computer Science 2025
Vydavatel
Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik
Místo
Dagstuhl
DOI
10.4230/LIPIcs.MFCS.2025.56
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"
}
Soubory
Projekty
Efektivní konečné automaty pro automatické usuzování, MŠMT, ERC CZ, LL1908, zahájení: 2020-01-01, ukončení: 2024-12-31, ukončen
QUAK: Analýza kvantových programů pomocí automatů, GAČR, Standardní projekty, GA25-18318S, 25-18318S, zahájení: 2025-01-01, ukončení: 2027-12-31, řešení
Reliable, Secure, and Intelligent Computer Systems, VUT, Vnitřní projekty VUT, FIT-S-23-8151, zahájení: 2023-03-01, ukončení: 2026-02-28, ukončen
Výzkumné skupiny
Výzkumná skupina automatizované analýzy a verifikace - VeriFIT (VZ VERIFIT)
Pracoviště
Ústav inteligentních systémů (UITS)
Nahoru