Negated String Containment is Decidable (Technical Report)

TL;DR

This paper proves that the not-contains string predicate, which checks if one string does not contain another, is decidable when strings are constrained by regular languages, impacting symbolic execution and string analysis.

Contribution

It establishes the decidability of the not-contains predicate for string sequences constrained by regular languages, resolving a long-standing open problem.

Findings

Decidability of not-contains predicate proven

Enables analysis of string constraints in symbolic execution

Combines with chain-free word equations and regular constraints

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 $\neg\mathit{Contains}(x_1 \ldots x_n, y_1 \ldots y_m)$, where $x_1 \ldots x_n$ and $y_1 \ldots 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.