sv-benchmarks
sv-benchmarks copied to clipboard
sosy-lab
Collection of Verification Tasks (MOVED, please follow the link)
Dear SV-COMP Community, We would like to contribute our `bwb`(Bitwise with Branching) termination benchmarks used in our work `Proving LTL Properties of Bitvector Programs and Decompiled Binaries`, which was accepted...
markdown-link-check does not solve https://github.com/tcort/markdown-link-check/issues/159, which is a problem for us because of false positives in doi.org. So we resort to the (less nice-looking) linkchecker. We first convert markdown files...
This task contains an overflow, so stating the termination property makes no sense, especially since no verdict is given.
I've noticed that various programs in this repo use `__VERIFIER_nondet_*` functions that seemingly aren't mentioned anywhere in the SV-COMP rules. I'm using [this section of the 2021 SV-COMP rules as...
The following program can overflow ``` int main() { int z, k; long long x, y, c; z = __VERIFIER_nondet_int(); k = __VERIFIER_nondet_int(); assume_abort_if_not(z >= 1); assume_abort_if_not(k >= 1); x...
Currently, the `data_model` key in a task definition is allowed to have the values `ILP32` or `LP64`. This does not contain enough information to deduce the size of all possible...
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...
The program ```pthread-ext/41_FreeBSD_abd_kbd_sliced``` is labeled as ```true```. However there should be a feasible counterexample trace (which Ultimate Automizer also found). One thread can simply call ```akbd_read_char(1)``` and therefore execute the...
The following tasks all have expected undefined behavior (as indicated by `false-valid-deref` or `false-no-overflow`), but also a result for some other property: https://github.com/sosy-lab/sv-benchmarks/blob/50702f8513f655c27b7338b3f363f892958f4ec6/c/check.py#L93-L115 The affected directories are - `busybox-1.22.0` -...