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-ext/32_pthread5_vs_false-unreach-call.i |
programSHA | 7353a88dff637399f8576bb4e95004a66251395a304bd1c58fdc45300702af0e |
witnessName | results-validated/cpa-seq-validate-violation-witnesses-divine-smt.2018-12-08_0324.logfiles/sv-comp19_prop-reachsafety.32_pthread5_vs_false-unreach-call.i.files/witness.graphml |
witnessSHA | 18bcf27bd8382e8668a1f19aa5addd98e2d2b8b7de14b4aa9c8737b6d474a872 |
Key | Value |
architecture | 32bit |
creationtime | 2018-12-08T04:36:22+01:00 |
inputwitnesshash | 92a236dcc0473b55fbed62e1d638c80bb171ef45af61943c744ddc04eb941a6a |
producer | CPAchecker 1.7-svn 29852 |
program-sha256 | 7353a88dff637399f8576bb4e95004a66251395a304bd1c58fdc45300702af0e |
programfile | ../../sv-benchmarks/c/pthread-ext/32_pthread5_vs_false-unreach-call.i |
programhash | 7353a88dff637399f8576bb4e95004a66251395a304bd1c58fdc45300702af0e |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/18bcf27bd8382e8668a1f19aa5addd98e2d2b8b7de14b4aa9c8737b6d474a872.graphml |
witness-sha256 | 18bcf27bd8382e8668a1f19aa5addd98e2d2b8b7de14b4aa9c8737b6d474a872 |
witness-size | 3182 |
witness-type | correctness_witness |
This witness was created for this program (cf. table above, 7353a88dff637399f8576bb4e95004a66251395a304bd1c58fdc45300702af0e).
Found 0 witnesses for program sv-benchmarks/c/pthread-ext/32_pthread5_vs_false-unreach-call.i, 7353a88dff637399f8576bb4e95004a66251395a304bd1c58fdc45300702af0e
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/7353a88dff637399f8576bb4e95004a66251395a304bd1c58fdc45300702af0e.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/pthread-ext/32_pthread5_vs_false-unreach-call.i, 7353a88dff637399f8576bb4e95004a66251395a304bd1c58fdc45300702af0e
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/7353a88dff637399f8576bb4e95004a66251395a304bd1c58fdc45300702af0e.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/pthread-ext/32_pthread5_vs_false-unreach-call.i, 7353a88dff637399f8576bb4e95004a66251395a304bd1c58fdc45300702af0e
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/7353a88dff637399f8576bb4e95004a66251395a304bd1c58fdc45300702af0e.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/pthread-ext/32_pthread5_vs_false-unreach-call.i, 7353a88dff637399f8576bb4e95004a66251395a304bd1c58fdc45300702af0e
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/7353a88dff637399f8576bb4e95004a66251395a304bd1c58fdc45300702af0e.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/pthread-ext/32_pthread5_vs_false-unreach-call.i, 7353a88dff637399f8576bb4e95004a66251395a304bd1c58fdc45300702af0e
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/7353a88dff637399f8576bb4e95004a66251395a304bd1c58fdc45300702af0e.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 9 witnesses for program sv-benchmarks/c/pthread-ext/32_pthread5_vs_false-unreach-call.i, 7353a88dff637399f8576bb4e95004a66251395a304bd1c58fdc45300702af0e
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/7353a88dff637399f8576bb4e95004a66251395a304bd1c58fdc45300702af0e.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
062d28e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | SMACK 1.9.3 | 3 | 2018-12-08T19:19:08 | ||
b112930 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-10T10:48:47+01:00 | 92a236d | |
754b3f1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-09T21:48:41+01:00 | be714e7 | |
bf23bdb | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-09T21:38:32+01:00 | 88a1d05 | |
5d6435b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-08T22:11:37+01:00 | 062d28e | |
18bcf27 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-08T04:36:22+01:00 | 92a236d | |
1049dec | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-06T19:33:34+01:00 | 0f75936 | |
bdfd964 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-06T09:20:23+01:00 | d0f90aa | |
65532e9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-05T23:37:57+01:00 |
Found 4 witnesses for program sv-benchmarks/c/pthread-ext/32_pthread5_vs_false-unreach-call.i, 7353a88dff637399f8576bb4e95004a66251395a304bd1c58fdc45300702af0e
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/7353a88dff637399f8576bb4e95004a66251395a304bd1c58fdc45300702af0e.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
35a4ea9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Yogar-CBMC 1.0 | 7 | 2017-12-03T05:57 CET (sv-comp) | ||
d0f90aa | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CBMC | 4 | 2017-12-01T10:15 CET (sv-comp) | ||
9d03e4f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 3.1 | 10 | 2017-12-01T11:28 CET (sv-comp) | ||
8add761 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26758M | 5 | 2017-12-01T08:46:24+01:00 |
Found 0 witnesses for program sv-benchmarks/c/pthread-ext/32_pthread5_vs_false-unreach-call.i, 7353a88dff637399f8576bb4e95004a66251395a304bd1c58fdc45300702af0e
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/7353a88dff637399f8576bb4e95004a66251395a304bd1c58fdc45300702af0e.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |