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

View and Validate the Witness

• View Witness
• 
  Click on the button to verify this program using this witness, and inpect the validation results, e.g., explore the ARG or error path.

Input Given to this Service about the Witness (URL Query)

Information about the Witness from Competition Database

from https://sv-comp.sosy-lab.org/2019/results/witnessInfoByHash/36ae84aab003be59b6a00cf2d4b620dc8c8a8c54deed2a00eb3e31be8f2c4069.json

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

Found 1 witnesses for program sv-benchmarks/c/termination-memory-linkedlists/ll_append-alloca_false-termination.c.i, a94e514ac338898e2e1e54a42b19ae4490ac5c412319209fc14736a6de9b7386
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/a94e514ac338898e2e1e54a42b19ae4490ac5c412319209fc14736a6de9b7386.json

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness
7c86aef	Inspect		CHECK( init(main()), LTL(F end) )	violation_witness	Automizer	11	2023-11-29T01:37:40Z

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

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

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness
8197641	Inspect		CHECK( init(main()), LTL(F end) )	violation_witness	Automizer	12	2022-12-13T12:00:36Z
6fa8fef	Inspect		CHECK( init(main()), LTL(F end) )	correctness_witness	Bubaak	3	2022-12-08T17:45:42Z

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

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

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness
0000143	Inspect		CHECK( init(main()), LTL(F end) )	violation_witness	Automizer	11	2021-12-07T00:43:38Z
7007f4d	Inspect		CHECK( init(main()), LTL(F end) )	correctness_witness	Symbiotic	2	2021-12-10T18:04:16

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

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

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness
60eedc2	Inspect		CHECK( init(main()), LTL(F end) )	correctness_witness	Symbiotic	2	2020-12-11T15:20:11
2d75433	Inspect		CHECK( init(main()), LTL(F end) )	correctness_witness	Symbiotic	2	2020-12-08T15:09:25

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

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

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

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

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

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

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness
160b73c	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	ESBMC 3.1	11	2017-12-01T20:52 CET (sv-comp)
9502475	Inspect		CHECK( init(main()), LTL(F end) )	violation_witness	Automizer	11	2017-12-03T11:15Z

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

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