Transition Power Abstractions for Deep Counterexample Detection

Our paper "Transition Power Abstractions for Deep Counterexample Detection" has been accepted to TACAS '22. The artifact accompanying this paper can be found here. It can be used to reproduce the results presented in the paper: it contains the benchmarks, tools, scripts, and instructions how to run the experiments.


Detailed results on benchmarks representing multi-phase loops

Results on unsafe and safe version of the benchmarks, time in seconds, timeout (TO) set to 5 minutes: PDF with tables.

Beside the artifact, the benchmarks can also be found in this GitHub repository.