Verification-Based Test Case Generation for Full Feasible Branch Coverage

摘要

The goal of this work is to improve the testing of programs that contain loops and complex methods. We achieve this goal with verification-based testing, which is a technique that can generate test cases not only from source code but also from loop invariants and method specifications provided by the user. These test cases ensure the execution of interesting program  paths that are likely to be missed by existing testing techniques that are  based on symbolic program execution. These techniques would require an  exhaustive inspection of all execution paths, which is hard to achieve in  presence of complex methods and impossible if loops are involved.  Verification-based testing takes a different approach.