HornStr: Invariant Synthesis for Regular Model Checking as Constrained Horn Clauses(Technical Report)
Hongjian Jiang, Anthony W. Lin, Oliver Markgraf, Philipp Rümmer, Daniel Stan
TL;DR
The paper addresses invariant synthesis for Regular Model Checking within the SMT-LIB 2.6 theory of strings by formulating RMC problems as Constrained Horn Clauses over strings. It introduces HornStr, the first CHC-based invariant-synthesis solver for RMC, which implements two learning strategies—L* automata learning and SAT-based automata learning—using string solver backends via SMT-LIB and supports incremental solving. The evaluation on benchmarks from parameterized verification and string rewriting (notably the MU puzzle) demonstrates HornStr’s ability to automatically verify challenging cases and to generate a large new class of SMT-LIB 2.6 string benchmarks (over 30,000 QF_S constraints). The work also discusses future extensions to broader CHC classes over strings and additional RMC verification tasks, and provides a flexible framework that can benefit string-solver developers and verification researchers alike.
Abstract
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 that invariant synthesis for RMC subsumes various important verification problems, including safety verification for parameterized systems. To achieve a simple and standardized file 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 verification. At the same time, it allows verification researchers to painlessly tap into the wealth of modern string solving techniques. To assess the effectiveness of HornStr, we conducted a comprehensive evaluation using benchmarks derived from applications including parameterized verification and string rewriting tasks. Our experiments highlight HornStr's capacity to effectively handle these benchmarks, e.g., as the first 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 30000 new QF_S constraints. We also detail the performance of various integrated string solvers, providing insights into their effectiveness on our new benchmarks.