Testing in Formal Verification via Witness Generation (Empirical Evaluation)

Abstract The communities surrounding formal software verifiers and automatic test generators have developed different formats to describe a path to an error. Test generators export a test case whose execution makes the error observable, while verifiers produce a violation witness, an abstract description of the error path. To leverage potential synergies between both communities, transformations between these formats are necessary. Previous work transformed violation witnesses to test cases, and improved test generation with formal verification techniques. But the other direction is not considered so far: Test cases are not yet transformed to violation witnesses, and there is no empirical evaluation for the application of test generators in formal verification. We change both. We present a transformation that allows the use of test generators in verification scenarios like the Competition on Software Verification (SV-COMP), both directly and as parts of bigger verification systems. In a large empirical evaluation we examine the improvements this can add to formal verifiers.