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/2018/results/witnessInfoByHash/e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855.json

The following keys are missing in the witness XML file: witness-type, sourcecodelang, producer, specification, programfile, programhash, architecture.

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

Found 0 witnesses for program sv-benchmarks/c/heap-manipulation/bubble_sort_linux_true-unreach-call_true-valid-memsafety.i, 0b4ac4d97d9e5c01f1c97fed7997e675193c91bbb9d1cc8f26b56c91f0719893
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/0b4ac4d97d9e5c01f1c97fed7997e675193c91bbb9d1cc8f26b56c91f0719893.json

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

Found 0 witnesses for program sv-benchmarks/c/heap-manipulation/bubble_sort_linux_true-unreach-call_true-valid-memsafety.i, 0b4ac4d97d9e5c01f1c97fed7997e675193c91bbb9d1cc8f26b56c91f0719893
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/0b4ac4d97d9e5c01f1c97fed7997e675193c91bbb9d1cc8f26b56c91f0719893.json

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

Found 0 witnesses for program sv-benchmarks/c/heap-manipulation/bubble_sort_linux_true-unreach-call_true-valid-memsafety.i, 0b4ac4d97d9e5c01f1c97fed7997e675193c91bbb9d1cc8f26b56c91f0719893
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/0b4ac4d97d9e5c01f1c97fed7997e675193c91bbb9d1cc8f26b56c91f0719893.json

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

Found 0 witnesses for program sv-benchmarks/c/heap-manipulation/bubble_sort_linux_true-unreach-call_true-valid-memsafety.i, 0b4ac4d97d9e5c01f1c97fed7997e675193c91bbb9d1cc8f26b56c91f0719893
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/0b4ac4d97d9e5c01f1c97fed7997e675193c91bbb9d1cc8f26b56c91f0719893.json

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

Found 5 witnesses for program sv-benchmarks/c/heap-manipulation/bubble_sort_linux_true-unreach-call_true-valid-memsafety.i, 0b4ac4d97d9e5c01f1c97fed7997e675193c91bbb9d1cc8f26b56c91f0719893
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/0b4ac4d97d9e5c01f1c97fed7997e675193c91bbb9d1cc8f26b56c91f0719893.json

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness
fa82270	Inspect		CHECK( init(main()), LTL(G valid-memtrack) )	correctness_witness	CPAchecker 1.9	34	2019-11-29T19:45:48+01:00
feb5b72	Inspect		CHECK( init(main()), LTL(G valid-memtrack) )	correctness_witness	CPAchecker 1.8-svn-35b8bb3bb3+	34	2019-12-01T18:42:34+01:00
e62dc33	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.9 / witnessValidation	34	2019-12-07T23:47:56+01:00	faf328e
fc7ab3d	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.9 / witnessValidation	34	2019-11-30T16:09:33+01:00	2cba010
2cba010	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.9 / svcomp20	34	2019-11-30T02:48:27+01:00

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

Found 8 witnesses for program sv-benchmarks/c/heap-manipulation/bubble_sort_linux_true-unreach-call_true-valid-memsafety.i, 0b4ac4d97d9e5c01f1c97fed7997e675193c91bbb9d1cc8f26b56c91f0719893
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/0b4ac4d97d9e5c01f1c97fed7997e675193c91bbb9d1cc8f26b56c91f0719893.json

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness
6408f4a	Inspect		CHECK( init(main()), LTL(G valid-memtrack) )	correctness_witness	CPAchecker 1.7-svn b8d6131600+	34	2018-12-07T05:54:21+01:00
5ca9602	Inspect		CHECK( init(main()), LTL(G valid-free) )	correctness_witness	CPAchecker 1.7-svn 29852	34	2018-12-05T11:42:17+01:00
36d1239	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7-svn b8d6131600+	34	2018-12-07T13:24:29+01:00
c19926d	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7-svn 29852	34	2018-12-08T05:55:06+01:00	36d1239
5f9bcff	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7-svn 29852	34	2018-12-07T08:47:55+01:00	2d5fe97
2adcce2	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7-svn 29852	34	2018-12-06T09:43:07+01:00	6051c40
081db4a	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7-svn 29852	34	2018-12-06T09:00:07+01:00	1151682
1151682	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7-svn 29852	34	2018-12-06T06:33:25+01:00

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

Found 2 witnesses for program sv-benchmarks/c/heap-manipulation/bubble_sort_linux_true-unreach-call_true-valid-memsafety.i, 0b4ac4d97d9e5c01f1c97fed7997e675193c91bbb9d1cc8f26b56c91f0719893
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/0b4ac4d97d9e5c01f1c97fed7997e675193c91bbb9d1cc8f26b56c91f0719893.json

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness
2d5fe97	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	PredatorHP	4	2017-12-01T20:30 CET (sv-comp)
e197f7b	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26773	34	2017-12-01T21:18:05+01:00	bdcf79a

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

Found 0 witnesses for program sv-benchmarks/c/heap-manipulation/bubble_sort_linux_true-unreach-call_true-valid-memsafety.i, 0b4ac4d97d9e5c01f1c97fed7997e675193c91bbb9d1cc8f26b56c91f0719893
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/0b4ac4d97d9e5c01f1c97fed7997e675193c91bbb9d1cc8f26b56c91f0719893.json