activity
20212025
most citedLearning Union of Integer Hypercubes with Queries (Technical Report)

1 citations · 3 across the 5 of their papers we have counts for

collaborators

5 papers

cs.LO2025★ 1 cited

The Power of Regular Constraint Propagation (Technical Report)

Matthew Hague, Artur Jeż, Anthony W. Lin +2

The past decade has witnessed substantial developments in string solving. Motivated by the complexity of string solving strategies adopted in existing string solvers, we investigat…

cs.LO2025★ 1 cited

OSTRICH2: Solver for Complex String Constraints

Matthew Hague, Denghang Hu, Artur Jeż +4

We present OSTRICH2, the latest evolution of the SMT solver OSTRICH for string constraints. OSTRICH2 supports a wide range of complex functions on strings and provides completeness…

cs.LO2025

HornStr: Invariant Synthesis for Regular Model Checking as Constrained Horn Clauses(Technical Report)

Hongjian Jiang, Anthony W. Lin, Oliver Markgraf +2

We present HornStr, the first solver for invariant synthesis for Regular Model Checking (RMC) with the specification provided in the SMT-LIB 2.6 theory of strings. It is well-known…

cs.LO2023

Decision Procedures for Sequence Theories (Technical Report)

Artur Jeż, Anthony W. Lin, Oliver Markgraf +1

Sequence theories are an extension of theories of strings with an infinite alphabet of letters, together with a corresponding alphabet theory (e.g. linear integer arithmetic). Sequ…

cs.LG2021★ 1 cited

Learning Union of Integer Hypercubes with Queries (Technical Report)

Oliver Markgraf, Daniel Stan, Anthony W. Lin

We study the problem of learning a finite union of integer (axis-aligned) hypercubes over the d-dimensional integer lattice, i.e., whose edges are parallel to the coordinate axes.…