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.

翻译：许多高级程序分析和验证方法基于求解约束霍恩子句（CHC）系统。测试CHC求解器至关重要，因为其正确性决定了分析程序中的缺陷是否会被检测到或遗漏。自动化软件测试领域一种成熟且高效的方法是模糊测试：分析程序对随机输入数据的反应。目前，尚无针对CHC求解器的模糊测试工具，而针对SMT求解器的模糊测试工具在CHC求解器测试中效率低下，因为它们未考虑CHC的特殊性。本文提出HornFuzz——一种基于变异的灰盒模糊测试技术，用于检测CHC求解器中的缺陷，其核心思想源于蜕变测试。我们在性能最高的CHC求解器之一Spacer上评估了该模糊测试工具，并发现Spacer中存在多个缺陷。特别地，某些发现的问题极为严重，需要通过对求解器进行重大改动来修复。