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/strcspn_true-termination.c.i, 3537cd0bed922b783c5bc2cf1d153661eb68e22062217013fbb7937014c3d604
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/3537cd0bed922b783c5bc2cf1d153661eb68e22062217013fbb7937014c3d604.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
64f95d9 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2023-12-18T09:44:18+01:00 | ||
528c614 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 8 | 2023-12-18T12:05:11+01:00 | 64f95d9 | |
4b9ea9b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 8 | 2023-11-30T08:26:46+01:00 | ||
5aebae2 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2.1-svn-e677b7cd46+ | 8 | 2023-12-03T18:18:36+01:00 | ||
0cd6bdc | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.1 | 8 | 2023-12-17T01:52:06+01:00 | ||
b5a5c5f | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-38892M | 11 | 2023-12-18T02:14:06+01:00 | ||
1b20533 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 2.0 | 8 | 2023-12-19T12:26:19+01:00 | ||
c827516 | 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 | 16 | 2023-12-02T13:28:02Z | ||
6524cce | 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-29T02:15:14Z | ||
666641c | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 8 | 2023-12-18T17:04:07+01:00 | ||
902f0c6 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Goblint (tags/svcomp24-0-gc2e9465a7) | 3 | 2023-12-01T01:26:49Z |
Found 10 witnesses for program sv-benchmarks/c/termination-libowfat/strcspn_true-termination.c.i, 3537cd0bed922b783c5bc2cf1d153661eb68e22062217013fbb7937014c3d604
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/3537cd0bed922b783c5bc2cf1d153661eb68e22062217013fbb7937014c3d604.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
92b9480 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2022-12-09T06:56:45+01:00 | ||
e369334 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 8 | 2023-01-28T14:19:10+01:00 | 92b9480 | |
a4bb24d | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 8 | 2022-12-10T18:35:49+01:00 | ||
04955c6 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2.1-svn-1715bd67dc+ | 8 | 2022-12-11T22:12:34+01:00 | ||
709a754 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.1 | 8 | 2022-12-25T11:59:45+01:00 | ||
234ac8b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0 | 8 | 2022-12-11T04:27:52+01:00 | ||
9dcd0d1 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-38892M | 11 | 2022-12-09T02:49:10+01:00 | ||
b46c108 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 8 | 2022-12-09T23:22:22+01:00 | ||
4b832bc | 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-14T14:23:13Z | ||
367067c | 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 | 15 | 2022-12-13T21:01:40Z |
Found 1 witnesses for program sv-benchmarks/c/termination-libowfat/strcspn_true-termination.c.i, 3537cd0bed922b783c5bc2cf1d153661eb68e22062217013fbb7937014c3d604
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/3537cd0bed922b783c5bc2cf1d153661eb68e22062217013fbb7937014c3d604.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
28db80c | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2021-12-10T19:11:20 |
Found 2 witnesses for program sv-benchmarks/c/termination-libowfat/strcspn_true-termination.c.i, 3537cd0bed922b783c5bc2cf1d153661eb68e22062217013fbb7937014c3d604
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/3537cd0bed922b783c5bc2cf1d153661eb68e22062217013fbb7937014c3d604.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
1fa4f41 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2020-12-11T21:01:46 | ||
528bb83 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2020-12-08T14:40:37 |
Found 0 witnesses for program sv-benchmarks/c/termination-libowfat/strcspn_true-termination.c.i, 3537cd0bed922b783c5bc2cf1d153661eb68e22062217013fbb7937014c3d604
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/3537cd0bed922b783c5bc2cf1d153661eb68e22062217013fbb7937014c3d604.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/strcspn_true-termination.c.i, 3537cd0bed922b783c5bc2cf1d153661eb68e22062217013fbb7937014c3d604
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/3537cd0bed922b783c5bc2cf1d153661eb68e22062217013fbb7937014c3d604.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/strcspn_true-termination.c.i, 3537cd0bed922b783c5bc2cf1d153661eb68e22062217013fbb7937014c3d604
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/3537cd0bed922b783c5bc2cf1d153661eb68e22062217013fbb7937014c3d604.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/strcspn_true-termination.c.i, 3537cd0bed922b783c5bc2cf1d153661eb68e22062217013fbb7937014c3d604
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/3537cd0bed922b783c5bc2cf1d153661eb68e22062217013fbb7937014c3d604.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |