Many of my research projects had some sets of benchmarks for various problem classes as side results. You can download some of them on this page.

  • MaxSAT instances for computing approximately propation complete and conflict propagating CNF encodings of constraints over Boolean variables: This benchmark set was submitted to the MaxSAT Evaluation 2018 and is based on the SAT 2018 paper that I co-authored. The benchmark set is available here.

  • Formal neural network verification (collision avoidance): This benchmark set was developed for and explained in my ATVA 2017 paper and encodes robustness checks for feed-forward neural network behavior. The benchmarks can be obtained here and the file format is explained here.

    A preprint of the paper is available on ArXiV/CoRR. Copyright by Springer Verlag. The final publication is available at

    Note that the preprint has exactly the same content as the published version.

  • GUI Glue Code Synthesis Specifications from the expense splitting Android application translated to the semantics and syntax used in the Reactive Synthesis competition (SyntCOMP). The specification require the use of a synthesis tool for full linear temporal logic, such as Strix. The specifications can be downloaded here.