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/mix027_tso.opt_false-unreach-call.i |
programSHA | 0492714f4b97327e7311ad7fd1716ee7a9f9ffc77deccf49b63e069a3ce1d37c |
witnessName | results-validated/cpa-seq-validate-violation-witnesses-pesco.2018-12-08_0739.logfiles/sv-comp19_prop-reachsafety.mix027_tso.opt_false-unreach-call.i.files/witness.graphml |
witnessSHA | deb2e576cd40abd9eb08b9043625785294333972329a7c2e101e25120e9f40d7 |
Key | Value |
architecture | 32bit |
creationtime | 2018-12-08T07:56:07+01:00 |
inputwitnesshash | fa3d9a415aa7f063526337a5a85eaaac25d7477dbd945e646b9d74677c2c87fe |
producer | CPAchecker 1.7-svn 29852 |
program-sha256 | 0492714f4b97327e7311ad7fd1716ee7a9f9ffc77deccf49b63e069a3ce1d37c |
programfile | ../../sv-benchmarks/c/pthread-wmm/mix027_tso.opt_false-unreach-call.i |
programhash | 0492714f4b97327e7311ad7fd1716ee7a9f9ffc77deccf49b63e069a3ce1d37c |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/deb2e576cd40abd9eb08b9043625785294333972329a7c2e101e25120e9f40d7.graphml |
witness-sha256 | deb2e576cd40abd9eb08b9043625785294333972329a7c2e101e25120e9f40d7 |
witness-size | 45816 |
witness-type | violation_witness |
This witness was created for this program (cf. table above, 0492714f4b97327e7311ad7fd1716ee7a9f9ffc77deccf49b63e069a3ce1d37c).
Found 0 witnesses for program sv-benchmarks/c/pthread-wmm/mix027_tso.opt_false-unreach-call.i, 0492714f4b97327e7311ad7fd1716ee7a9f9ffc77deccf49b63e069a3ce1d37c
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/0492714f4b97327e7311ad7fd1716ee7a9f9ffc77deccf49b63e069a3ce1d37c.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/mix027_tso.opt_false-unreach-call.i, 0492714f4b97327e7311ad7fd1716ee7a9f9ffc77deccf49b63e069a3ce1d37c
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/0492714f4b97327e7311ad7fd1716ee7a9f9ffc77deccf49b63e069a3ce1d37c.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/mix027_tso.opt_false-unreach-call.i, 0492714f4b97327e7311ad7fd1716ee7a9f9ffc77deccf49b63e069a3ce1d37c
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/0492714f4b97327e7311ad7fd1716ee7a9f9ffc77deccf49b63e069a3ce1d37c.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/mix027_tso.opt_false-unreach-call.i, 0492714f4b97327e7311ad7fd1716ee7a9f9ffc77deccf49b63e069a3ce1d37c
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/0492714f4b97327e7311ad7fd1716ee7a9f9ffc77deccf49b63e069a3ce1d37c.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/mix027_tso.opt_false-unreach-call.i, 0492714f4b97327e7311ad7fd1716ee7a9f9ffc77deccf49b63e069a3ce1d37c
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/0492714f4b97327e7311ad7fd1716ee7a9f9ffc77deccf49b63e069a3ce1d37c.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 10 witnesses for program sv-benchmarks/c/pthread-wmm/mix027_tso.opt_false-unreach-call.i, 0492714f4b97327e7311ad7fd1716ee7a9f9ffc77deccf49b63e069a3ce1d37c
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/0492714f4b97327e7311ad7fd1716ee7a9f9ffc77deccf49b63e069a3ce1d37c.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
6bf6262 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | SMACK 1.9.3 | 3 | 2018-12-08T06:15:05 | ||
fa3d9a4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 35 | 2018-12-06T12:55:36+01:00 | ||
43ef350 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 30 | 2018-12-09T21:49:07+01:00 | 26fc12f | |
cfd291b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 29 | 2018-12-09T21:38:32+01:00 | 190d146 | |
deb2e57 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 46 | 2018-12-08T07:56:07+01:00 | fa3d9a4 | |
d051e6d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 961 | 2018-12-08T05:06:34+01:00 | 7c3eb7b | |
1197404 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 31 | 2018-12-06T19:54:06+01:00 | 7587c64 | |
0f2c695 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 46 | 2018-12-06T09:49:30+01:00 | c268d7c | |
c268d7c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 35 | 2018-12-06T00:32:51+01:00 | ||
f3bcb47 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 34 | 2018-12-06T10:19:54+01:00 | 5abaeac |
Found 5 witnesses for program sv-benchmarks/c/pthread-wmm/mix027_tso.opt_false-unreach-call.i, 0492714f4b97327e7311ad7fd1716ee7a9f9ffc77deccf49b63e069a3ce1d37c
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/0492714f4b97327e7311ad7fd1716ee7a9f9ffc77deccf49b63e069a3ce1d37c.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
1bbc198 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Yogar-CBMC 1.0 | 18 | 2017-12-03T06:14 CET (sv-comp) | ||
da0b2c6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 30 | 2017-12-01T10:09:54+01:00 | ||
91f241c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CBMC | 4 | 2017-12-01T10:14 CET (sv-comp) | ||
43b1dd1 | 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 | e606d58 | |
a02c1fe | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26758M | 100 | 2017-12-01T08:46:27+01:00 |
Found 0 witnesses for program sv-benchmarks/c/pthread-wmm/mix027_tso.opt_false-unreach-call.i, 0492714f4b97327e7311ad7fd1716ee7a9f9ffc77deccf49b63e069a3ce1d37c
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/0492714f4b97327e7311ad7fd1716ee7a9f9ffc77deccf49b63e069a3ce1d37c.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |