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.