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/mix009_pso.oepc_false-unreach-call.i |
programSHA | 757f7e1bd660db5c5d113471b435cf4c9efc154b6e4f7b9526db70d78dba40df |
witnessName | results-validated/cpa-seq-validate-violation-witnesses-cpa-seq.2018-12-06_0944.logfiles/sv-comp19_prop-reachsafety.mix009_pso.oepc_false-unreach-call.i.files/witness.graphml |
witnessSHA | 8bd08a64a5f8e2162b4d65089394309faf33ae93de1b41fa108bbb1d3037ec82 |
Key | Value |
architecture | 32bit |
creationtime | 2018-12-06T09:48:38+01:00 |
inputwitnesshash | cc0a72d28903057b13cf614bb32a86b7f652fc52bf6fea91c4146bf23bfd2225 |
producer | CPAchecker 1.7-svn 29852 |
program-sha256 | 757f7e1bd660db5c5d113471b435cf4c9efc154b6e4f7b9526db70d78dba40df |
programfile | ../../sv-benchmarks/c/pthread-wmm/mix009_pso.oepc_false-unreach-call.i |
programhash | 757f7e1bd660db5c5d113471b435cf4c9efc154b6e4f7b9526db70d78dba40df |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/8bd08a64a5f8e2162b4d65089394309faf33ae93de1b41fa108bbb1d3037ec82.graphml |
witness-sha256 | 8bd08a64a5f8e2162b4d65089394309faf33ae93de1b41fa108bbb1d3037ec82 |
witness-size | 23824 |
witness-type | violation_witness |
This witness was created for this program (cf. table above, 757f7e1bd660db5c5d113471b435cf4c9efc154b6e4f7b9526db70d78dba40df).
Found 0 witnesses for program sv-benchmarks/c/pthread-wmm/mix009_pso.oepc_false-unreach-call.i, 757f7e1bd660db5c5d113471b435cf4c9efc154b6e4f7b9526db70d78dba40df
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/757f7e1bd660db5c5d113471b435cf4c9efc154b6e4f7b9526db70d78dba40df.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/mix009_pso.oepc_false-unreach-call.i, 757f7e1bd660db5c5d113471b435cf4c9efc154b6e4f7b9526db70d78dba40df
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/757f7e1bd660db5c5d113471b435cf4c9efc154b6e4f7b9526db70d78dba40df.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/mix009_pso.oepc_false-unreach-call.i, 757f7e1bd660db5c5d113471b435cf4c9efc154b6e4f7b9526db70d78dba40df
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/757f7e1bd660db5c5d113471b435cf4c9efc154b6e4f7b9526db70d78dba40df.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/mix009_pso.oepc_false-unreach-call.i, 757f7e1bd660db5c5d113471b435cf4c9efc154b6e4f7b9526db70d78dba40df
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/757f7e1bd660db5c5d113471b435cf4c9efc154b6e4f7b9526db70d78dba40df.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/mix009_pso.oepc_false-unreach-call.i, 757f7e1bd660db5c5d113471b435cf4c9efc154b6e4f7b9526db70d78dba40df
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/757f7e1bd660db5c5d113471b435cf4c9efc154b6e4f7b9526db70d78dba40df.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/mix009_pso.oepc_false-unreach-call.i, 757f7e1bd660db5c5d113471b435cf4c9efc154b6e4f7b9526db70d78dba40df
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/757f7e1bd660db5c5d113471b435cf4c9efc154b6e4f7b9526db70d78dba40df.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
a8b5200 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | SMACK 1.9.3 | 3 | 2018-12-07T21:39:38 | ||
e94bc6c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 23 | 2018-12-08T00:48:10+01:00 | ||
f1c4ddd | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 577 | 2018-12-10T10:49:19+01:00 | 365b1ef | |
9d00188 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 21 | 2018-12-09T21:47:48+01:00 | 655cf16 | |
38f50c9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 22 | 2018-12-09T21:38:36+01:00 | 501b728 | |
9273619 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 24 | 2018-12-08T08:05:52+01:00 | e94bc6c | |
c65b256 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 94 | 2018-12-08T04:56:34+01:00 | a1706ba | |
57dbf75 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 577 | 2018-12-08T04:35:13+01:00 | 365b1ef | |
b8c372c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 23 | 2018-12-06T19:53:46+01:00 | fac81c6 | |
3a7f932 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 94 | 2018-12-06T10:19:09+01:00 | 906f5b8 | |
8bd08a6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 24 | 2018-12-06T09:48:38+01:00 | cc0a72d | |
3088d7b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 195 | 2018-12-06T09:20:05+01:00 | 678f779 | |
cc0a72d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 23 | 2018-12-05T13:44:35+01:00 | ||
0729a46 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 17 | 2018-12-09T20:53:39+01:00 | 12227f3 | |
9f00556 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 17 | 2018-12-09T20:38:21+01:00 | a12dc7b | |
d7c8f01 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 17 | 2018-12-08T22:07:45+01:00 | a8b5200 |
Found 8 witnesses for program sv-benchmarks/c/pthread-wmm/mix009_pso.oepc_false-unreach-call.i, 757f7e1bd660db5c5d113471b435cf4c9efc154b6e4f7b9526db70d78dba40df
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/757f7e1bd660db5c5d113471b435cf4c9efc154b6e4f7b9526db70d78dba40df.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
f2f7825 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Yogar-CBMC 1.0 | 14 | 2017-12-03T05:47 CET (sv-comp) | ||
d61e5e9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 kind | 4 | 2017-12-02T12:49:24.692228 | ||
0f938af | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 incr | 4 | 2017-12-02T04:30:03.700648 | ||
6ff3d46 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 22 | 2017-12-01T11:05 CET (sv-comp) | ||
c905c83 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 20 | 2017-12-01T09:34:51+01:00 | ||
678f779 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CBMC | 3 | 2017-12-01T10:21 CET (sv-comp) | ||
3f09d04 | 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 | 3cacf87 | |
80a47f4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26758M | 14 | 2017-12-01T08:46:39+01:00 |
Found 0 witnesses for program sv-benchmarks/c/pthread-wmm/mix009_pso.oepc_false-unreach-call.i, 757f7e1bd660db5c5d113471b435cf4c9efc154b6e4f7b9526db70d78dba40df
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/757f7e1bd660db5c5d113471b435cf4c9efc154b6e4f7b9526db70d78dba40df.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |