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

• Test-input generation
• Fuzzing

Type of tool

Fuzzer

Expected input

• Program
• Safety property

Format:

• Program: C program
• Safety property: ?

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.

Internals

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.