6 papers
Synthesis and Verification of Transformer Programs (Technical Report)
Hongjian Jiang, Matthew Hague, Philipp Rümmer +1
C-RASP is a simple programming language that was recently shown to capture concepts expressible by transformers. In this paper, we develop new algorithmic techniques for automatica…
Decision Procedure for A Theory of String Sequences
Denghang Hu, Taolue Chen, Philipp Rümmer +2
The theory of sequences, supported by many SMT solvers, can model program data types including bounded arrays and lists. Sequences are parameterized by the element data type and pr…
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…
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…
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…
Probabilistic Bisimulation for Parameterized Anonymity and Uniformity Verification
Chih-Duo Hong, Anthony W. Lin, Philipp Rümmer +1
Bisimulation is crucial for verifying process equivalence in probabilistic systems. This paper presents a novel logical framework for analyzing bisimulation in probabilistic parame…