Benchmarks

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 link.springer.com.
  
  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.

• The FreeQBF Specifications for Reactive Synthesis were built for Dagstuhl Seminar 24171 and describe the intermediated fixed points computed during a GR(1) synthesis fixed point computation. They are available in the form of QDIMACS files and QCIR files, where the latter contains the operations performed to arrive at a Boolean formulas representing the prefixed point. You can obtain the benchmark set here. The ZIP file includes a few slides that describe on a high level what is encoded. The GR(1) specifications from which the benchmarks were built are also included.