Horn2VMT: Translating Horn Reachability into Transition Systems

Relational transition system models have for decades been the bread and butter representation of hardware and software model checking. The VMT format1 provides a means of describing sequential model checking problems using SMT-LIB-compatible combinational formulas. MathSAT [4], EUForia [3], and other tools support VMT natively, but unfortunately they do not support Horn clause formats. While it is well known that linear Horn clauses can be expressed as transition systems, we are not aware of a precise description in the literature. This paper contributes a procedure, proof of correctness, and prototype implementation for translating linear Horn clauses into VMT. Our procedure is able to convert SV-COMP 2 and SeaHorn [6] benchmarks into VMT for use with various model checkers. Our prototype implementation will be available at https://github.com/dbueno/horn2vmt.