Reproduction Package for Article `Cooperation between Automatic and Interactive Software Verifiers'

Benchmark Set for Cooperation This artifact contains the benchmark set that was created as part of a publication on Cooperation between Automatic and Interactive Software Verifiers. The benchmark set consists of 330 verification tasks which use information from the correctness witnesses of the ReachSafety-Loops category of SV-COMP 2021. There are two versions of these tasks: In one version that can be found in the folder assertions we take the invariants in the witnesses and translated them into assertions in the programs In the other version we convert the invariants into ACSL annotations instead, these can be found in the folder named annotations The directory structure is as follows: assertions |-2ls.xml # benchmark definition file for a consuming verifier |- ... # benchmark definition files for every other consuming verifier |-automizer # folder for a producing verifier |-2ls.set # a set file specifying which of the tasks in this directory are part of our 330 task benchmark set |-simple_3-2.c # a program for a task, where the invariants from the witness of automizer have been added as assertions |-simple_3-2.cyml # the task definition file |- ... # other tasks |- ... # directories for other producers |-plain # directory with original, unmodified programs as well as all witnesses that were used. |-simple_3-2.c |-simple_3-2.yml |-simple_3-2.yml_automizer.graphml # a witness of veriabs for this task |- ... # other witnesses for the same task |- ... # other tasks annotations |- ... # mostly identical to the `assertions folder`, just the generated programs contain ACSL annotations instead of assumptions frama-c-sv # the version of frama-c-sv used for the benchmarks in the corresponding publication |-frama-c-sv.py |- ..