Negated String Containment is Decidable (Technical Report)

2025/06/27 by Vojtěch Havlena, Havlena, Vojtěch, Michal Hečko +5
Computer Science · #FOS: Computer and information sciences #Formal Languages and Automata Theory (cs.FL) #Logic in Computer Science (cs.LO) #Software Testing and Debugging Techniques #Web Application Security Vulnerabilities #semigroups and automata theory

paper · pdf · doi:10.48550/arxiv.2506.22061

openalex publication_date 2025/06/27 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

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 \negContains(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.

Citations

• A Uniform Framework for Handling Position Constraints in String Solving (Technical Report)
• Layered and Staged Monte Carlo Tree Search for SMT Strategy Synthesis
• Solving String Constraints With Regex-Dependent Functions Through Transducers With Priorities And Variables
• An SMT Solver for Regular Expressions and Linear Arithmetic over String\n Length
• A Decision Procedure for Path Feasibility of String Manipulating Programs with Integer Data Type
• On Solving Word Equations Using SAT
• Decision Procedures for Path Feasibility of String-Manipulating Programs with Complex Operations
• The Satisfiability of Extended Word Equations: The Boundary Between\n Decidability and Undecidability
• What Is Decidable about String Constraints with the ReplaceAll Function
• String Solving with Word Equations and Transducers: Towards a Logic for\n Analysing Mutation XSS (Full Version)
• Monadic Decomposition
• Algorithmic Verification of Single-Pass List Processing Programs

Related

• (Un)Decidability Results for Word Equations with Length and Regular Expression Constraints
• Chain-Free String Constraints (Technical Report)
• Decidable Logics Combining Word Equations, Regular Expressions and Length Constraints
• What Is Decidable about String Constraints with the ReplaceAll Function
• Satisfiability of Context-free String Constraints with Subword-ordering and Transducers