Result Details

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-20.
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)
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(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.

Keywords

not contains,regular languages,string constraints,combinatorics on words

URL
Published
2025
Pages
1–20
Journal
Leibniz International Proceedings in Informatics, ISSN
Conference
Mathematical Foundations of Computer Science 2025
Publisher
Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik
Place
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"
}
Files
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
Research groups
Výzkumná skupina automatizované analýzy a verifikace - VeriFIT (RG VERIFIT)
Departments
Ústav inteligentních systémů (DITS)
Back to top