
Registered user since Mon 27 Mar 2023
Contributions
2023
View general profile
Registered user since Mon 27 Mar 2023
Contributions
Research (Full Papers)
Thu 15 Jun 2023 14:00 - 14:20 at Aurora Hall - Software Testing and Analysis Chair(s): Davide TaibiMany 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.
Link to publication DOI Pre-print File Attached