Taming Cyclic Dependencies in Stabilization-Based String Constraint Solving

Siyi Wu; Bican Xia

Home/Archive/arXiv

arXiv · 2610.25197

Taming Cyclic Dependencies in Stabilization-Based String Constraint Solving

Siyi Wu·Bican Xia

View original source ↗Read source document ↗Export metadata ↓

Abstract

Word equations with cyclic variable dependencies pose a challenge to SMT string solvers. In stabilization-based procedures, such dependencies can trigger repeated refinement of regular-language assignments without reaching stability. We present Z3-Noodler-C, an extension of Z3-Noodler, combining equality-aware stabilization with dedicated loop reasoning. We introduce equality predicates to retain relevant equations as single stability obligations, and extend stabilization with equality-aware substitution and adapted concatenation-eliminating refinement to expose cyclic dependencies as overlapping variable bindings. Dedicated loop reasoning rules then exploit the periodic structure of these bindings, avoiding certain infinite derivations. We evaluate Z3-Noodler-C against Z3-Noodler, cvc5 and OSTRICH2. On 64 systematically generated, syntactically simple instances involving cyclic dependencies and regular constraints, our solver solves all instances, compared with only 20 solved for the best baseline. On equation-oriented instances from SMT-LIB'25, Z3-Noodler-C achieves the highest coverage, solving 20 more instances than Z3-Noodler while maintaining competitive aggregate CPU time.

Explore related subjects

cs.LO

Keep this discovery

Explore connections, maps & timelines

BibTeX RIS

Siyi Wu, Bican Xia. 2026-10-18. Taming Cyclic Dependencies in Stabilization-Based String Constraint Solving. https://arxiv.org/abs/2610.25197

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

Constructive Ordinal Exponentiation

In classical mathematics, ordinal arithmetic is well-studied; constructively, addition and multiplication are well-known. We study constructive ordinal exponentiation, where ordinals are taken to be transitive, extensional, and wellfounded orders on sets. We present a negative result showing that general constructive ordinal exponentiation is impossible, but we suggest two definitions that come close. The first definition is abstract and solely motivated by the expected equations; this works as long as the base of the exponential is positive. The second definition is based on decreasing lists and can be seen as a constructive version of Sierpi{ń}ski's definition via functions with finite support; this requires the base to have a trichotomous least element. Whenever it makes sense to ask the question, the two constructions are equivalent, allowing us to prove algebraic laws, cancellation properties, and preservation of decidability of the exponential. The core ideas do not depend on any specific constructive set theory or type theory, but a concrete computer-checked mechanization using the Agda proof assistant is given in homotopy type theory.

cs.LO↗

arXiv2026

TREBL -- A Relative Complete Temporal Event-B Logic. Part I: Theory

The verification of liveness conditions is an important aspect of state-based rigorous methods. This article addresses the extension of the logic of Event-B to a powerful logic, in which properties of traces of an Event-B machine can be expressed. However, all formulae of this logic are still interpreted over states of an Event-B machine rather than traces. The logic exploits that for an Event-B machine $M$ a state $S$ determines all traces of $M$ starting in $S$. We identify a fragment called TREBL of this logic, in which all liveness conditions of interest can be expressed, and define a set of sound derivation rules for the fragment. We further show relative completeness of these derivation rules in the sense that for every valid entailment of a formula $φ$ one can find a derivation, provided the machine $M$ is sufficiently refined. The decisive property is that certain variant terms must be definable in the refined machine. We show that such refinements always exist. Throughout the article several examples from the field of security are used to illustrate the theory.

cs.LO↗

arXiv2026

Forall-Exists Relational Verification by Filtering to Forall-Forall

Relational verification encompasses reasoning about data abstraction, security and privacy, secure compilation, and functional specification of tensor programs, among others. Several relational logics and tools support compositional reasoning about $\forall\forall$ (2-safety) properties and, generally, $k$-safety properties. In contrast, few logics and tools exist for reasoning about $\forall\exists$ properties which are critical in the presence of nondeterminism. This paper's primary contribution is a technique for verifying a $\forall\exists$ judgment by way of a novel transformation. The filter-adequacy transformation adds assertions to a product program in such a way that the desired $\forall\exists$ property (of a pair of underlying unary programs) is implied by a $\forall\forall$ property of the transformed product. The paper develops bicoms, a form of product programs that facilitates expressing good alignments and caters for direct translation of $\forall\forall$ properties to unary correctness; proves that successful $\forall\forall$ verification of a transformed bicom implies the $\forall\exists$ spec for its underlying unary commands; and evaluates the technique using a prototype auto-active relational verifier. The technique enables users to work with ordinary assertions and assumptions, and a standard assertion language, so that existing $\forall\forall$ and unary verification tools can be used for $\forall\exists$.

cs.LO↗