  We describe and evaluate a novel white-box fuzzer for C programs named
FuSeBMC, which combines fuzzing and symbolic execution, and applies Bounded
Model Checking (BMC) to find security vulnerabilities in C programs. FuSeBMC
explores and analyzes C programs (1) to find execution paths that lead to
property violations and (2) to incrementally inject labels to guide the fuzzer
and the BMC engine to produce test-cases for code coverage. FuSeBMC
successfully participates in Test-Comp'21 and achieves first place in the
Cover-Error category and second place in the Overall category.
