Negated String Containment is Decidable (Technical Report)

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 Contains(x_1\dots x_n,y_1\dots y_m)$, where $x_1\dots x_n$ and $y_1\dots 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.