Skip to content

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
Edited by Hernan Ponce de Leon

Merge request reports

Loading