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 11 witnesses for program sv-benchmarks/c/termination-libowfat/strlcat_true-termination.c.i, 4a2b4697f5c3b66d485090307ef74ec11d08954b2ae38adb1c0f438a86221c12
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/4a2b4697f5c3b66d485090307ef74ec11d08954b2ae38adb1c0f438a86221c12.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
5db917b | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2023-12-18T08:51:36+01:00 | ||
f6b6141 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 3 | 2023-11-29T21:43:10Z | ||
d345d6f | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 7.4.0 incr | 7 | 2023-12-01T10:41:41Z | ||
3f1780c | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Taipan | 12 | 2023-12-02T13:48:09Z | ||
f821215 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Kojak | 12 | 2023-12-03T01:29:13Z | ||
8a68bf3 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CBMC | 14 | 2023-12-17T19:54:41+01:00 | ||
2fbb389 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Automizer | 12 | 2023-11-29T00:28:37Z | ||
281a10c | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | sv-sanitizers 0.1.1 | 3 | 2023-11-28T22:07:12Z | ||
59379b5 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | Bubaak | 3 | 2023-12-05T07:43:51Z | ||
54c834e | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | Bubaak | 3 | 2023-12-04T05:21:38Z | ||
25ccfae | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | Bubaak | 3 | 2023-12-01T19:38:54Z |
Found 9 witnesses for program sv-benchmarks/c/termination-libowfat/strlcat_true-termination.c.i, 4a2b4697f5c3b66d485090307ef74ec11d08954b2ae38adb1c0f438a86221c12
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/4a2b4697f5c3b66d485090307ef74ec11d08954b2ae38adb1c0f438a86221c12.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
150c309 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2022-12-09T07:10:08+01:00 | ||
acaae41 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 3 | 2022-12-12T14:54:30Z | ||
1a4b55c | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 7.0.0 incr | 6 | 2022-12-18T18:15:42Z | ||
753b43a | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 6.8.0 incr | 6 | 2022-12-25T12:28:59Z | ||
5a7cc4e | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Taipan | 12 | 2022-12-14T12:03:59Z | ||
6c3133d | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Kojak | 12 | 2022-12-15T02:39:04Z | ||
05c1e11 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CBMC | 14 | 2022-12-08T04:44:05+01:00 | ||
821db26 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Automizer | 12 | 2022-12-13T14:16:41Z | ||
8301382 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | Bubaak | 3 | 2022-12-08T21:17:44Z |
Found 1 witnesses for program sv-benchmarks/c/termination-libowfat/strlcat_true-termination.c.i, 4a2b4697f5c3b66d485090307ef74ec11d08954b2ae38adb1c0f438a86221c12
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/4a2b4697f5c3b66d485090307ef74ec11d08954b2ae38adb1c0f438a86221c12.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
baaa59b | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2021-12-10T17:26:37 |
Found 2 witnesses for program sv-benchmarks/c/termination-libowfat/strlcat_true-termination.c.i, 4a2b4697f5c3b66d485090307ef74ec11d08954b2ae38adb1c0f438a86221c12
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/4a2b4697f5c3b66d485090307ef74ec11d08954b2ae38adb1c0f438a86221c12.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
ae5fb07 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2020-12-11T15:57:47 | ||
755ad04 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2020-12-08T19:37:17 |
Found 0 witnesses for program sv-benchmarks/c/termination-libowfat/strlcat_true-termination.c.i, 4a2b4697f5c3b66d485090307ef74ec11d08954b2ae38adb1c0f438a86221c12
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/4a2b4697f5c3b66d485090307ef74ec11d08954b2ae38adb1c0f438a86221c12.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/termination-libowfat/strlcat_true-termination.c.i, 4a2b4697f5c3b66d485090307ef74ec11d08954b2ae38adb1c0f438a86221c12
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/4a2b4697f5c3b66d485090307ef74ec11d08954b2ae38adb1c0f438a86221c12.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/termination-libowfat/strlcat_true-termination.c.i, 4a2b4697f5c3b66d485090307ef74ec11d08954b2ae38adb1c0f438a86221c12
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/4a2b4697f5c3b66d485090307ef74ec11d08954b2ae38adb1c0f438a86221c12.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/termination-libowfat/strlcat_true-termination.c.i, 4a2b4697f5c3b66d485090307ef74ec11d08954b2ae38adb1c0f438a86221c12
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/4a2b4697f5c3b66d485090307ef74ec11d08954b2ae38adb1c0f438a86221c12.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |