Every Component Matters: Generating Parallel Verification Benchmarks with Hardness Guarantees

In this paper, we show how to automatically generate hard verification tasks in order to support events like the Model Checking Contest or the Rigorous Examination of Reactive Systems Challenge with tailored benchmark problems for analyzing the validity of linear-time properties in parallel systems. Characteristic of the generated benchmarks are two hardness guarantees: (i) every parallel component is relevant and (ii) the state space of the analyzed system is exponential in the number of its parallel components. Generated benchmarks can be made available, e.g., as Promela code or Petri nets.