Add pthread-deagle benchmarks under ConcurrentSafety Category
Dear SV-COMP Community,
We would like to contribute our pthread-deagle
benchmarks, which have been used in the PLDI'2021 paper "Satisfiability modulo ordering consistency theory for multi-threaded program verification"(DOI) and latter unpublished works. The benchmarks were added into a new folder c/pthread-deagle
under the ConcurrencySafety
Category.
Each benchmark contains .c
.i
and .yml
file. We format these benchmarks with REUSE
project, provide README.md
and Makefile
, and passed Compile and Sanity Checks
following your contribution guideline. All the benchmarks are under the Apache 2.0
license. Please let us know if there are any issues.
Thank you very much for your consideration. We are looking forward to your acceptance.
Best Regards.
-
programs added to new and appropriately named directory -
license present and acceptable (in machine-readable comment at beginning of program as specified by the REUSE project) -
contributed-by present (either in README file or as comment at beginning of program) -
programs added to a .set
file of an existing category, or new sub-category established (if justified) -
intended property matches the corresponding .prp
file -
programs and expected answer added to a .yml
file according to task definitions
-
data model present in task-definition file -
original (ideally not preprocessed) sources present -
preprocessed files present -
preprocessed files generated with correct architecture -
Makefile added with correct content and without overly broad suppression of warnings