Formal verification of programs has long been used to provide rigorous correctness guarantees on program behavior. However, the scalability of these techniques is limited, as they require appropriate encoding for various program constructs—encodings that are often unavailable in practice, or may grow in complexity, making them difficult to solve using these techniques.

On the other hand, coverage-guided fuzzing (CGF) is a random testing technique that uses program coverage to select and prioritize inputs. While it can scale to more complex programs—as it does not require any state encoding—this very characteristic makes it fall short in providing correctness guarantees, as it is, by definition, an incomplete approach.

In this paper, we propose improving automated program verification for Java programs using program fuzzing to find counterexamples. More precisely, we adapt a coverage-guided fuzzing tool to be used on verification tasks from the top software verification competition (SV-COMP). Our results show the advantages of using fuzzing in verification, either due to the difficulty or absence of appropriate verification summarization for certain program functions, or when path/state explosion becomes a bottleneck.