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/831705df3fb7fa0d5fdd37e730593440edd7e83c6ca3c32cdbb1046a60ce87f6.json

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

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

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

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

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

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

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

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

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

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

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

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

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness
fd16180	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	SMACK 1.9.3	3	2018-12-07T21:35:24
6391bb1	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.7-svn b8d6131600+	28	2018-12-07T07:52:18+01:00
78fd2b1	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.7-svn 29852	22	2018-12-09T21:49:14+01:00	60e963f
f0f2e44	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.7-svn 29852	22	2018-12-09T21:38:26+01:00	652a43d
ca0063b	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.7-svn 29852	27	2018-12-08T07:53:24+01:00	6391bb1
3a13123	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.7-svn 29852	56	2018-12-08T05:04:46+01:00	83c3a72
7bd5114	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.7-svn 29852	24	2018-12-06T19:52:48+01:00	cf4d238
63bff7a	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.7-svn 29852	56	2018-12-06T10:20:12+01:00	831705d
c59dcca	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.7-svn 29852	27	2018-12-06T09:49:18+01:00	a35e9b1
a35e9b1	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.7-svn 29852	28	2018-12-06T06:32:10+01:00

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

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

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness
7ef0062	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	Yogar-CBMC 1.0	17	2017-12-03T05:19 CET (sv-comp)
bac5a84	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.6.1-svn 26773	25	2017-12-01T10:02:37+01:00
6558698	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CBMC	4	2017-12-01T10:33 CET (sv-comp)
e02bc77	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	accf366
5696c3e	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26758M	16	2017-12-01T08:46:19+01:00

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

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