CoVeriTest with Dynamic Partitioning of the Iteration Time Limit (Competition Contribution)

Our CoVeriTest submission, which is implemented in the analysis framework CPAchecker, uses verification techniques for automatic test-case generation. To this end, it checks the reachability of every test goal and generates one test case per reachable goal. Instead of checking the reachability of every test goal individually, which is too expensive, CoVeriTest considers all test goals at once and removes already covered goals from future reachability queries. To deal with the diverse set of Test-Comp tasks, CoVeriTest uses a hybrid approach that interleaves value and predicate analysis. In contrast to Test-Comp’19, the time limit per iteration is no longer fixed for an analysis. Instead, we fix the iteration time limit and split it dynamically among the analyses, rewarding analyses that previously covered more test goals per time unit.