PV3 VeriFuzzchecks whether a user-specified error location in C code can be reached

VeriFuzz is a coverage driven automated test-input generation tool based on grey-box fuzzing

Application domain/field

Type of tool


Expected input


Expected output

It runs until an error location was reached or until the max. time is over. If an error location was found, then it will generate a witness.


VeriFuzz generates new test inputs based on evolutionary algorithms. For each test it will consider whether to add it to the set of test inputs based on the code coverage. This is repeated until a crashing test-input is found that causes the program to reach the error location (indicated with __VERIFIER_error()) or when the time budget has elapsed. It uses CBMC for the initial input generation. Built on top of afl-fuzz.

Related papers

VeriFuzz: Program Aware Fuzzing (TACAS '19)

Last publication date

4 April 2019

ProVerB specific

ProVerB is a part of SLEBoK. Last updated: February 2023.