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/mix011_tso.oepc_false-unreach-call.i |
programSHA |
eaa120845952a8e259d086d1e8bc98fe995ce2446b8b374ff7a83a75c2018198 |
witnessName |
results-verified/depthk.2017-12-01_1024.logfiles/sv-comp18.mix011_tso.oepc_false-unreach-call.i.files/witness.graphml |
witnessSHA |
f8d132dd7ab18019c9e63d6218b91292d622e288c609d02890d5833c72b6f83f |
Information about the Witness from Competition Database
from https://sv-comp.sosy-lab.org/2018/results/witnessInfoByHash/f8d132dd7ab18019c9e63d6218b91292d622e288c609d02890d5833c72b6f83f.json
Key |
Value |
architecture |
32bit |
creationtime |
2017-12-01T12:18 CET (sv-comp) |
memoryModel |
precise |
producer |
ESBMC 3.1 |
program-sha256 |
eaa120845952a8e259d086d1e8bc98fe995ce2446b8b374ff7a83a75c2018198 |
programfile |
/tmp/vcloud-vcloud-master/worker/working_dir_7e1a38c1-11a9-4a7b-b4bd-3f15134feb96/sv-benchmarks/c/pthread-wmm/mix011_tso.oepc_false-unreach-call.i |
programhash |
ef096405536c7180d29d13dd7b74e6910d568689 |
sourcecodelang |
C |
specification |
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file |
witnessFileByHash/f8d132dd7ab18019c9e63d6218b91292d622e288c609d02890d5833c72b6f83f.graphml |
witness-sha256 |
f8d132dd7ab18019c9e63d6218b91292d622e288c609d02890d5833c72b6f83f |
witness-size |
26396 |
witness-type |
violation_witness |
Available Results for the Program from Witness Store SV-COMP '24
Trying to find witnesses for program (eaa120845952a8e259d086d1e8bc98fe995ce2446b8b374ff7a83a75c2018198, sv-benchmarks/c/pthread-wmm/mix011_tso.oepc_false-unreach-call.i).
Found 0 witnesses for program sv-benchmarks/c/pthread-wmm/mix011_tso.oepc_false-unreach-call.i, eaa120845952a8e259d086d1e8bc98fe995ce2446b8b374ff7a83a75c2018198
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/eaa120845952a8e259d086d1e8bc98fe995ce2446b8b374ff7a83a75c2018198.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 (eaa120845952a8e259d086d1e8bc98fe995ce2446b8b374ff7a83a75c2018198, sv-benchmarks/c/pthread-wmm/mix011_tso.oepc_false-unreach-call.i).
Found 0 witnesses for program sv-benchmarks/c/pthread-wmm/mix011_tso.oepc_false-unreach-call.i, eaa120845952a8e259d086d1e8bc98fe995ce2446b8b374ff7a83a75c2018198
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/eaa120845952a8e259d086d1e8bc98fe995ce2446b8b374ff7a83a75c2018198.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 (eaa120845952a8e259d086d1e8bc98fe995ce2446b8b374ff7a83a75c2018198, sv-benchmarks/c/pthread-wmm/mix011_tso.oepc_false-unreach-call.i).
Found 0 witnesses for program sv-benchmarks/c/pthread-wmm/mix011_tso.oepc_false-unreach-call.i, eaa120845952a8e259d086d1e8bc98fe995ce2446b8b374ff7a83a75c2018198
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/eaa120845952a8e259d086d1e8bc98fe995ce2446b8b374ff7a83a75c2018198.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 (eaa120845952a8e259d086d1e8bc98fe995ce2446b8b374ff7a83a75c2018198, sv-benchmarks/c/pthread-wmm/mix011_tso.oepc_false-unreach-call.i).
Found 0 witnesses for program sv-benchmarks/c/pthread-wmm/mix011_tso.oepc_false-unreach-call.i, eaa120845952a8e259d086d1e8bc98fe995ce2446b8b374ff7a83a75c2018198
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/eaa120845952a8e259d086d1e8bc98fe995ce2446b8b374ff7a83a75c2018198.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 (eaa120845952a8e259d086d1e8bc98fe995ce2446b8b374ff7a83a75c2018198, sv-benchmarks/c/pthread-wmm/mix011_tso.oepc_false-unreach-call.i).
Found 0 witnesses for program sv-benchmarks/c/pthread-wmm/mix011_tso.oepc_false-unreach-call.i, eaa120845952a8e259d086d1e8bc98fe995ce2446b8b374ff7a83a75c2018198
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/eaa120845952a8e259d086d1e8bc98fe995ce2446b8b374ff7a83a75c2018198.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 (eaa120845952a8e259d086d1e8bc98fe995ce2446b8b374ff7a83a75c2018198, sv-benchmarks/c/pthread-wmm/mix011_tso.oepc_false-unreach-call.i).
Found 12 witnesses for program sv-benchmarks/c/pthread-wmm/mix011_tso.oepc_false-unreach-call.i, eaa120845952a8e259d086d1e8bc98fe995ce2446b8b374ff7a83a75c2018198
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/eaa120845952a8e259d086d1e8bc98fe995ce2446b8b374ff7a83a75c2018198.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
6f3015d |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
SMACK 1.9.3 |
3 |
2018-12-08T07:24:02 |
|
e262347 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn b8d6131600+ |
29 |
2018-12-06T20:13:25+01:00 |
|
9e6039b |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
26 |
2018-12-09T21:49:36+01:00 |
c86128c |
b145565 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
26 |
2018-12-09T21:38:33+01:00 |
4e48b5d |
03fe545 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
37 |
2018-12-08T08:59:56+01:00 |
e262347 |
e746ff9 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
233 |
2018-12-08T05:03:58+01:00 |
ef4f945 |
f534836 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
27 |
2018-12-06T19:52:37+01:00 |
d2bcc26 |
26e9b08 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
233 |
2018-12-06T10:17:59+01:00 |
1619f6b |
a41497d |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
37 |
2018-12-06T09:49:15+01:00 |
d82af37 |
a8c447b |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
429 |
2018-12-06T09:09:58+01:00 |
1b45a13 |
d82af37 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
29 |
2018-12-05T11:47:27+01:00 |
|
20f9883 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
34 |
2018-12-10T10:50:05+01:00 |
dedb557 |
Available Results for the Program from Witness Store SV-COMP '18
Trying to find witnesses for program (eaa120845952a8e259d086d1e8bc98fe995ce2446b8b374ff7a83a75c2018198, sv-benchmarks/c/pthread-wmm/mix011_tso.oepc_false-unreach-call.i).
Found 6 witnesses for program sv-benchmarks/c/pthread-wmm/mix011_tso.oepc_false-unreach-call.i, eaa120845952a8e259d086d1e8bc98fe995ce2446b8b374ff7a83a75c2018198
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/eaa120845952a8e259d086d1e8bc98fe995ce2446b8b374ff7a83a75c2018198.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
b866e20 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
Yogar-CBMC 1.0 |
16 |
2017-12-03T05:17 CET (sv-comp) |
|
f8d132d |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
ESBMC 3.1 |
26 |
2017-12-01T12:18 CET (sv-comp) |
|
6c0e100 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.6.1-svn 26773 |
24 |
2017-12-01T10:27:25+01:00 |
|
1b45a13 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CBMC |
4 |
2017-12-01T09:48 CET (sv-comp) |
|
f9edfd4 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.6.1-svn 26773 |
35 |
2017-12-01T08:48:27+01:00 |
4b9ba34 |
b8601ab |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.6.1-svn 26758M |
100 |
2017-12-01T08:46:21+01:00 |
|
Available Results for the Program from Witness Store SV-COMP '17
Trying to find witnesses for program (eaa120845952a8e259d086d1e8bc98fe995ce2446b8b374ff7a83a75c2018198, sv-benchmarks/c/pthread-wmm/mix011_tso.oepc_false-unreach-call.i).
Found 0 witnesses for program sv-benchmarks/c/pthread-wmm/mix011_tso.oepc_false-unreach-call.i, eaa120845952a8e259d086d1e8bc98fe995ce2446b8b374ff7a83a75c2018198
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/eaa120845952a8e259d086d1e8bc98fe995ce2446b8b374ff7a83a75c2018198.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |