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/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/pthread-wmm/mix008_power.oepc_false-unreach-call.i, ac23db92ca27faacfa8cdef025d7c8ba6526332576bbc6e9b30db3644a1bf010
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/ac23db92ca27faacfa8cdef025d7c8ba6526332576bbc6e9b30db3644a1bf010.json

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

Found 0 witnesses for program sv-benchmarks/c/pthread-wmm/mix008_power.oepc_false-unreach-call.i, ac23db92ca27faacfa8cdef025d7c8ba6526332576bbc6e9b30db3644a1bf010
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/ac23db92ca27faacfa8cdef025d7c8ba6526332576bbc6e9b30db3644a1bf010.json

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

Found 0 witnesses for program sv-benchmarks/c/pthread-wmm/mix008_power.oepc_false-unreach-call.i, ac23db92ca27faacfa8cdef025d7c8ba6526332576bbc6e9b30db3644a1bf010
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/ac23db92ca27faacfa8cdef025d7c8ba6526332576bbc6e9b30db3644a1bf010.json

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

Found 0 witnesses for program sv-benchmarks/c/pthread-wmm/mix008_power.oepc_false-unreach-call.i, ac23db92ca27faacfa8cdef025d7c8ba6526332576bbc6e9b30db3644a1bf010
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/ac23db92ca27faacfa8cdef025d7c8ba6526332576bbc6e9b30db3644a1bf010.json

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

Found 0 witnesses for program sv-benchmarks/c/pthread-wmm/mix008_power.oepc_false-unreach-call.i, ac23db92ca27faacfa8cdef025d7c8ba6526332576bbc6e9b30db3644a1bf010
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/ac23db92ca27faacfa8cdef025d7c8ba6526332576bbc6e9b30db3644a1bf010.json

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

Found 8 witnesses for program sv-benchmarks/c/pthread-wmm/mix008_power.oepc_false-unreach-call.i, ac23db92ca27faacfa8cdef025d7c8ba6526332576bbc6e9b30db3644a1bf010
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/ac23db92ca27faacfa8cdef025d7c8ba6526332576bbc6e9b30db3644a1bf010.json

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness
b1dc282	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	SMACK 1.9.3	3	2018-12-08T06:07:37
36ae0fa	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.7-svn b8d6131600+	35	2018-12-06T23:26:55+01:00
1de852b	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.7-svn 29852	31	2018-12-09T21:47:41+01:00	be59692
25c056c	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.7-svn 29852	30	2018-12-09T21:38:35+01:00	56d6cd2
59a2a3f	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.7-svn 29852	32	2018-12-06T19:53:44+01:00	58535e3
13a2923	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.7-svn 29852	35	2018-12-06T07:55:18+01:00
492c747	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7-svn 29852	17	2018-12-08T08:58:58+01:00	36ae0fa
60dc700	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7-svn 29852	17	2018-12-06T09:50:03+01:00	13a2923

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

Found 5 witnesses for program sv-benchmarks/c/pthread-wmm/mix008_power.oepc_false-unreach-call.i, ac23db92ca27faacfa8cdef025d7c8ba6526332576bbc6e9b30db3644a1bf010
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/ac23db92ca27faacfa8cdef025d7c8ba6526332576bbc6e9b30db3644a1bf010.json

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness
1b82d8b	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	Yogar-CBMC 1.0	18	2017-12-03T05:38 CET (sv-comp)
60983a0	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.6.1-svn 26773	30	2017-12-01T10:21:30+01:00
3ed3d81	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CBMC	4	2017-12-01T10:13 CET (sv-comp)
d3f908d	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26773	18	2017-12-01T08:48:28+01:00	fb0943b
e662d47	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26758M	18	2017-12-01T08:46:39+01:00

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

Found 0 witnesses for program sv-benchmarks/c/pthread-wmm/mix008_power.oepc_false-unreach-call.i, ac23db92ca27faacfa8cdef025d7c8ba6526332576bbc6e9b30db3644a1bf010
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/ac23db92ca27faacfa8cdef025d7c8ba6526332576bbc6e9b30db3644a1bf010.json