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).
Found 0 witnesses for program sv-benchmarks/c/pthread-wmm/mix000_pso.oepc_false-unreach-call.i, bc8a6cb30dffdc2b3a1ca41fb68fad516af4ea6c19ba00b4be059fca888d3e29
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/bc8a6cb30dffdc2b3a1ca41fb68fad516af4ea6c19ba00b4be059fca888d3e29.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/pthread-wmm/mix000_pso.oepc_false-unreach-call.i, bc8a6cb30dffdc2b3a1ca41fb68fad516af4ea6c19ba00b4be059fca888d3e29
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/bc8a6cb30dffdc2b3a1ca41fb68fad516af4ea6c19ba00b4be059fca888d3e29.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/pthread-wmm/mix000_pso.oepc_false-unreach-call.i, bc8a6cb30dffdc2b3a1ca41fb68fad516af4ea6c19ba00b4be059fca888d3e29
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/bc8a6cb30dffdc2b3a1ca41fb68fad516af4ea6c19ba00b4be059fca888d3e29.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/pthread-wmm/mix000_pso.oepc_false-unreach-call.i, bc8a6cb30dffdc2b3a1ca41fb68fad516af4ea6c19ba00b4be059fca888d3e29
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/bc8a6cb30dffdc2b3a1ca41fb68fad516af4ea6c19ba00b4be059fca888d3e29.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/pthread-wmm/mix000_pso.oepc_false-unreach-call.i, bc8a6cb30dffdc2b3a1ca41fb68fad516af4ea6c19ba00b4be059fca888d3e29
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/bc8a6cb30dffdc2b3a1ca41fb68fad516af4ea6c19ba00b4be059fca888d3e29.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 15 witnesses for program sv-benchmarks/c/pthread-wmm/mix000_pso.oepc_false-unreach-call.i, bc8a6cb30dffdc2b3a1ca41fb68fad516af4ea6c19ba00b4be059fca888d3e29
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/bc8a6cb30dffdc2b3a1ca41fb68fad516af4ea6c19ba00b4be059fca888d3e29.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
37fe776 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | SMACK 1.9.3 | 3 | 2018-12-08T17:02:31 | ||
b993c7a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 29 | 2018-12-07T20:20:12+01:00 | ||
8e9de9b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 27 | 2018-12-09T21:49:38+01:00 | e28694c | |
305b81d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 27 | 2018-12-09T21:38:36+01:00 | a34deff | |
3d78e2f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 28 | 2018-12-08T08:43:21+01:00 | b993c7a | |
be03994 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 60 | 2018-12-08T05:00:22+01:00 | 943f05f | |
093c16c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 27 | 2018-12-06T19:53:11+01:00 | cb854f0 | |
c850ede | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 60 | 2018-12-06T10:13:34+01:00 | 0ad88fc | |
a4bb4be | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 28 | 2018-12-06T09:49:19+01:00 | d5960ba | |
36e04e4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 235 | 2018-12-06T09:09:40+01:00 | 35a7c94 | |
d5960ba | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 29 | 2018-12-05T10:35:12+01:00 | ||
904b799 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 34 | 2018-12-09T20:54:33+01:00 | 76304f1 | |
5313599 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 34 | 2018-12-09T20:37:59+01:00 | 87d2b6a | |
a31b775 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 34 | 2018-12-08T22:08:55+01:00 | 37fe776 | |
a846966 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 34 | 2018-12-08T04:00:52+01:00 | 55c1def |
Found 8 witnesses for program sv-benchmarks/c/pthread-wmm/mix000_pso.oepc_false-unreach-call.i, bc8a6cb30dffdc2b3a1ca41fb68fad516af4ea6c19ba00b4be059fca888d3e29
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/bc8a6cb30dffdc2b3a1ca41fb68fad516af4ea6c19ba00b4be059fca888d3e29.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
3388646 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Yogar-CBMC 1.0 | 16 | 2017-12-03T06:02 CET (sv-comp) | ||
63bfffa | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 kind | 5 | 2017-12-02T15:34:11.602002 | ||
22e9c70 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 incr | 5 | 2017-12-02T04:15:05.733512 | ||
423a255 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 24 | 2017-12-01T12:28 CET (sv-comp) | ||
201c13b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 25 | 2017-12-01T09:32:44+01:00 | ||
35a7c94 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CBMC | 3 | 2017-12-01T09:20 CET (sv-comp) | ||
516488b | 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 | 9a71a48 | |
06cd9a6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26758M | 14 | 2017-12-01T08:46:21+01:00 |
Found 0 witnesses for program sv-benchmarks/c/pthread-wmm/mix000_pso.oepc_false-unreach-call.i, bc8a6cb30dffdc2b3a1ca41fb68fad516af4ea6c19ba00b4be059fca888d3e29
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/bc8a6cb30dffdc2b3a1ca41fb68fad516af4ea6c19ba00b4be059fca888d3e29.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |