Detail výsledku

Negated String Containment is Decidable

HAVLENA, V.; HEČKO, M.; HOLÍK, L.; LENGÁL, O. Negated String Containment is Decidable. 50th International Symposium on Mathematical Foundations of Computer Science. Leibniz International Proceedings in Informatics, LIPIcs. Dagstuhl: Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 2025. no. 345, p. 1-20. ISSN: 1868-8969.
Typ
článek ve sborníku konference
Jazyk
anglicky
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(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

Rok
2025
Strany
1–20
Časopis
Leibniz International Proceedings in Informatics, LIPIcs, č. 345, ISSN 1868-8969
Sborník
50th International Symposium on Mathematical Foundations of Computer Science
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",
  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"
}
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, 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, řešení
Výzkumné skupiny
Výzkumná skupina automatizované analýzy a verifikace - VeriFIT (VZ VERIFIT)
Pracoviště
Ústav inteligentních systémů (UITS)
Nahoru