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

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

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

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

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

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

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

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

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

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

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

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

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

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness
3859f80	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	SMACK 1.9.3	3	2018-12-08T11:15:52
d1ef574	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.7-svn b8d6131600+	22	2018-12-07T01:56:43+01:00
a67d911	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.7-svn 29852	18	2018-12-09T21:49:34+01:00	0c636e8
4fdf222	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.7-svn 29852	18	2018-12-09T21:38:29+01:00	2d12218
3df8095	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.7-svn 29852	23	2018-12-08T08:38:50+01:00	d1ef574
8b63cd4	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.7-svn 29852	83	2018-12-08T05:03:01+01:00	99c1610
585ae32	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.7-svn 29852	19	2018-12-06T19:53:57+01:00	914a872
1a3b950	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.7-svn 29852	83	2018-12-06T10:18:32+01:00	8e983af
ee0d2ef	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.7-svn 29852	23	2018-12-06T09:48:11+01:00	2e265d2
2e265d2	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.7-svn 29852	22	2018-12-05T18:55:11+01:00

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

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

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness
b259747	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	Yogar-CBMC 1.0	16	2017-12-03T05:45 CET (sv-comp)
8653750	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.6.1-svn 26773	20	2017-12-01T10:13:29+01:00
37c9bd5	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CBMC	4	2017-12-01T09:53 CET (sv-comp)
6e03053	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	59f29a2
1ebe591	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26758M	16	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/mix039_power.opt_false-unreach-call.i, 3567137ace356cdddabc29d520cdc1e4aca1fcb0532e813392575b465cafc587
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/3567137ace356cdddabc29d520cdc1e4aca1fcb0532e813392575b465cafc587.json