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).
Key | Value |
programName | sv-benchmarks/c/pthread-wmm/mix024_tso.opt_false-unreach-call.i |
programSHA | 6cc757808a796c030477ca4387a661811e720a4b62906f94a08e3785496a3b5f |
witnessName | results-validated/cpa-seq-validate-violation-witnesses-divine-explicit.2018-12-10_1048.logfiles/sv-comp19_prop-reachsafety.mix024_tso.opt_false-unreach-call.i.files/witness.graphml |
witnessSHA | 8fbb5c9bc029c1836491f52f9e28ed2dfc2317768baf03c0858e3d7cfee52837 |
Key | Value |
architecture | 32bit |
creationtime | 2018-12-10T10:50:07+01:00 |
inputwitnesshash | 0a5f109d5b35cc683deadd548d0d678e4f0c6077139dabaa5568ae27ec728aae |
producer | CPAchecker 1.7-svn 29852 |
program-sha256 | 6cc757808a796c030477ca4387a661811e720a4b62906f94a08e3785496a3b5f |
programfile | ../../sv-benchmarks/c/pthread-wmm/mix024_tso.opt_false-unreach-call.i |
programhash | 6cc757808a796c030477ca4387a661811e720a4b62906f94a08e3785496a3b5f |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/8fbb5c9bc029c1836491f52f9e28ed2dfc2317768baf03c0858e3d7cfee52837.graphml |
witness-sha256 | 8fbb5c9bc029c1836491f52f9e28ed2dfc2317768baf03c0858e3d7cfee52837 |
witness-size | 16973 |
witness-type | correctness_witness |
This witness was created for this program (cf. table above, 6cc757808a796c030477ca4387a661811e720a4b62906f94a08e3785496a3b5f).
Found 0 witnesses for program sv-benchmarks/c/pthread-wmm/mix024_tso.opt_false-unreach-call.i, 6cc757808a796c030477ca4387a661811e720a4b62906f94a08e3785496a3b5f
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/6cc757808a796c030477ca4387a661811e720a4b62906f94a08e3785496a3b5f.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/mix024_tso.opt_false-unreach-call.i, 6cc757808a796c030477ca4387a661811e720a4b62906f94a08e3785496a3b5f
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/6cc757808a796c030477ca4387a661811e720a4b62906f94a08e3785496a3b5f.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/mix024_tso.opt_false-unreach-call.i, 6cc757808a796c030477ca4387a661811e720a4b62906f94a08e3785496a3b5f
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/6cc757808a796c030477ca4387a661811e720a4b62906f94a08e3785496a3b5f.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/mix024_tso.opt_false-unreach-call.i, 6cc757808a796c030477ca4387a661811e720a4b62906f94a08e3785496a3b5f
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/6cc757808a796c030477ca4387a661811e720a4b62906f94a08e3785496a3b5f.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/mix024_tso.opt_false-unreach-call.i, 6cc757808a796c030477ca4387a661811e720a4b62906f94a08e3785496a3b5f
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/6cc757808a796c030477ca4387a661811e720a4b62906f94a08e3785496a3b5f.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 12 witnesses for program sv-benchmarks/c/pthread-wmm/mix024_tso.opt_false-unreach-call.i, 6cc757808a796c030477ca4387a661811e720a4b62906f94a08e3785496a3b5f
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/6cc757808a796c030477ca4387a661811e720a4b62906f94a08e3785496a3b5f.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
9a68a7c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | SMACK 1.9.3 | 3 | 2018-12-08T18:13:17 | ||
5997f07 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 29 | 2018-12-07T14:33:23+01:00 | ||
deea365 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 26 | 2018-12-09T21:49:31+01:00 | 7a13211 | |
eeac3b1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 26 | 2018-12-09T21:38:38+01:00 | 21b0b13 | |
b0404ee | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 33 | 2018-12-08T09:07:41+01:00 | 5997f07 | |
7e561d2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 342 | 2018-12-08T05:06:19+01:00 | 67de626 | |
87d9c4d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 26 | 2018-12-06T19:52:59+01:00 | 53f2fd6 | |
e1c2b37 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 342 | 2018-12-06T10:19:47+01:00 | 5a19e5e | |
5c2f046 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 33 | 2018-12-06T09:48:46+01:00 | d50dd1d | |
d50dd1d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 29 | 2018-12-05T13:17:46+01:00 | ||
8fbb5c9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 17 | 2018-12-10T10:50:07+01:00 | 0a5f109 | |
04ae353 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 17 | 2018-12-06T09:17:15+01:00 | a92fa76 |
Found 6 witnesses for program sv-benchmarks/c/pthread-wmm/mix024_tso.opt_false-unreach-call.i, 6cc757808a796c030477ca4387a661811e720a4b62906f94a08e3785496a3b5f
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/6cc757808a796c030477ca4387a661811e720a4b62906f94a08e3785496a3b5f.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
6c582a0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Yogar-CBMC 1.0 | 16 | 2017-12-03T05:57 CET (sv-comp) | ||
58afc6e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 26 | 2017-12-01T10:59 CET (sv-comp) | ||
03982cf | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 25 | 2017-12-01T09:42:34+01:00 | ||
a92fa76 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CBMC | 4 | 2017-12-01T10:07 CET (sv-comp) | ||
ef4e342 | 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 | d12b9de | |
fbb2afd | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26758M | 16 | 2017-12-01T08:46:40+01:00 |
Found 0 witnesses for program sv-benchmarks/c/pthread-wmm/mix024_tso.opt_false-unreach-call.i, 6cc757808a796c030477ca4387a661811e720a4b62906f94a08e3785496a3b5f
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/6cc757808a796c030477ca4387a661811e720a4b62906f94a08e3785496a3b5f.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |