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/e710c46e43f55c94c9af9cde3d9201b88e845fa4ca9b788a8dbf91a09ea1fd36.json

This witness was created for this program (cf. table above, ad6767ef1e79b5a8a226c957c502cc252f68f59821c1bcb31dfbbbe6213ecff6).

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

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

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

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

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

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

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

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

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

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

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

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

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness
f81e653	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	SMACK 1.9.3	3	2018-12-08T00:41:00
66c4a3b	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.7-svn b8d6131600+	26	2018-12-06T13:26:31+01:00
8e19688	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.7-svn 29852	22	2018-12-09T21:49:10+01:00	a9f1a1e
5e34289	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.7-svn 29852	22	2018-12-09T21:38:29+01:00	6f537aa
d396e51	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.7-svn 29852	26	2018-12-08T07:51:01+01:00	66c4a3b
7270d43	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.7-svn 29852	45	2018-12-08T04:54:58+01:00	41d3a87
e710c46	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.7-svn 29852	23	2018-12-06T19:52:41+01:00	11c5cef
751dfa7	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.7-svn 29852	45	2018-12-06T10:14:15+01:00	590ebd6
65471c6	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.7-svn 29852	26	2018-12-06T09:49:03+01:00	fedf127
fedf127	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.7-svn 29852	26	2018-12-05T20:35:55+01:00
12560e3	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7-svn 29852	34	2018-12-10T10:50:07+01:00	fec93bd
aec5491	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7-svn 29852	34	2018-12-06T09:18:46+01:00	895ccdb

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

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

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness
6b1f5d4	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	Yogar-CBMC 1.0	16	2017-12-03T05:58 CET (sv-comp)
8db9c9b	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	ESBMC 3.1	27	2017-12-01T11:46 CET (sv-comp)
3694f02	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.6.1-svn 26773	24	2017-12-01T09:36:01+01:00
895ccdb	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CBMC	4	2017-12-01T10:14 CET (sv-comp)
522a26a	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26773	35	2017-12-01T08:48:24+01:00	d944c99
9538c7d	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26758M	16	2017-12-01T08:46:25+01:00

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

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