HornFuzz: Fuzzing CHC solvers

Many advanced program analysis and verification methods are based on solving systems of Constrained Horn Clauses (CHC). Testing CHC solvers is very important, as correctness of their work determines whether bugs in the analyzed programs are detected or missed. One of the well-established and efficient methods of automated software testing is fuzzing: analyzing the reactions of programs to random input data. Currently, there are no fuzzers for CHC solvers, and fuzzers for SMT solvers are not efficient in CHC solver testing, since they do not consider CHC specifics. In this paper, we present HornFuzz, a mutation-based gray-box fuzzing technique for detecting bugs in CHC solvers based on the idea of metamorphic testing. We evaluated our fuzzer on one of the highest performing CHC solvers, Spacer, and found a handful of bugs in Spacer. In particular, some discovered problems are so serious that they require fixes with significant changes to the solver.