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/mix034_rmo.opt_false-unreach-call.i, e24b0659761cdfe089f964f2e1808759484c430af7440f604cb037f2fb03d242
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/e24b0659761cdfe089f964f2e1808759484c430af7440f604cb037f2fb03d242.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/mix034_rmo.opt_false-unreach-call.i, e24b0659761cdfe089f964f2e1808759484c430af7440f604cb037f2fb03d242
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/e24b0659761cdfe089f964f2e1808759484c430af7440f604cb037f2fb03d242.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/mix034_rmo.opt_false-unreach-call.i, e24b0659761cdfe089f964f2e1808759484c430af7440f604cb037f2fb03d242
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/e24b0659761cdfe089f964f2e1808759484c430af7440f604cb037f2fb03d242.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/mix034_rmo.opt_false-unreach-call.i, e24b0659761cdfe089f964f2e1808759484c430af7440f604cb037f2fb03d242
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/e24b0659761cdfe089f964f2e1808759484c430af7440f604cb037f2fb03d242.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/mix034_rmo.opt_false-unreach-call.i, e24b0659761cdfe089f964f2e1808759484c430af7440f604cb037f2fb03d242
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/e24b0659761cdfe089f964f2e1808759484c430af7440f604cb037f2fb03d242.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/mix034_rmo.opt_false-unreach-call.i, e24b0659761cdfe089f964f2e1808759484c430af7440f604cb037f2fb03d242
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/e24b0659761cdfe089f964f2e1808759484c430af7440f604cb037f2fb03d242.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
c6ce1d1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | SMACK 1.9.3 | 3 | 2018-12-08T13:21:27 | ||
6834e8f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 23 | 2018-12-08T01:20:59+01:00 | ||
f6e0a50 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 432 | 2018-12-10T10:48:59+01:00 | 1f5277e | |
fca7e78 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 22 | 2018-12-09T21:47:58+01:00 | 0bdb25e | |
1b14e5c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 21 | 2018-12-09T21:38:36+01:00 | 6d1f411 | |
7719de8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 24 | 2018-12-08T07:43:53+01:00 | 6834e8f | |
4994ebd | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 94 | 2018-12-08T05:06:14+01:00 | 319e5f3 | |
d10a51f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 432 | 2018-12-08T04:36:22+01:00 | 1f5277e | |
0b756e9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 22 | 2018-12-06T19:53:21+01:00 | 8993db7 | |
0b5b980 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 94 | 2018-12-06T10:10:04+01:00 | 8c1ec34 | |
22da955 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 24 | 2018-12-06T09:49:04+01:00 | 3514d56 | |
d276cd1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 146 | 2018-12-06T09:20:40+01:00 | a7353a4 | |
3514d56 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 23 | 2018-12-05T23:47:32+01:00 | ||
876a029 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 16 | 2018-12-09T20:38:42+01:00 | 3c3a501 | |
4581e23 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 16 | 2018-12-08T22:08:14+01:00 | c6ce1d1 |
Found 8 witnesses for program sv-benchmarks/c/pthread-wmm/mix034_rmo.opt_false-unreach-call.i, e24b0659761cdfe089f964f2e1808759484c430af7440f604cb037f2fb03d242
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/e24b0659761cdfe089f964f2e1808759484c430af7440f604cb037f2fb03d242.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
2ae719c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Yogar-CBMC 1.0 | 14 | 2017-12-03T05:55 CET (sv-comp) | ||
2e321ff | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 kind | 4 | 2017-12-02T14:45:39.466180 | ||
6bce107 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 incr | 4 | 2017-12-02T00:59:19.847353 | ||
4197fd4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 21 | 2017-12-01T10:32 CET (sv-comp) | ||
034d114 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 20 | 2017-12-01T09:56:34+01:00 | ||
a7353a4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CBMC | 3 | 2017-12-01T09:20 CET (sv-comp) | ||
942711e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 17 | 2017-12-01T08:48:24+01:00 | ddeb049 | |
b90877e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26758M | 12 | 2017-12-01T08:46:34+01:00 |
Found 0 witnesses for program sv-benchmarks/c/pthread-wmm/mix034_rmo.opt_false-unreach-call.i, e24b0659761cdfe089f964f2e1808759484c430af7440f604cb037f2fb03d242
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/e24b0659761cdfe089f964f2e1808759484c430af7440f604cb037f2fb03d242.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |