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/reducercommutativity/sep10_true-unreach-call.i |
programSHA | 2fe8f963c330593b6ee268850ff5f2696229c0b67f333b95f4b4a9418edfccfa |
witnessName | results-verified/cpa-bam-bnb.2017-11-30_1120.logfiles/sv-comp18.sep10_true-unreach-call.i.files/witness.graphml |
witnessSHA | 7bc95cd2343d35d7f21010b010edeb88d1141fdeddd1e23dbfaf8aa112b4d888 |
Key | Value |
architecture | 32bit |
creationtime | 2017-11-30T20:58:26+01:00 |
producer | CPAchecker 1.6.1-svn 26725 |
program-sha256 | 2fe8f963c330593b6ee268850ff5f2696229c0b67f333b95f4b4a9418edfccfa |
programfile | ../../sv-benchmarks/c/reducercommutativity/sep10_true-unreach-call.i |
programhash | 296305352db81de7603dacdfc840cce470057e81 |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/7bc95cd2343d35d7f21010b010edeb88d1141fdeddd1e23dbfaf8aa112b4d888.graphml |
witness-sha256 | 7bc95cd2343d35d7f21010b010edeb88d1141fdeddd1e23dbfaf8aa112b4d888 |
witness-size | 60731 |
witness-type | violation_witness |
Found 0 witnesses for program sv-benchmarks/c/reducercommutativity/sep10_true-unreach-call.i, 2fe8f963c330593b6ee268850ff5f2696229c0b67f333b95f4b4a9418edfccfa
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/2fe8f963c330593b6ee268850ff5f2696229c0b67f333b95f4b4a9418edfccfa.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/reducercommutativity/sep10_true-unreach-call.i, 2fe8f963c330593b6ee268850ff5f2696229c0b67f333b95f4b4a9418edfccfa
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/2fe8f963c330593b6ee268850ff5f2696229c0b67f333b95f4b4a9418edfccfa.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/reducercommutativity/sep10_true-unreach-call.i, 2fe8f963c330593b6ee268850ff5f2696229c0b67f333b95f4b4a9418edfccfa
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/2fe8f963c330593b6ee268850ff5f2696229c0b67f333b95f4b4a9418edfccfa.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/reducercommutativity/sep10_true-unreach-call.i, 2fe8f963c330593b6ee268850ff5f2696229c0b67f333b95f4b4a9418edfccfa
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/2fe8f963c330593b6ee268850ff5f2696229c0b67f333b95f4b4a9418edfccfa.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 6 witnesses for program sv-benchmarks/c/reducercommutativity/sep10_true-unreach-call.i, 2fe8f963c330593b6ee268850ff5f2696229c0b67f333b95f4b4a9418edfccfa
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/2fe8f963c330593b6ee268850ff5f2696229c0b67f333b95f4b4a9418edfccfa.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
bfa6d56 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 9 | 2019-12-11T20:15:14+01:00 | bb64002 | |
6fcd786 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 9 | 2019-12-11T20:02:56+01:00 | 15533c0 | |
f1229bb | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 9 | 2019-12-08T00:37:17+01:00 | eefc068 | |
72313a4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 9 | 2019-12-06T01:44:01+01:00 | 5e3fbb0 | |
2024a9f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 9 | 2019-12-05T19:13:11+01:00 | 9cde66e | |
7d02947 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / svcomp20 | 165 | 2019-11-30T05:25:50+01:00 |
Found 13 witnesses for program sv-benchmarks/c/reducercommutativity/sep10_true-unreach-call.i, 2fe8f963c330593b6ee268850ff5f2696229c0b67f333b95f4b4a9418edfccfa
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/2fe8f963c330593b6ee268850ff5f2696229c0b67f333b95f4b4a9418edfccfa.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
eafe4c4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T16:57 CET (sv-comp) | ||
2222b17 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | SMACK 1.9.3 | 3 | 2018-12-08T07:38:47 | ||
c196a5f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7 | 10 | 2018-12-10T18:39:10+01:00 | ||
7e15393 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 10 | 2018-12-07T09:33:00+01:00 | ||
e075aa7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 10 | 2018-12-10T20:22:10+01:00 | c196a5f | |
4fd4756 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-09T21:21:10+01:00 | b042a52 | |
bb54900 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-08T23:33:26+01:00 | eafe4c4 | |
54afc68 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-08T21:44:20+01:00 | 2222b17 | |
1015dd5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-08T06:54:53+01:00 | 7e15393 | |
a1bc85a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-08T03:54:45+01:00 | 9ded40a | |
7dec212 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-07T17:58:43+01:00 | 1ca5818 | |
dc8b0ea | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-06T09:43:16+01:00 | 08776dd | |
e971a24 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-06T07:42:06+01:00 | ff0bce7 |
Found 19 witnesses for program sv-benchmarks/c/reducercommutativity/sep10_true-unreach-call.i, 2fe8f963c330593b6ee268850ff5f2696229c0b67f333b95f4b4a9418edfccfa
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/2fe8f963c330593b6ee268850ff5f2696229c0b67f333b95f4b4a9418edfccfa.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
aebd6a7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26758M | 101 | 2017-11-30T18:56:19+01:00 | ||
7bc95cd | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26725 | 61 | 2017-11-30T20:58:26+01:00 | ||
1ca5818 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | skink | 3 | 2017-12-01T22:35 CET (sv-comp) | ||
cad2f24 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Symbiotic | 1 | 2017-12-02T00:23 CET (sv-comp) | ||
1822858 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Map2Check | 5 | 2017-12-01T20:42 CET (sv-comp) | ||
4e6bbd7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 kind | 3 | 2017-12-01T21:38:14.898151 | ||
f503b9b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 incr | 3 | 2017-12-01T12:54:08.387133 | ||
8967116 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 3.1 | 30 | 2017-12-01T02:13 CET (sv-comp) | ||
27f5454 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn | 10 | 2017-12-02T23:46:43+01:00 | ||
645374f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 9 | 2017-12-02T20:46:20+01:00 | 75b5dce | |
97fdee8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 9 | 2017-12-02T08:54:51+01:00 | 2869eb5 | |
eaebe35 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 9 | 2017-12-02T00:30:06+01:00 | 59f7691 | |
8a5f9e0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 9 | 2017-12-01T22:42:12+01:00 | e63f950 | |
48a4787 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 9 | 2017-12-01T22:19:36+01:00 | 6d08db3 | |
c6277c5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 9 | 2017-12-01T08:27:56+01:00 | 832f2c7 | |
6548937 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 9 | 2017-12-01T07:17:09+01:00 | e7edbe3 | |
d184b0e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 9 | 2017-12-01T06:59:19+01:00 | c34e87a | |
4702e48 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CBMC | 59 | 2017-11-30T17:15 CET (sv-comp) | ||
e12b355 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | 2LS | 105 | 2017-11-30T18:50 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/reducercommutativity/sep10_true-unreach-call.i, 2fe8f963c330593b6ee268850ff5f2696229c0b67f333b95f4b4a9418edfccfa
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/2fe8f963c330593b6ee268850ff5f2696229c0b67f333b95f4b4a9418edfccfa.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |