Witness Inspection

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).

This link does not point to a witness, but below is a list of witnesses for the same program.

Available Results for the Program from Witness Store SV-COMP '24

Trying to find witnesses for program (5777537c095ec59108b5d9f37cf81712da3de2e0342074f5f1b9baa22f97ec21, sv-benchmarks/c/termination-memory-linkedlists/cll_by_lseg_traverse-alloca_false-termination.c.i).

Found 3 witnesses for program sv-benchmarks/c/termination-memory-linkedlists/cll_by_lseg_traverse-alloca_false-termination.c.i, 5777537c095ec59108b5d9f37cf81712da3de2e0342074f5f1b9baa22f97ec21
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/5777537c095ec59108b5d9f37cf81712da3de2e0342074f5f1b9baa22f97ec21.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download adf3102 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Bubaak 3 2023-12-05T11:54:07Z
Download 6d30c78 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Bubaak 3 2023-12-04T12:43:37Z
Download 2bcb0cb Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Automizer 9 2023-11-29T05:03:07Z

Available Results for the Program from Witness Store SV-COMP '23

Trying to find witnesses for program (5777537c095ec59108b5d9f37cf81712da3de2e0342074f5f1b9baa22f97ec21, sv-benchmarks/c/termination-memory-linkedlists/cll_by_lseg_traverse-alloca_false-termination.c.i).

Found 2 witnesses for program sv-benchmarks/c/termination-memory-linkedlists/cll_by_lseg_traverse-alloca_false-termination.c.i, 5777537c095ec59108b5d9f37cf81712da3de2e0342074f5f1b9baa22f97ec21
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/5777537c095ec59108b5d9f37cf81712da3de2e0342074f5f1b9baa22f97ec21.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 34fc684 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Bubaak 3 2022-12-08T15:03:27Z
Download 4001bf3 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Automizer 9 2022-12-13T16:35:19Z

Available Results for the Program from Witness Store SV-COMP '22

Trying to find witnesses for program (5777537c095ec59108b5d9f37cf81712da3de2e0342074f5f1b9baa22f97ec21, sv-benchmarks/c/termination-memory-linkedlists/cll_by_lseg_traverse-alloca_false-termination.c.i).

Found 2 witnesses for program sv-benchmarks/c/termination-memory-linkedlists/cll_by_lseg_traverse-alloca_false-termination.c.i, 5777537c095ec59108b5d9f37cf81712da3de2e0342074f5f1b9baa22f97ec21
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/5777537c095ec59108b5d9f37cf81712da3de2e0342074f5f1b9baa22f97ec21.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 1033f90 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Automizer 9 2021-12-06T18:42:30Z
Download 6c43b01 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 2 2021-12-10T16:12:59

Available Results for the Program from Witness Store SV-COMP '21

Trying to find witnesses for program (5777537c095ec59108b5d9f37cf81712da3de2e0342074f5f1b9baa22f97ec21, sv-benchmarks/c/termination-memory-linkedlists/cll_by_lseg_traverse-alloca_false-termination.c.i).

Found 2 witnesses for program sv-benchmarks/c/termination-memory-linkedlists/cll_by_lseg_traverse-alloca_false-termination.c.i, 5777537c095ec59108b5d9f37cf81712da3de2e0342074f5f1b9baa22f97ec21
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/5777537c095ec59108b5d9f37cf81712da3de2e0342074f5f1b9baa22f97ec21.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 20e669f Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 2 2020-12-11T19:35:24
Download 80a4f3c Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 2 2020-12-08T23:02:59

Available Results for the Program from Witness Store SV-COMP '20

Trying to find witnesses for program (5777537c095ec59108b5d9f37cf81712da3de2e0342074f5f1b9baa22f97ec21, sv-benchmarks/c/termination-memory-linkedlists/cll_by_lseg_traverse-alloca_false-termination.c.i).

Found 0 witnesses for program sv-benchmarks/c/termination-memory-linkedlists/cll_by_lseg_traverse-alloca_false-termination.c.i, 5777537c095ec59108b5d9f37cf81712da3de2e0342074f5f1b9baa22f97ec21
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/5777537c095ec59108b5d9f37cf81712da3de2e0342074f5f1b9baa22f97ec21.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness

Available Results for the Program from Witness Store SV-COMP '19

Trying to find witnesses for program (5777537c095ec59108b5d9f37cf81712da3de2e0342074f5f1b9baa22f97ec21, sv-benchmarks/c/termination-memory-linkedlists/cll_by_lseg_traverse-alloca_false-termination.c.i).

Found 0 witnesses for program sv-benchmarks/c/termination-memory-linkedlists/cll_by_lseg_traverse-alloca_false-termination.c.i, 5777537c095ec59108b5d9f37cf81712da3de2e0342074f5f1b9baa22f97ec21
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/5777537c095ec59108b5d9f37cf81712da3de2e0342074f5f1b9baa22f97ec21.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness

Available Results for the Program from Witness Store SV-COMP '18

Trying to find witnesses for program (5777537c095ec59108b5d9f37cf81712da3de2e0342074f5f1b9baa22f97ec21, sv-benchmarks/c/termination-memory-linkedlists/cll_by_lseg_traverse-alloca_false-termination.c.i).

Found 2 witnesses for program sv-benchmarks/c/termination-memory-linkedlists/cll_by_lseg_traverse-alloca_false-termination.c.i, 5777537c095ec59108b5d9f37cf81712da3de2e0342074f5f1b9baa22f97ec21
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/5777537c095ec59108b5d9f37cf81712da3de2e0342074f5f1b9baa22f97ec21.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download f5ae431 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 9 2017-12-01T19:04 CET (sv-comp)
Download fd79447 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Automizer 9 2017-12-03T11:13Z

Available Results for the Program from Witness Store SV-COMP '17

Trying to find witnesses for program (5777537c095ec59108b5d9f37cf81712da3de2e0342074f5f1b9baa22f97ec21, sv-benchmarks/c/termination-memory-linkedlists/cll_by_lseg_traverse-alloca_false-termination.c.i).

Found 0 witnesses for program sv-benchmarks/c/termination-memory-linkedlists/cll_by_lseg_traverse-alloca_false-termination.c.i, 5777537c095ec59108b5d9f37cf81712da3de2e0342074f5f1b9baa22f97ec21
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/5777537c095ec59108b5d9f37cf81712da3de2e0342074f5f1b9baa22f97ec21.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness