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/termination-memory-alloca/java_Sequence-alloca_true-termination.c.i |
programSHA | d628f3524885345eb9e2318f2d0dbb026e233c3bcc51319b2ad8fc1a71d35580 |
witnessName | results-verified/esbmc-incr.2017-12-02_0845.logfiles/sv-comp18.java_Sequence-alloca_true-termination.c.i.files/witness.graphml |
witnessSHA | 1623c7309364f4ffb4de9680b19ff8f53738422c438b49b48facf7366671f370 |
Key | Value |
architecture | 64bit |
creationtime | 2017-12-02T09:47:16.199071 |
producer | ESBMC 4.6.0 |
program-sha256 | d628f3524885345eb9e2318f2d0dbb026e233c3bcc51319b2ad8fc1a71d35580 |
programfile | ../../sv-benchmarks/c/termination-memory-alloca/java_Sequence-alloca_true-termination.c.i |
programhash | 8a6685c614a472075ec95b2104ea4dfab3f7f92c |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/1623c7309364f4ffb4de9680b19ff8f53738422c438b49b48facf7366671f370.graphml |
witness-sha256 | 1623c7309364f4ffb4de9680b19ff8f53738422c438b49b48facf7366671f370 |
witness-size | 3416 |
witness-type | correctness_witness |
Found 25 witnesses for program sv-benchmarks/c/termination-memory-alloca/java_Sequence-alloca_true-termination.c.i, d628f3524885345eb9e2318f2d0dbb026e233c3bcc51319b2ad8fc1a71d35580
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/d628f3524885345eb9e2318f2d0dbb026e233c3bcc51319b2ad8fc1a71d35580.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
484965b | Inspect | valid-memsafety | correctness_witness | DIVINE 4 | 2 | 2023-12-18T10:54:34+01:00 | ||
f7e97c6 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 3 | 2023-11-30T00:21:00Z | ||
aa4a9b8 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-11-30T07:52:41+01:00 | ||
f17ddb2 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2.1-svn-e677b7cd46+ | 5 | 2023-12-03T18:11:28+01:00 | ||
f2a5493 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.1 | 5 | 2023-12-17T02:35:25+01:00 | ||
e001213 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 5 | 2023-12-18T18:27:14+01:00 | ||
a210e75 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-38892M | 8 | 2023-12-18T01:44:17+01:00 | ||
63fa71c | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Bubaak | 3 | 2023-12-05T09:38:11Z | ||
3ea92bb | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Bubaak | 3 | 2023-12-04T08:34:59Z | ||
926ab54 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Bubaak | 3 | 2023-12-01T20:29:04Z | ||
0e86b40 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 7.4.0 incr | 3 | 2023-12-01T13:21:51Z | ||
0d85bbf | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Taipan | 14 | 2023-12-02T07:22:54Z | ||
362ffdc | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | PredatorHP | 4 | 2023-11-30T08:25:21Z | ||
5f3f1c4 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Mopsa (v1.0~pre2) | 3 | 2023-11-29T10:13:21Z | ||
63d4a57 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Goblint (tags/svcomp24-0-gc2e9465a7) | 17 | 2023-12-01T01:58:52Z | ||
52f2184 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CBMC | 80 | 2023-12-17T13:10:39+01:00 | ||
f1d805c | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Automizer | 14 | 2023-11-28T23:40:58Z | ||
6e545cf | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 7.4.0 | 3 | 2023-12-01T10:12:55Z | ||
160f86b | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 3 | 2023-12-17T01:32:34Z | ||
7674847 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 3 | 2023-11-29T19:40:08Z | ||
5c83f16 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2023-12-20T00:14:36 | ||
97c9cff | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 80 | 2023-12-17T13:42:29+01:00 | ||
21ad897 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Bubaak | 3 | 2023-12-05T09:49:34Z | ||
ee0d610 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Bubaak | 3 | 2023-12-04T12:50:32Z | ||
321cf12 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Bubaak | 3 | 2023-12-01T20:39:01Z |
Found 19 witnesses for program sv-benchmarks/c/termination-memory-alloca/java_Sequence-alloca_true-termination.c.i, d628f3524885345eb9e2318f2d0dbb026e233c3bcc51319b2ad8fc1a71d35580
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/d628f3524885345eb9e2318f2d0dbb026e233c3bcc51319b2ad8fc1a71d35580.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
4750e80 | Inspect | valid-memsafety | correctness_witness | DIVINE 4 | 2 | 2022-12-09T05:15:35+01:00 | ||
7cc8ce1 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 5 | 2022-12-10T14:59:40+01:00 | ||
732ebd8 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2.1-svn-1715bd67dc+ | 5 | 2022-12-12T01:43:36+01:00 | ||
7e7b5d4 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.1 | 5 | 2022-12-25T13:03:39+01:00 | ||
f3965fb | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 5 | 2022-12-10T04:37:38+01:00 | ||
57dd3d0 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-38892M | 8 | 2022-12-09T03:21:43+01:00 | ||
4ce7151 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Bubaak | 3 | 2022-12-08T21:17:39Z | ||
7caa3a3 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 7.0.0 incr | 3 | 2022-12-18T19:06:21Z | ||
c85c9aa | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Taipan | 14 | 2022-12-14T03:45:09Z | ||
074ceba | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Mopsa (v1.0~pre2) | 3 | 2022-12-11T10:22:00Z | ||
5b12f00 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CBMC | 80 | 2022-12-08T04:38:38+01:00 | ||
647497e | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Automizer | 14 | 2022-12-13T13:37:30Z | ||
11acd04 | Inspect | CHECK( init(main()), LTL(G ! call(reach_error())) ) | correctness_witness | ESBMC 6.8.0 | 3 | 2022-12-25T10:51:28Z | ||
bf56292 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 7.0.0 | 3 | 2022-12-18T17:45:55Z | ||
4d44cbd | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 3 | 2022-12-25T10:51:28Z | ||
5850ff8 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 3 | 2022-12-12T12:27:29Z | ||
132a49e | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2022-12-11T14:38:42 | ||
cc28491 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 80 | 2022-12-08T05:05:00+01:00 | ||
fb0235a | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Bubaak | 3 | 2022-12-08T16:41:11Z |
Found 5 witnesses for program sv-benchmarks/c/termination-memory-alloca/java_Sequence-alloca_true-termination.c.i, d628f3524885345eb9e2318f2d0dbb026e233c3bcc51319b2ad8fc1a71d35580
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/d628f3524885345eb9e2318f2d0dbb026e233c3bcc51319b2ad8fc1a71d35580.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
332d5fa | Inspect | CHECK( init(main()), LTL(G ! call(reach_error())) ) | correctness_witness | ESBMC 6.8.0 | 3 | 2021-12-08T04:13:23Z | ||
c3cd43c | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2021-12-10T17:44:11 | ||
d31738f | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 3 | 2021-12-07T12:10:37Z | ||
493cee8 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2021-12-09T05:10:12 | ||
cfa44fb | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 78 | 2021-12-06T02:07:50+01:00 |
Found 3 witnesses for program sv-benchmarks/c/termination-memory-alloca/java_Sequence-alloca_true-termination.c.i, d628f3524885345eb9e2318f2d0dbb026e233c3bcc51319b2ad8fc1a71d35580
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/d628f3524885345eb9e2318f2d0dbb026e233c3bcc51319b2ad8fc1a71d35580.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
41a1dac | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2020-12-11T18:40:14 | ||
df789a3 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2020-12-09T00:12:39 | ||
8e1bae5 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2020-12-08T11:02:24 |
Found 1 witnesses for program sv-benchmarks/c/termination-memory-alloca/java_Sequence-alloca_true-termination.c.i, d628f3524885345eb9e2318f2d0dbb026e233c3bcc51319b2ad8fc1a71d35580
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/d628f3524885345eb9e2318f2d0dbb026e233c3bcc51319b2ad8fc1a71d35580.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
2019bee | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2019-12-04T01:11 CET (comp) |
Found 2 witnesses for program sv-benchmarks/c/termination-memory-alloca/java_Sequence-alloca_true-termination.c.i, d628f3524885345eb9e2318f2d0dbb026e233c3bcc51319b2ad8fc1a71d35580
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/d628f3524885345eb9e2318f2d0dbb026e233c3bcc51319b2ad8fc1a71d35580.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
d256b27 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T17:00 CET (sv-comp) | ||
8887d46 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2018-12-07T01:11 CET (sv-comp) |
Found 5 witnesses for program sv-benchmarks/c/termination-memory-alloca/java_Sequence-alloca_true-termination.c.i, d628f3524885345eb9e2318f2d0dbb026e233c3bcc51319b2ad8fc1a71d35580
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/d628f3524885345eb9e2318f2d0dbb026e233c3bcc51319b2ad8fc1a71d35580.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
877e0d4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T23:53:16.659472 | ||
1623c73 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T09:47:16.199071 | ||
728bc00 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 3.1 | 6 | 2017-12-01T16:54 CET (sv-comp) | ||
b89b69a | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 82 | 2017-12-01T13:50 CET (sv-comp) | ||
9f33e2d | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | 2LS | 26 | 2017-12-01T11:56 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/termination-memory-alloca/java_Sequence-alloca_true-termination.c.i, d628f3524885345eb9e2318f2d0dbb026e233c3bcc51319b2ad8fc1a71d35580
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/d628f3524885345eb9e2318f2d0dbb026e233c3bcc51319b2ad8fc1a71d35580.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |