Synthesizing Subtle Bugs with Known Witnesses.

This paper presents a new technique for the generation of verification benchmarks that are automatically guaranteed to be hard, or as we say, to contain subtle bugs/property violations: (i) Identifying a bug requires to match many computation steps and (ii) corresponding counterexamples are sparse among all feasible executions. Key idea is to iteratively synthesize Buchi automata for variations of a set of LTL properties and to combine these automata in a fashion that each property can be individually controlled in the resulting model: Based on our notion of a counterexample handle, it is possible to switch the satisfaction of a given property on and off without affecting that of the other considered properties. This orthogonality of our treatment of counterexamples is vital for the subsequent parts of the benchmark generation process. Together with the mentioned hardness, it helps to overcome the undesired clustering of counterexamples observed during previous iterations of the RERS Challenge. Even more importantly, these handles and associated counterexamples are sufficient to automatically generate the modal contracts required for the parallel decomposition process that allows us to generate parallel verification benchmarks of arbitrary size, for example in form of a Petri net or in Promela.