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/heap-manipulation/merge_sort_false-unreach-call_false-valid-memcleanup.i |
programSHA | 61be264313c2cc691e6d9d8cd67f06fa6fb42ebce20e4cac56aadad9c84afa6c |
witnessName | results-verified/divine-explicit.2018-12-10_1000.logfiles/sv-comp19_prop-reachsafety.merge_sort_false-unreach-call_false-valid-memcleanup.i.files/witness.graphml |
witnessSHA | 5b8606367783596dec00c1deec58ba0fd881cdafbddcc20addc7c11ffd0fa9d1 |
Key | Value |
architecture | 32bit |
creationtime | 2018-12-07T00:59 CET (sv-comp) |
memorymodel | precise |
producer | DIVINE 4 |
programfile | ../../sv-benchmarks/c/heap-manipulation/merge_sort_false-unreach-call_false-valid-memcleanup.i |
programhash | 534681b11e8e68e6058985d885b01f2cbfa43e5b |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/5b8606367783596dec00c1deec58ba0fd881cdafbddcc20addc7c11ffd0fa9d1.graphml |
witness-sha256 | 5b8606367783596dec00c1deec58ba0fd881cdafbddcc20addc7c11ffd0fa9d1 |
witness-size | 3709 |
witness-type | violation_witness |
Found 0 witnesses for program sv-benchmarks/c/heap-manipulation/merge_sort_false-unreach-call_false-valid-memcleanup.i, 61be264313c2cc691e6d9d8cd67f06fa6fb42ebce20e4cac56aadad9c84afa6c
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/61be264313c2cc691e6d9d8cd67f06fa6fb42ebce20e4cac56aadad9c84afa6c.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/heap-manipulation/merge_sort_false-unreach-call_false-valid-memcleanup.i, 61be264313c2cc691e6d9d8cd67f06fa6fb42ebce20e4cac56aadad9c84afa6c
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/61be264313c2cc691e6d9d8cd67f06fa6fb42ebce20e4cac56aadad9c84afa6c.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/heap-manipulation/merge_sort_false-unreach-call_false-valid-memcleanup.i, 61be264313c2cc691e6d9d8cd67f06fa6fb42ebce20e4cac56aadad9c84afa6c
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/61be264313c2cc691e6d9d8cd67f06fa6fb42ebce20e4cac56aadad9c84afa6c.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/heap-manipulation/merge_sort_false-unreach-call_false-valid-memcleanup.i, 61be264313c2cc691e6d9d8cd67f06fa6fb42ebce20e4cac56aadad9c84afa6c
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/61be264313c2cc691e6d9d8cd67f06fa6fb42ebce20e4cac56aadad9c84afa6c.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 25 witnesses for program sv-benchmarks/c/heap-manipulation/merge_sort_false-unreach-call_false-valid-memcleanup.i, 61be264313c2cc691e6d9d8cd67f06fa6fb42ebce20e4cac56aadad9c84afa6c
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/61be264313c2cc691e6d9d8cd67f06fa6fb42ebce20e4cac56aadad9c84afa6c.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
13bd5cc | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | Symbiotic | 1 | 2019-12-01 22:39:45 | ||
3eedfaa | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | CPAchecker 1.9 | 10 | 2019-12-11T21:43:57+01:00 | 4e9c143 | |
7b13d5d | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | CPAchecker 1.9 | 11 | 2019-12-11T21:09:34+01:00 | 13bd5cc | |
9b8b119 | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | CPAchecker 1.9 | 10 | 2019-12-08T00:07:31+01:00 | 9e6ae57 | |
cf0dc00 | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | CPAchecker 1.9 | 10 | 2019-12-03T08:10:25+01:00 | 8bec80e | |
8bec80e | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | CPAchecker 1.9 | 10 | 2019-11-29T14:22:36+01:00 | ||
4e9c143 | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 10 | 2019-12-01T15:28:06+01:00 | ||
8f7e49c | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | correctness_witness | CPAchecker 1.9 | 30 | 2019-12-11T22:00:21+01:00 | 309e117 | |
8940f9a | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | correctness_witness | CPAchecker 1.9 | 30 | 2019-12-08T00:27:12+01:00 | 56b9579 | |
1c6f481 | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | correctness_witness | CPAchecker 1.9 | 30 | 2019-12-07T21:17:56+01:00 | 00408f3 | |
61bd4c9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2019-12-02 03:21:35 | ||
6304334 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 13 | 2019-12-11T21:47:05+01:00 | 0470e83 | |
f8d97ef | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 13 | 2019-12-11T21:45:11+01:00 | 8330789 | |
ee300d2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 13 | 2019-12-11T21:09:02+01:00 | 61bd4c9 | |
420cb4c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 16 | 2019-12-11T20:55:26+01:00 | 758710d | |
bb15413 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 6446 | 2019-12-11T20:45:22+01:00 | 8508c77 | |
cfc79bc | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 13 | 2019-12-08T00:26:07+01:00 | dd50393 | |
f211f0b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 13 | 2019-12-08T00:06:04+01:00 | d187557 | |
49207bd | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 13 | 2019-12-07T21:17:09+01:00 | 2b91f1f | |
b9f9654 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 13 | 2019-12-05T20:20:28+01:00 | 509ad6e | |
5e5fefb | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 13 | 2019-12-03T08:57:02+01:00 | 7536b57 | |
926cbb7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / svcomp20 | 18 | 2019-11-29T20:45:11+01:00 | ||
8330789 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco | 13 | 2019-11-30T22:55:41+01:00 | ||
8937cbb | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 30 | 2019-12-08T01:51:30+01:00 | d01b9d2 | |
5d62f7b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 30 | 2019-12-03T08:08:57+01:00 | 926cbb7 |
Found 27 witnesses for program sv-benchmarks/c/heap-manipulation/merge_sort_false-unreach-call_false-valid-memcleanup.i, 61be264313c2cc691e6d9d8cd67f06fa6fb42ebce20e4cac56aadad9c84afa6c
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/61be264313c2cc691e6d9d8cd67f06fa6fb42ebce20e4cac56aadad9c84afa6c.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
1595296 | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | Symbiotic | 1 | 2018-12-08T16:44 CET (sv-comp) | ||
26683d7 | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | SMACK 1.9.3 | 3 | 2018-12-08T04:51:35 | ||
68e3267 | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | CPAchecker 1.7-svn 29852 | 10 | 2018-12-08T23:43:28+01:00 | 1595296 | |
069fbc5 | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | CPAchecker 1.7-svn 29852 | 10 | 2018-12-08T22:11:00+01:00 | 26683d7 | |
84e375f | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | CPAchecker 1.7-svn 29852 | 10 | 2018-12-07T09:15:59+01:00 | 7f92492 | |
cf39982 | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | CPAchecker 1.7-svn 29852 | 10 | 2018-12-06T10:17:54+01:00 | a5a8dba | |
414064d | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | CPAchecker 1.7-svn 29852 | 10 | 2018-12-06T09:48:21+01:00 | 3be2416 | |
3be2416 | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | CPAchecker 1.7-svn 29852 | 10 | 2018-12-05T18:23:06+01:00 | ||
a589627 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2018-12-08T00:53 CET (sv-comp) | ||
2c7c1dc | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | SMACK 1.9.3 | 3 | 2018-12-08T15:44:33 | ||
025b54b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7 | 11 | 2018-12-10T18:33:07+01:00 | ||
5e3855d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 18 | 2018-12-07T18:23:59+01:00 | ||
11dba7c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 12 | 2018-12-10T20:35:09+01:00 | 025b54b | |
1deb102 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 12 | 2018-12-10T10:48:43+01:00 | 5b86063 | |
e8722e7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 12 | 2018-12-09T20:53:07+01:00 | 3c50ba5 | |
d3dc350 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 12 | 2018-12-09T20:34:34+01:00 | 9859f4b | |
8bad89c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 12 | 2018-12-09T20:18:18+01:00 | ae7e0a7 | |
2ce854b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 12 | 2018-12-08T23:43:44+01:00 | a589627 | |
7f411a7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 12 | 2018-12-08T22:09:39+01:00 | 2c7c1dc | |
a7cf083 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 12 | 2018-12-08T04:55:20+01:00 | 2ccfdf3 | |
333161a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 12 | 2018-12-08T04:35:48+01:00 | 5b86063 | |
6a31dde | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 12 | 2018-12-07T09:14:55+01:00 | 26ce0a6 | |
1fde979 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 12 | 2018-12-06T10:19:19+01:00 | 8362f14 | |
46e4fdb | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 12 | 2018-12-06T09:15:55+01:00 | 2b9ca09 | |
e54b881 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 18 | 2018-12-06T03:59:46+01:00 | ||
8ae8590 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 30 | 2018-12-08T08:58:11+01:00 | 5e3855d | |
150944e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 30 | 2018-12-06T09:48:47+01:00 | e54b881 |
Found 14 witnesses for program sv-benchmarks/c/heap-manipulation/merge_sort_false-unreach-call_false-valid-memcleanup.i, 61be264313c2cc691e6d9d8cd67f06fa6fb42ebce20e4cac56aadad9c84afa6c
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/61be264313c2cc691e6d9d8cd67f06fa6fb42ebce20e4cac56aadad9c84afa6c.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
48e69aa | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Taipan | 11 | 2017-12-02T19:27Z | ||
78e986f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2017-12-01T22:43 CET (sv-comp) | ||
26ce0a6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | PredatorHP | 5 | 2017-12-01T20:26 CET (sv-comp) | ||
cb1ebba | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Map2Check | 3 | 2017-12-01T20:54 CET (sv-comp) | ||
51ac09c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Kojak | 11 | 2017-12-02T21:27Z | ||
b641f7f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 kind | 4 | 2017-12-01T16:37:15.442650 | ||
ebebb27 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 incr | 4 | 2017-12-01T11:15:57.302236 | ||
e261d9d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 4 | 2017-12-01T06:20 CET (sv-comp) | ||
696292a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 11 | 2017-11-30T11:39:12+01:00 | ||
ad626c6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26758M | 16 | 2017-11-30T15:29:08+01:00 | ||
217a968 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26725 | 10 | 2017-11-30T21:27:50+01:00 | ||
2bbc040 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker (unknown version) | 15 | 2017-12-02T04:48:20+01:00 | ||
befe649 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CBMC | 9 | 2017-11-30T13:16 CET (sv-comp) | ||
6f82ab3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Automizer | 11 | 2017-12-02T07:31Z |
Found 0 witnesses for program sv-benchmarks/c/heap-manipulation/merge_sort_false-unreach-call_false-valid-memcleanup.i, 61be264313c2cc691e6d9d8cd67f06fa6fb42ebce20e4cac56aadad9c84afa6c
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/61be264313c2cc691e6d9d8cd67f06fa6fb42ebce20e4cac56aadad9c84afa6c.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |