sv-benchmarks icon indicating copy to clipboard operation
sv-benchmarks copied to clipboard

DynamiTe's NLA termination benchmarks

Open letonchanh opened this issue 3 years ago • 0 comments

Dear SV-COMP Community,

We would like to contribute our NLA termination benchmarks, which have been used in the OOPSLA'20 paper "DynamiTe: Dynamic termination and non-termination proofs" to sv-benchmarks. The benchmarks were added into the folder c/termination-nla. Please let us know if there are any issues.

Thank you very much for your consideration. We are looking forward to your acceptance.

  • [x] programs added to new and appropriately named directory

  • [x] license present and acceptable (in machine-readable comment at beginning of program as specified by the REUSE project)

  • [x] 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)

  • [x] intended property matches the corresponding .prp file

  • [x] programs and expected answer added to a .yml file according to task definitions

  • [x] data model present in task-definition file
  • [x] original (ideally not preprocessed) sources present
  • [x] preprocessed files present
  • [x] preprocessed files generated with correct architecture
  • [x] Makefile added with correct content and without overly broad suppression of warnings

On behalf of DynamiTe team,

Ton Chanh Le

letonchanh avatar Jun 15 '21 02:06 letonchanh