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/mix012_tso.oepc_false-unreach-call.i |
programSHA | e3e0d8eb76e617ad36ee563cb3582a703b06975261a62fb1099717ac1f61bffb |
witnessName | results-verified/cpa-seq.2018-12-05_0546.logfiles/sv-comp19_prop-reachsafety.mix012_tso.oepc_false-unreach-call.i.files/witness.graphml |
witnessSHA | 83012d7ef63c56a79b75c7fc34bc359567e3628ceee02c728f9ef750e426fe41 |
Key | Value |
architecture | 32bit |
creationtime | 2018-12-05T19:25:52+01:00 |
producer | CPAchecker 1.7-svn 29852 |
program-sha256 | e3e0d8eb76e617ad36ee563cb3582a703b06975261a62fb1099717ac1f61bffb |
programfile | ../../sv-benchmarks/c/pthread-wmm/mix012_tso.oepc_false-unreach-call.i |
programhash | e3e0d8eb76e617ad36ee563cb3582a703b06975261a62fb1099717ac1f61bffb |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/83012d7ef63c56a79b75c7fc34bc359567e3628ceee02c728f9ef750e426fe41.graphml |
witness-sha256 | 83012d7ef63c56a79b75c7fc34bc359567e3628ceee02c728f9ef750e426fe41 |
witness-size | 23430 |
witness-type | violation_witness |
This witness was created for this program (cf. table above, e3e0d8eb76e617ad36ee563cb3582a703b06975261a62fb1099717ac1f61bffb).
Found 0 witnesses for program sv-benchmarks/c/pthread-wmm/mix012_tso.oepc_false-unreach-call.i, e3e0d8eb76e617ad36ee563cb3582a703b06975261a62fb1099717ac1f61bffb
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/e3e0d8eb76e617ad36ee563cb3582a703b06975261a62fb1099717ac1f61bffb.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/mix012_tso.oepc_false-unreach-call.i, e3e0d8eb76e617ad36ee563cb3582a703b06975261a62fb1099717ac1f61bffb
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/e3e0d8eb76e617ad36ee563cb3582a703b06975261a62fb1099717ac1f61bffb.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/mix012_tso.oepc_false-unreach-call.i, e3e0d8eb76e617ad36ee563cb3582a703b06975261a62fb1099717ac1f61bffb
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/e3e0d8eb76e617ad36ee563cb3582a703b06975261a62fb1099717ac1f61bffb.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/mix012_tso.oepc_false-unreach-call.i, e3e0d8eb76e617ad36ee563cb3582a703b06975261a62fb1099717ac1f61bffb
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/e3e0d8eb76e617ad36ee563cb3582a703b06975261a62fb1099717ac1f61bffb.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/mix012_tso.oepc_false-unreach-call.i, e3e0d8eb76e617ad36ee563cb3582a703b06975261a62fb1099717ac1f61bffb
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/e3e0d8eb76e617ad36ee563cb3582a703b06975261a62fb1099717ac1f61bffb.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 16 witnesses for program sv-benchmarks/c/pthread-wmm/mix012_tso.oepc_false-unreach-call.i, e3e0d8eb76e617ad36ee563cb3582a703b06975261a62fb1099717ac1f61bffb
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/e3e0d8eb76e617ad36ee563cb3582a703b06975261a62fb1099717ac1f61bffb.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
1ae6f12 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | SMACK 1.9.3 | 3 | 2018-12-08T04:58:45 | ||
9e58b7b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 23 | 2018-12-07T01:15:32+01:00 | ||
16d1aa0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 432 | 2018-12-10T10:49:05+01:00 | 926ea6e | |
0a38028 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 22 | 2018-12-09T21:48:51+01:00 | 14fcb2f | |
f6e9fe0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 22 | 2018-12-09T21:38:26+01:00 | a2137d7 | |
d8eb471 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 24 | 2018-12-08T08:36:51+01:00 | 9e58b7b | |
179cfa5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 94 | 2018-12-08T04:58:49+01:00 | 3c4e8ce | |
3aa806e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 432 | 2018-12-08T04:21:57+01:00 | 926ea6e | |
cc8ac2f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 22 | 2018-12-06T19:53:43+01:00 | f795fd4 | |
0777d3a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 94 | 2018-12-06T10:20:03+01:00 | 6fc4de0 | |
151b1ef | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 24 | 2018-12-06T09:49:12+01:00 | 83012d7 | |
a144a5b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 146 | 2018-12-06T09:10:49+01:00 | d396f8e | |
83012d7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 23 | 2018-12-05T19:25:52+01:00 | ||
38145a4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 16 | 2018-12-09T20:53:58+01:00 | 140105f | |
229f7f0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 16 | 2018-12-09T20:34:04+01:00 | ed9241f | |
8c9ae5c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 16 | 2018-12-08T22:09:44+01:00 | 1ae6f12 |
Found 8 witnesses for program sv-benchmarks/c/pthread-wmm/mix012_tso.oepc_false-unreach-call.i, e3e0d8eb76e617ad36ee563cb3582a703b06975261a62fb1099717ac1f61bffb
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/e3e0d8eb76e617ad36ee563cb3582a703b06975261a62fb1099717ac1f61bffb.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
9583ea6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Yogar-CBMC 1.0 | 14 | 2017-12-03T05:53 CET (sv-comp) | ||
5fba68c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 kind | 4 | 2017-12-02T15:04:27.786230 | ||
6cf0148 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 incr | 4 | 2017-12-02T04:19:37.738864 | ||
c5ab1b0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 21 | 2017-12-01T11:23 CET (sv-comp) | ||
45e37f0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 20 | 2017-12-01T10:02:45+01:00 | ||
d396f8e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CBMC | 3 | 2017-12-01T09:42 CET (sv-comp) | ||
26a3aac | 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 | ecd892f | |
1a7d616 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26758M | 12 | 2017-12-01T08:46:35+01:00 |
Found 0 witnesses for program sv-benchmarks/c/pthread-wmm/mix012_tso.oepc_false-unreach-call.i, e3e0d8eb76e617ad36ee563cb3582a703b06975261a62fb1099717ac1f61bffb
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/e3e0d8eb76e617ad36ee563cb3582a703b06975261a62fb1099717ac1f61bffb.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |