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

TL;DR

HornStr introduces a novel solver for invariant synthesis in Regular Model Checking using string-based Constrained Horn Clauses, enabling automated verification of complex systems and generating new benchmarks for SMT solvers.

Contribution

It is the first to unify invariant synthesis for RMC with string constraints via CHCs, supporting multiple automata learning strategies and integrating with existing SMT solvers.

Findings

Successfully verified the MU puzzle automatically.

Generated over 30,000 new string constraints for benchmarks.

Demonstrated effectiveness on parameterized verification and rewriting tasks.

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.