Result Details
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.
Type
conference paper
Language
English
Authors
Havlena Vojtěch, Ing., Ph.D., DITS (FIT)
Hečko Michal, Ing., DITS (FIT)
Holík Lukáš, doc. Mgr., Ph.D., DITS (FIT)
Lengál Ondřej, doc. Ing., Ph.D., DITS (FIT)
Hečko Michal, Ing., DITS (FIT)
Holík Lukáš, doc. Mgr., Ph.D., DITS (FIT)
Lengál Ondřej, doc. Ing., Ph.D., DITS (FIT)
Abstract
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.
Keywords
not contains,regular languages,string constraints,combinatorics on words
Published
2025
Pages
1–20
Journal
Leibniz International Proceedings in Informatics, LIPIcs, no. 345, ISSN 1868-8969
Proceedings
50th International Symposium on Mathematical Foundations of Computer Science
Conference
Mathematical Foundations of Computer Science 2025
Publisher
Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik
Place
Dagstuhl
DOI
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"
}
Projects
Efficient Finite Automata for Automated Reasoning, MŠMT, ERC CZ, LL1908, start: 2020-01-01, end: 2024-12-31, completed
QUAK: Quantum Program Analysis using Automata Toolkit, GACR, Standardní projekty, 25-18318S, start: 2025-01-01, end: 2027-12-31, running
Reliable, Secure, and Intelligent Computer Systems, BUT, Vnitřní projekty VUT, FIT-S-23-8151, start: 2023-03-01, end: 2026-02-28, running
QUAK: Quantum Program Analysis using Automata Toolkit, GACR, Standardní projekty, 25-18318S, start: 2025-01-01, end: 2027-12-31, running
Reliable, Secure, and Intelligent Computer Systems, BUT, Vnitřní projekty VUT, FIT-S-23-8151, start: 2023-03-01, end: 2026-02-28, running
Research groups
Departments