Chain-Free String Constraints (Technical Report)

TL;DR

This paper introduces a new decidable fragment of string constraints called weakly chaining string constraints, expanding the boundaries of decidability and providing a prototype implementation with competitive experimental results.

Contribution

It defines a novel decidable fragment of string constraints that generalizes existing fragments and integrates it into an existing framework with promising experimental outcomes.

Findings

Decidability of the weakly chaining string constraints fragment.

Prototype implementation demonstrates competitiveness.

Framework achieves accurate results in experiments.

Abstract

We address the satisfiability problem for string constraints that combine relational constraints represented by transducers, word equations, and string length constraints. This problem is undecidable in general. Therefore, we propose a new decidable fragment of string constraints, called weakly chaining string constraints, for which we show that the satisfiability problem is decidable. This fragment pushes the borders of decidability of string constraints by generalising the existing straight-line as well as the acyclic fragment of the string logic. We have developed a prototype implementation of our new decision procedure, and integrated it into in an existing framework that uses CEGAR with under-approximation of string constraints based on flattening. Our experimental results show the competitiveness and accuracy of the new framework.