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/mix014_rmo.opt_false-unreach-call.i |
programSHA |
c4afbc558537df276b78df879e3badeb621aaafc146f7d1e5f7ea0eaf56aae8d |
witnessName |
results-verified/depthk.2018-12-05_0936.logfiles/sv-comp19_prop-reachsafety.mix014_rmo.opt_false-unreach-call.i.files/witness.graphml |
witnessSHA |
6d64dc3a1f92a5ae7ee6fc62fef36ddca5a040d3364e6a567aa8c87111515dde |
Information about the Witness from Competition Database
from https://sv-comp.sosy-lab.org/2019/results/witnessInfoByHash/6d64dc3a1f92a5ae7ee6fc62fef36ddca5a040d3364e6a567aa8c87111515dde.json
Key |
Value |
architecture |
32bit |
creationtime |
2018-12-06T00:25:29.974675 |
producer |
DepthK v3.0 |
programfile |
/tmp/vcloud-vcloud-master/worker/working_dir_a400ceb9-66a4-4ee7-936a-68d04380dcd9/sv-benchmarks/c/pthread-wmm/mix014_rmo.opt_false-unreach-call.i |
programhash |
e7acd6c1655158291642621653063d06c424a440 |
sourcecodelang |
C |
specification |
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file |
witnessFileByHash/6d64dc3a1f92a5ae7ee6fc62fef36ddca5a040d3364e6a567aa8c87111515dde.graphml |
witness-sha256 |
6d64dc3a1f92a5ae7ee6fc62fef36ddca5a040d3364e6a567aa8c87111515dde |
witness-size |
4948 |
witness-type |
violation_witness |
Available Results for the Program from Witness Store SV-COMP '24
Trying to find witnesses for program (c4afbc558537df276b78df879e3badeb621aaafc146f7d1e5f7ea0eaf56aae8d, sv-benchmarks/c/pthread-wmm/mix014_rmo.opt_false-unreach-call.i).
Found 0 witnesses for program sv-benchmarks/c/pthread-wmm/mix014_rmo.opt_false-unreach-call.i, c4afbc558537df276b78df879e3badeb621aaafc146f7d1e5f7ea0eaf56aae8d
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/c4afbc558537df276b78df879e3badeb621aaafc146f7d1e5f7ea0eaf56aae8d.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 (c4afbc558537df276b78df879e3badeb621aaafc146f7d1e5f7ea0eaf56aae8d, sv-benchmarks/c/pthread-wmm/mix014_rmo.opt_false-unreach-call.i).
Found 0 witnesses for program sv-benchmarks/c/pthread-wmm/mix014_rmo.opt_false-unreach-call.i, c4afbc558537df276b78df879e3badeb621aaafc146f7d1e5f7ea0eaf56aae8d
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/c4afbc558537df276b78df879e3badeb621aaafc146f7d1e5f7ea0eaf56aae8d.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 (c4afbc558537df276b78df879e3badeb621aaafc146f7d1e5f7ea0eaf56aae8d, sv-benchmarks/c/pthread-wmm/mix014_rmo.opt_false-unreach-call.i).
Found 0 witnesses for program sv-benchmarks/c/pthread-wmm/mix014_rmo.opt_false-unreach-call.i, c4afbc558537df276b78df879e3badeb621aaafc146f7d1e5f7ea0eaf56aae8d
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/c4afbc558537df276b78df879e3badeb621aaafc146f7d1e5f7ea0eaf56aae8d.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 (c4afbc558537df276b78df879e3badeb621aaafc146f7d1e5f7ea0eaf56aae8d, sv-benchmarks/c/pthread-wmm/mix014_rmo.opt_false-unreach-call.i).
Found 0 witnesses for program sv-benchmarks/c/pthread-wmm/mix014_rmo.opt_false-unreach-call.i, c4afbc558537df276b78df879e3badeb621aaafc146f7d1e5f7ea0eaf56aae8d
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/c4afbc558537df276b78df879e3badeb621aaafc146f7d1e5f7ea0eaf56aae8d.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 (c4afbc558537df276b78df879e3badeb621aaafc146f7d1e5f7ea0eaf56aae8d, sv-benchmarks/c/pthread-wmm/mix014_rmo.opt_false-unreach-call.i).
Found 0 witnesses for program sv-benchmarks/c/pthread-wmm/mix014_rmo.opt_false-unreach-call.i, c4afbc558537df276b78df879e3badeb621aaafc146f7d1e5f7ea0eaf56aae8d
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/c4afbc558537df276b78df879e3badeb621aaafc146f7d1e5f7ea0eaf56aae8d.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 (c4afbc558537df276b78df879e3badeb621aaafc146f7d1e5f7ea0eaf56aae8d, sv-benchmarks/c/pthread-wmm/mix014_rmo.opt_false-unreach-call.i).
Found 10 witnesses for program sv-benchmarks/c/pthread-wmm/mix014_rmo.opt_false-unreach-call.i, c4afbc558537df276b78df879e3badeb621aaafc146f7d1e5f7ea0eaf56aae8d
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/c4afbc558537df276b78df879e3badeb621aaafc146f7d1e5f7ea0eaf56aae8d.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
7dbcecf |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
SMACK 1.9.3 |
3 |
2018-12-08T00:30:03 |
|
063ff9f |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn b8d6131600+ |
28 |
2018-12-07T01:39:01+01:00 |
|
04add3f |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
23 |
2018-12-09T21:49:20+01:00 |
04439fe |
59ba80c |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
23 |
2018-12-09T21:38:34+01:00 |
c65a46f |
3408911 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
27 |
2018-12-08T08:16:49+01:00 |
063ff9f |
635d956 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
57 |
2018-12-08T05:00:17+01:00 |
b5dc309 |
25a16dd |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
24 |
2018-12-06T19:52:44+01:00 |
7b597d4 |
cd25ecc |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
57 |
2018-12-06T10:20:31+01:00 |
6d64dc3 |
e29db6b |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
27 |
2018-12-06T09:49:01+01:00 |
b632e97 |
b632e97 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
28 |
2018-12-06T03:45:45+01:00 |
|
Available Results for the Program from Witness Store SV-COMP '18
Trying to find witnesses for program (c4afbc558537df276b78df879e3badeb621aaafc146f7d1e5f7ea0eaf56aae8d, sv-benchmarks/c/pthread-wmm/mix014_rmo.opt_false-unreach-call.i).
Found 5 witnesses for program sv-benchmarks/c/pthread-wmm/mix014_rmo.opt_false-unreach-call.i, c4afbc558537df276b78df879e3badeb621aaafc146f7d1e5f7ea0eaf56aae8d
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/c4afbc558537df276b78df879e3badeb621aaafc146f7d1e5f7ea0eaf56aae8d.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
6cef6d7 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
Yogar-CBMC 1.0 |
17 |
2017-12-03T05:31 CET (sv-comp) |
|
96cd8d2 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.6.1-svn 26773 |
25 |
2017-12-01T09:53:21+01:00 |
|
599e918 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CBMC |
4 |
2017-12-01T09:45 CET (sv-comp) |
|
65fcb14 |
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 |
840c8ec |
1edae04 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.6.1-svn 26758M |
18 |
2017-12-01T08:46:19+01:00 |
|
Available Results for the Program from Witness Store SV-COMP '17
Trying to find witnesses for program (c4afbc558537df276b78df879e3badeb621aaafc146f7d1e5f7ea0eaf56aae8d, sv-benchmarks/c/pthread-wmm/mix014_rmo.opt_false-unreach-call.i).
Found 0 witnesses for program sv-benchmarks/c/pthread-wmm/mix014_rmo.opt_false-unreach-call.i, c4afbc558537df276b78df879e3badeb621aaafc146f7d1e5f7ea0eaf56aae8d
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/c4afbc558537df276b78df879e3badeb621aaafc146f7d1e5f7ea0eaf56aae8d.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |