HornStr: Invariant Synthesis for Regular Model Checking as Constrained Horn Clauses

This archive is provided as artifact material for the article "HornStr: A string Theory Solver for Constrained Horn Clauses" for CAV2025. Abstract: We present HornStr, the first solver for invariant synthesis for Regular Model Checking (RMC) with the specication provided in the SMT-LIB 2.6 theory of strings. It is well-known that invariant synthesis for RMC subsumes various important verication problems, including safety verication for parameterized systems. To achieve a simple and standardized le format, we treat the invariant synthesis problem as a problem of solving Constrained Horn Clauses (CHCs) over strings. Two strategies for synthesizing invariants in terms of regular constraints are supported: (1) L* automata learning, and (2) SAT-based automata learning. HornStr implements these strategies with the help of existing SMT solvers for strings, which are interfaced through SMT-LIB. HornStr provides an easy-to-use interface for string solver developers to apply their techniques to verication and at the same time verication researchers to painlessly tap into the wealth of modern string solving techniques. To assess the eectiveness of HornStr, we conducted a comprehensive evaluation using benchmarks derived from applications including parameterized verication and string rewriting tasks. Our experiments highlight HornStr's capacity to eectively handle these benchmarks, e.g., as the rst solver to verify the challenging MU puzzle automatically. Finally, HornStr can be used to automatically generate a new class of interesting SMT-LIB 2.6 string constraint benchmarks, which might in the future be used in the SMT-COMP strings track. In particular, our experiments on the above invariant synthesis benchmarks produce more than 10000 new QF_S constraints. We also detail the performance of various integrated string solvers, providing insights into their eectiveness on our new benchmarks.