A description of this web service can be found in the CAV paper "Verification-Aided Debugging: An Interactive Web-Service for Exploring Error Witnesses" (more material).
Found 10 witnesses for program sv-benchmarks/c/termination-15/cstrncpy_diffterm_alloca_true-termination.c.i, 29a0de6b7697865a37e60a82150f204059592b57f74fd0ca1d5024446fc510b4
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/29a0de6b7697865a37e60a82150f204059592b57f74fd0ca1d5024446fc510b4.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
fe91056 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2023-12-18T09:58:11+01:00 | ||
0dcb76c | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 7 | 2023-12-18T12:07:45+01:00 | fe91056 | |
89c7367 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 7 | 2023-11-30T09:07:33+01:00 | ||
2568e16 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2.1-svn-e677b7cd46+ | 7 | 2023-12-03T22:18:43+01:00 | ||
0212561 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.1 | 7 | 2023-12-17T02:50:53+01:00 | ||
3f18bc5 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 7 | 2023-12-18T19:42:35+01:00 | ||
5ff8e56 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-38892M | 12 | 2023-12-18T01:33:31+01:00 | ||
e932ec8 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Automizer | 16 | 2023-11-29T03:42:42Z | ||
a2ce263 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 2.0 | 7 | 2023-12-19T11:15:30+01:00 | ||
3cc2983 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Goblint (tags/svcomp24-0-gc2e9465a7) | 3 | 2023-12-01T01:44:24Z |
Found 9 witnesses for program sv-benchmarks/c/termination-15/cstrncpy_diffterm_alloca_true-termination.c.i, 29a0de6b7697865a37e60a82150f204059592b57f74fd0ca1d5024446fc510b4
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/29a0de6b7697865a37e60a82150f204059592b57f74fd0ca1d5024446fc510b4.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
b513eae | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2022-12-09T05:23:57+01:00 | ||
ff396a0 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 7 | 2023-01-28T14:19:43+01:00 | b513eae | |
7b44277 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 7 | 2022-12-10T19:02:57+01:00 | ||
fd88dbb | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2.1-svn-1715bd67dc+ | 7 | 2022-12-12T01:08:19+01:00 | ||
130cbc7 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.1 | 7 | 2022-12-25T11:45:32+01:00 | ||
ddded96 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 7 | 2022-12-10T01:23:56+01:00 | ||
90b73fd | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-38892M | 12 | 2022-12-09T02:54:13+01:00 | ||
288fff3 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 2.0 | 7 | 2022-12-11T05:10:17+01:00 | ||
2048b79 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Taipan | 15 | 2022-12-14T09:13:11Z |
Found 1 witnesses for program sv-benchmarks/c/termination-15/cstrncpy_diffterm_alloca_true-termination.c.i, 29a0de6b7697865a37e60a82150f204059592b57f74fd0ca1d5024446fc510b4
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/29a0de6b7697865a37e60a82150f204059592b57f74fd0ca1d5024446fc510b4.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
851dd18 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2021-12-10T19:03:04 |
Found 2 witnesses for program sv-benchmarks/c/termination-15/cstrncpy_diffterm_alloca_true-termination.c.i, 29a0de6b7697865a37e60a82150f204059592b57f74fd0ca1d5024446fc510b4
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/29a0de6b7697865a37e60a82150f204059592b57f74fd0ca1d5024446fc510b4.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
f6f05a6 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2020-12-11T14:23:54 | ||
c5b90e8 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2020-12-08T23:56:41 |
Found 0 witnesses for program sv-benchmarks/c/termination-15/cstrncpy_diffterm_alloca_true-termination.c.i, 29a0de6b7697865a37e60a82150f204059592b57f74fd0ca1d5024446fc510b4
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/29a0de6b7697865a37e60a82150f204059592b57f74fd0ca1d5024446fc510b4.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/termination-15/cstrncpy_diffterm_alloca_true-termination.c.i, 29a0de6b7697865a37e60a82150f204059592b57f74fd0ca1d5024446fc510b4
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/29a0de6b7697865a37e60a82150f204059592b57f74fd0ca1d5024446fc510b4.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/termination-15/cstrncpy_diffterm_alloca_true-termination.c.i, 29a0de6b7697865a37e60a82150f204059592b57f74fd0ca1d5024446fc510b4
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/29a0de6b7697865a37e60a82150f204059592b57f74fd0ca1d5024446fc510b4.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/termination-15/cstrncpy_diffterm_alloca_true-termination.c.i, 29a0de6b7697865a37e60a82150f204059592b57f74fd0ca1d5024446fc510b4
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/29a0de6b7697865a37e60a82150f204059592b57f74fd0ca1d5024446fc510b4.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |