Sebastian Ruland, Malte Lochau, Andy Schürr, and Oliver Fehse

Software model checkers can generate high-quality test cases from counterexamples of a reachability analysis. However, naively invoking a model checker for each test goal in isolation does not scale to large programs as a repeated construction of an abstract program model is expensive. In contrast, invoking a model checker for all test goals in a single run leads to low abstraction possibilities and thus to low scalability. Our approach therefore pursues a test-suite generation technique that allows for configurable multi-goal set partitioning (MGP), using configurable partitioning strategies, and simultaneous processing of multiple test goals in one reachability analysis. Our approach therefore employs recent techniques from multi-property verification in order to control the computational overhead for tracking multi-goal reachability information. Our tool, called CPA/Tiger-MGP, uses predicate-abstraction-based program analysis in the model-checking frameworkCPAchecker.

The submitted Version of CPA/Tiger-MGP for Test-Comp is built from revision 30601 from the official CPAchecker repository, branch tigerIntegration2.

To run CPA/Tiger-MGP, enter the following command:

• scripts/cpa.sh -benchmark -heap 10000M -tigertestcomp19 -spec spec.prp task

where spec is either coverage-error-call or coverage-branches and task is the c or intermediate file to be analysed. CPA/Tiger-MGP prints statistics of the run to the console and writes test-cases and test-suite meta-data in the output folder. To reproduce the results, use a Linux system with Java 8 runtime environment, BenchExec, SV-Benchmarks and run Benchexec with the following files:

• the benchmark definition hybridtiger.py which is archived at https://gitlab.com/sosy-lab/test-comp/bench-defs/blob/master/benchmark-defs/hybridtiger.xml
• the tool-info module cpachecker.py which can be found at https://github.com/sosy-lab/benchexec/tree/master/benchexec/tools

This work was funded by the Hessian LOEWE initiative within the Software-Factory 4.0 project.