CoVeriTest: interleaving value and predicate analysis for test-case generation

Verification techniques are well-suited for automatic test-case generation. They basically need to check the reachability of every test goal and generate test cases for all reachable goals. This is also the basic idea of ourCoVeriTest submission. However, the set of test goals is not fixed inCoVeriTest , instead we can configure the set of test goals. For Test-Comp'19, we support the set of all __VERIFIER_error() calls as well as the set of all branches. Thus, we can deal with the two test specifications considered in Test-Comp'19. Since the tasks in Test-Comp are diverse and verification techniques have different strengths and weaknesses, we also do not stick to a single verification technique, but use a hybrid approach that combines multiple techniques. More concrete,CoVeriTest interleaves different verification techniques and allows to configure the cooperation (i.e., information exchange and time limits). To choose from a large set of verification techniques,CoVeriTest is integrated into the analysis frameworkCPAchecker. For the competition, we interleaveCPAchecker's value and predicate analysis and let both analyses resume their analysis performed in the previous iteration.