sv-benchmarks
sv-benchmarks copied to clipboard
DynamiTe's NLA termination benchmarks
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