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
Input Given to this Service about the Witness (URL Query)
Key |
Value |
programName |
sv-benchmarks/c/pthread-wmm/mix023_tso.oepc_false-unreach-call.i |
programSHA |
178b42d878441679f1ca307e77e6a5deacfd6c8d31ad36e31295b815d3a36f3b |
witnessName |
results-verified/yogar-cbmc-parallel.2018-12-09_2127.logfiles/sv-comp19_prop-reachsafety.mix023_tso.oepc_false-unreach-call.i.files/witness.graphml |
witnessSHA |
9eae03c51aa4f1878f38b1b7675f9a9e008c4ac09854a5f2ea76fc23d0255740 |
Information about the Witness from Competition Database
from https://sv-comp.sosy-lab.org/2019/results/witnessInfoByHash/9eae03c51aa4f1878f38b1b7675f9a9e008c4ac09854a5f2ea76fc23d0255740.json
Key |
Value |
architecture |
32bit |
creationtime |
2018-12-09T21:27 CET (sv-comp) |
producer |
Yogar-CBMC-Parallel |
programfile |
yogar-tmp/temp_file2.i |
programhash |
75d32481ce29406801ceee20a82ca92a57f54b26 |
sourcecodelang |
C |
specification |
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file |
witnessFileByHash/9eae03c51aa4f1878f38b1b7675f9a9e008c4ac09854a5f2ea76fc23d0255740.graphml |
witness-sha256 |
9eae03c51aa4f1878f38b1b7675f9a9e008c4ac09854a5f2ea76fc23d0255740 |
witness-size |
28752 |
witness-type |
violation_witness |
Available Results for the Program from Witness Store SV-COMP '24
Trying to find witnesses for program (178b42d878441679f1ca307e77e6a5deacfd6c8d31ad36e31295b815d3a36f3b, sv-benchmarks/c/pthread-wmm/mix023_tso.oepc_false-unreach-call.i).
Found 0 witnesses for program sv-benchmarks/c/pthread-wmm/mix023_tso.oepc_false-unreach-call.i, 178b42d878441679f1ca307e77e6a5deacfd6c8d31ad36e31295b815d3a36f3b
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/178b42d878441679f1ca307e77e6a5deacfd6c8d31ad36e31295b815d3a36f3b.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
Available Results for the Program from Witness Store SV-COMP '23
Trying to find witnesses for program (178b42d878441679f1ca307e77e6a5deacfd6c8d31ad36e31295b815d3a36f3b, sv-benchmarks/c/pthread-wmm/mix023_tso.oepc_false-unreach-call.i).
Found 0 witnesses for program sv-benchmarks/c/pthread-wmm/mix023_tso.oepc_false-unreach-call.i, 178b42d878441679f1ca307e77e6a5deacfd6c8d31ad36e31295b815d3a36f3b
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/178b42d878441679f1ca307e77e6a5deacfd6c8d31ad36e31295b815d3a36f3b.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
Available Results for the Program from Witness Store SV-COMP '22
Trying to find witnesses for program (178b42d878441679f1ca307e77e6a5deacfd6c8d31ad36e31295b815d3a36f3b, sv-benchmarks/c/pthread-wmm/mix023_tso.oepc_false-unreach-call.i).
Found 0 witnesses for program sv-benchmarks/c/pthread-wmm/mix023_tso.oepc_false-unreach-call.i, 178b42d878441679f1ca307e77e6a5deacfd6c8d31ad36e31295b815d3a36f3b
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/178b42d878441679f1ca307e77e6a5deacfd6c8d31ad36e31295b815d3a36f3b.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
Available Results for the Program from Witness Store SV-COMP '21
Trying to find witnesses for program (178b42d878441679f1ca307e77e6a5deacfd6c8d31ad36e31295b815d3a36f3b, sv-benchmarks/c/pthread-wmm/mix023_tso.oepc_false-unreach-call.i).
Found 0 witnesses for program sv-benchmarks/c/pthread-wmm/mix023_tso.oepc_false-unreach-call.i, 178b42d878441679f1ca307e77e6a5deacfd6c8d31ad36e31295b815d3a36f3b
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/178b42d878441679f1ca307e77e6a5deacfd6c8d31ad36e31295b815d3a36f3b.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
Available Results for the Program from Witness Store SV-COMP '20
Trying to find witnesses for program (178b42d878441679f1ca307e77e6a5deacfd6c8d31ad36e31295b815d3a36f3b, sv-benchmarks/c/pthread-wmm/mix023_tso.oepc_false-unreach-call.i).
Found 0 witnesses for program sv-benchmarks/c/pthread-wmm/mix023_tso.oepc_false-unreach-call.i, 178b42d878441679f1ca307e77e6a5deacfd6c8d31ad36e31295b815d3a36f3b
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/178b42d878441679f1ca307e77e6a5deacfd6c8d31ad36e31295b815d3a36f3b.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
Available Results for the Program from Witness Store SV-COMP '19
Trying to find witnesses for program (178b42d878441679f1ca307e77e6a5deacfd6c8d31ad36e31295b815d3a36f3b, sv-benchmarks/c/pthread-wmm/mix023_tso.oepc_false-unreach-call.i).
Found 11 witnesses for program sv-benchmarks/c/pthread-wmm/mix023_tso.oepc_false-unreach-call.i, 178b42d878441679f1ca307e77e6a5deacfd6c8d31ad36e31295b815d3a36f3b
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/178b42d878441679f1ca307e77e6a5deacfd6c8d31ad36e31295b815d3a36f3b.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
d5c0c99 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
SMACK 1.9.3 |
3 |
2018-12-08T05:37:03 |
|
bfa9d75 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
54 |
2018-12-09T21:48:01+01:00 |
9eae03c |
0b3cf2d |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
56 |
2018-12-09T21:38:34+01:00 |
8028a08 |
82d56df |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
57 |
2018-12-06T19:53:13+01:00 |
7902054 |
656ced8 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn b8d6131600+ |
103 |
2018-12-07T10:08:14+01:00 |
|
2e012b6 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
103 |
2018-12-08T07:43:49+01:00 |
656ced8 |
89be692 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
103 |
2018-12-08T05:06:16+01:00 |
3a236c6 |
a7bc201 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
103 |
2018-12-06T10:16:24+01:00 |
874628f |
92ebabc |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
103 |
2018-12-06T09:49:04+01:00 |
1d68c94 |
c42f2aa |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
103 |
2018-12-06T09:20:02+01:00 |
4b4b5ed |
1d68c94 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
103 |
2018-12-05T15:54:47+01:00 |
|
Available Results for the Program from Witness Store SV-COMP '18
Trying to find witnesses for program (178b42d878441679f1ca307e77e6a5deacfd6c8d31ad36e31295b815d3a36f3b, sv-benchmarks/c/pthread-wmm/mix023_tso.oepc_false-unreach-call.i).
Found 4 witnesses for program sv-benchmarks/c/pthread-wmm/mix023_tso.oepc_false-unreach-call.i, 178b42d878441679f1ca307e77e6a5deacfd6c8d31ad36e31295b815d3a36f3b
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/178b42d878441679f1ca307e77e6a5deacfd6c8d31ad36e31295b815d3a36f3b.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
44284c7 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
Yogar-CBMC 1.0 |
29 |
2017-12-03T05:53 CET (sv-comp) |
|
4b4b5ed |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CBMC |
4 |
2017-12-01T10:07 CET (sv-comp) |
|
fd4f3d6 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.6.1-svn 26773 |
104 |
2017-12-01T08:48:24+01:00 |
c6fd082 |
c03c582 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.6.1-svn 26758M |
186 |
2017-12-01T08:46:19+01:00 |
|
Available Results for the Program from Witness Store SV-COMP '17
Trying to find witnesses for program (178b42d878441679f1ca307e77e6a5deacfd6c8d31ad36e31295b815d3a36f3b, sv-benchmarks/c/pthread-wmm/mix023_tso.oepc_false-unreach-call.i).
Found 0 witnesses for program sv-benchmarks/c/pthread-wmm/mix023_tso.oepc_false-unreach-call.i, 178b42d878441679f1ca307e77e6a5deacfd6c8d31ad36e31295b815d3a36f3b
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/178b42d878441679f1ca307e77e6a5deacfd6c8d31ad36e31295b815d3a36f3b.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |