PV3 ⊧ VeriFuzzchecks whether a user-specified error location in C code can be reachedVeriFuzz is a coverage driven automated test-input generation tool based on grey-box fuzzing
- Test-input generation
Type of toolFuzzer
- Safety property
- Program: C program
- Safety property: ?
Expected outputIt 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.
InternalsVeriFuzz 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.