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/0f7bdaee5b0cf49082ce5337e41832ab8886f2bf33b67653d50a5a1a80f03f85.json

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

Found 0 witnesses for program sv-benchmarks/c/pthread-wmm/mix036_pso.opt_false-unreach-call.i, 14b7a2e1dd05863790de8e0ff1ca269e95115af8fbf02ecd2d4e9a32b91ec80f
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/14b7a2e1dd05863790de8e0ff1ca269e95115af8fbf02ecd2d4e9a32b91ec80f.json

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

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

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

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

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

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

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

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

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

Found 10 witnesses for program sv-benchmarks/c/pthread-wmm/mix036_pso.opt_false-unreach-call.i, 14b7a2e1dd05863790de8e0ff1ca269e95115af8fbf02ecd2d4e9a32b91ec80f
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/14b7a2e1dd05863790de8e0ff1ca269e95115af8fbf02ecd2d4e9a32b91ec80f.json

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness
960fdbe	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	SMACK 1.9.3	3	2018-12-08T05:42:13
55a06b3	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.7-svn b8d6131600+	22	2018-12-07T08:59:29+01:00
c6fbc66	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.7-svn 29852	18	2018-12-09T21:49:48+01:00	14f6598
294f997	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.7-svn 29852	18	2018-12-09T21:38:28+01:00	c6ba134
a3402ff	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.7-svn 29852	23	2018-12-08T07:54:15+01:00	55a06b3
bccd81a	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.7-svn 29852	83	2018-12-08T04:56:48+01:00	fff193f
db8d41e	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.7-svn 29852	19	2018-12-06T19:52:24+01:00	8848ffb
1da3a2e	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.7-svn 29852	83	2018-12-06T10:16:16+01:00	8ccdd1d
613c195	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.7-svn 29852	23	2018-12-06T09:49:20+01:00	6c3c8a6
6c3c8a6	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.7-svn 29852	22	2018-12-05T21:24:46+01:00

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

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

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness
23c6472	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	Yogar-CBMC 1.0	16	2017-12-03T05:42 CET (sv-comp)
b03a0b3	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.6.1-svn 26773	20	2017-12-01T09:51:28+01:00
0f7bdae	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CBMC	4	2017-12-01T10:21 CET (sv-comp)
3edd290	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26773	18	2017-12-01T08:48:24+01:00	8f59120
215f6c2	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26758M	16	2017-12-01T08:46:36+01:00

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

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