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…