Interrogation Testing of CHC Solvers

A Constrained Horn Clause (CHC) is a specific type of logic formula that contains uninterpreted predicates. CHC formulas are often used by static program analyzers to encode program properties, which are then verified using CHC solvers. The solvers themselves are complex tools and may contain bugs, which can lead to verifying unsafe programs, flagging safe programs as unsafe, or providing analyzers with incorrect invariants and counterexamples. It is, therefore, crucial to develop techniques for systematically testing CHC solvers. In this paper, we present the first interrogation-testing technique for CHC solvers, which we implement in a tool called HornGator. Our technique uses witnesses generated by the solver under test to form new CHC instances. It also integrates a knowledge base maintaining a history of past solver queries. All this information helps HornGator generate more diverse instances, thereby improving its bug-finding effectiveness. As a result, HornGator found 21 unique bugs in five state-of-the-art CHC solvers, all of which are confirmed by the developers, 18 are fixed, and eight are of the highest severity.