CPA/Tiger-MGP: Test-Goal Set Partitioning forEfficient Multi-Goal Test-Suite Generation – Replication Package


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.

Supplementary Data

CPA/Tiger-MGP1, 2, 3
Benchmark definitionXML


Reproducing the Results

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:


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