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/HarrisLalNoriRajamani-2010SAS-Fig1-alloca_true-termination.c.i |
programSHA | 7d44dc9ee297680f321b2cf4dcd79f3ba6ced2470ed6439fc6dd5eb0285efc9c |
witnessName | results-verified/cbmc-path.2018-12-04_2245.logfiles/sv-comp19_prop-termination.HarrisLalNoriRajamani-2010SAS-Fig1-alloca_true-termination.c.i.files/witness.graphml |
witnessSHA | e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855 |
Key | Value |
creationtime | 2018-12-05T13:03 CET (sv-comp) |
error-programhash | Key 'programhash' not present. |
error-specification-exists | Key 'specification' not present. |
error-xmlparsing | File produces XML parsing error. |
witness-file | witnessFileByHash/e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855.graphml |
witness-sha256 | e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855 |
witness-size | 0 |
The following keys are missing in the witness XML file: witness-type, sourcecodelang, producer, specification, programfile, programhash, architecture.
Found 24 witnesses for program sv-benchmarks/c/termination-memory-alloca/HarrisLalNoriRajamani-2010SAS-Fig1-alloca_true-termination.c.i, 7d44dc9ee297680f321b2cf4dcd79f3ba6ced2470ed6439fc6dd5eb0285efc9c
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/7d44dc9ee297680f321b2cf4dcd79f3ba6ced2470ed6439fc6dd5eb0285efc9c.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
bb378f9 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2023-12-18T10:29:23+01:00 | ||
01e4986 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 3 | 2023-11-29T21:53:53Z | ||
222286b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 8 | 2023-12-18T12:06:06+01:00 | bb378f9 | |
843814f | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 8 | 2023-11-30T07:05:51+01:00 | ||
c3e14ac | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2.1-svn-e677b7cd46+ | 8 | 2023-12-03T23:18:13+01:00 | ||
b13ed44 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 8 | 2023-12-19T00:10:00+01:00 | ||
f9c5b27 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-38892M | 14 | 2023-12-18T01:34:30+01:00 | ||
90e93f4 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Bubaak | 3 | 2023-12-05T07:23:04Z | ||
d8f6220 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Bubaak | 3 | 2023-12-04T09:45:04Z | ||
98ca90e | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Bubaak | 3 | 2023-12-01T20:36:12Z | ||
19c1d0e | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 7.4.0 incr | 3 | 2023-12-01T15:02:58Z | ||
9944333 | 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 | 24 | 2023-12-02T14:57:00Z | ||
13a6bdc | 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:24:47Z | ||
06c8736 | 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-29T13:16:10Z | ||
34f2ea8 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Kojak | 47 | 2023-12-02T20:28:09Z | ||
f2efa30 | 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) | 38 | 2023-12-01T02:00:31Z | ||
0242dce | 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 | 28 | 2023-12-17T15:35:33+01:00 | ||
9186a97 | 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 | 24 | 2023-11-28T22:56:02Z | ||
7dc0aaa | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 7.4.0 | 3 | 2023-12-01T15:48:29Z | ||
58de399 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 3 | 2023-11-29T22:17:15Z | ||
86bef2d | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2023-12-19T23:58:55 | ||
ca967d8 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 28 | 2023-12-17T13:45:54+01:00 | ||
1f92014 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Bubaak | 3 | 2023-12-05T08:13:45Z | ||
a644f1d | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Bubaak | 3 | 2023-12-04T14:57:49Z |
Found 19 witnesses for program sv-benchmarks/c/termination-memory-alloca/HarrisLalNoriRajamani-2010SAS-Fig1-alloca_true-termination.c.i, 7d44dc9ee297680f321b2cf4dcd79f3ba6ced2470ed6439fc6dd5eb0285efc9c
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/7d44dc9ee297680f321b2cf4dcd79f3ba6ced2470ed6439fc6dd5eb0285efc9c.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
f6f3f82 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2022-12-09T06:27:25+01:00 | ||
c7be182 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 8 | 2023-01-28T14:21:11+01:00 | f6f3f82 | |
e098642 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 8 | 2022-12-10T18:44:30+01:00 | ||
eb912fe | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2.1-svn-1715bd67dc+ | 8 | 2022-12-11T20:46:18+01:00 | ||
5ce227c | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 8 | 2022-12-10T02:47:23+01:00 | ||
7a3bbca | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-38892M | 14 | 2022-12-09T03:08:10+01:00 | ||
40f8fe1 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Bubaak | 3 | 2022-12-08T18:20:32Z | ||
0061b57 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 7.0.0 incr | 3 | 2022-12-18T23:53:26Z | ||
d759801 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 6.8.0 incr | 3 | 2022-12-25T11:38:44Z | ||
3159dca | 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 | 24 | 2022-12-14T14:31:59Z | ||
3243c2e | 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-11T11:01:24Z | ||
4c5204c | 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 | 28 | 2022-12-08T10:21:29+01:00 | ||
87e64ae | 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 | 24 | 2022-12-13T10:27:11Z | ||
3e76195 | Inspect | CHECK( init(main()), LTL(G ! call(reach_error())) ) | correctness_witness | ESBMC 6.8.0 | 3 | 2022-12-25T10:19:42Z | ||
30a7f44 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 7.0.0 | 3 | 2022-12-18T21:35:34Z | ||
bf3931d | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 3 | 2022-12-12T16:58:34Z | ||
379cdff | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2022-12-11T15:53:01 | ||
b45db09 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 28 | 2022-12-08T04:57:36+01:00 | ||
abae008 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Bubaak | 3 | 2022-12-08T16:06:53Z |
Found 4 witnesses for program sv-benchmarks/c/termination-memory-alloca/HarrisLalNoriRajamani-2010SAS-Fig1-alloca_true-termination.c.i, 7d44dc9ee297680f321b2cf4dcd79f3ba6ced2470ed6439fc6dd5eb0285efc9c
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/7d44dc9ee297680f321b2cf4dcd79f3ba6ced2470ed6439fc6dd5eb0285efc9c.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
eed5ddb | Inspect | CHECK( init(main()), LTL(G ! call(reach_error())) ) | correctness_witness | ESBMC 6.8.0 | 3 | 2021-12-08T04:51:41Z | ||
68ad8ca | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 3 | 2021-12-07T15:33:05Z | ||
57f3293 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2021-12-09T07:45:30 | ||
5057fdc | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 24 | 2021-12-06T03:13:27+01:00 |
Found 3 witnesses for program sv-benchmarks/c/termination-memory-alloca/HarrisLalNoriRajamani-2010SAS-Fig1-alloca_true-termination.c.i, 7d44dc9ee297680f321b2cf4dcd79f3ba6ced2470ed6439fc6dd5eb0285efc9c
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/7d44dc9ee297680f321b2cf4dcd79f3ba6ced2470ed6439fc6dd5eb0285efc9c.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
d1b48fc | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2020-12-11T21:24:49 | ||
6938c66 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2020-12-08T19:13:05 | ||
da85dbc | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2020-12-08T08:45:12 |
Found 1 witnesses for program sv-benchmarks/c/termination-memory-alloca/HarrisLalNoriRajamani-2010SAS-Fig1-alloca_true-termination.c.i, 7d44dc9ee297680f321b2cf4dcd79f3ba6ced2470ed6439fc6dd5eb0285efc9c
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/7d44dc9ee297680f321b2cf4dcd79f3ba6ced2470ed6439fc6dd5eb0285efc9c.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
1da4a29 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2019-12-03T22:37 CET (comp) |
Found 2 witnesses for program sv-benchmarks/c/termination-memory-alloca/HarrisLalNoriRajamani-2010SAS-Fig1-alloca_true-termination.c.i, 7d44dc9ee297680f321b2cf4dcd79f3ba6ced2470ed6439fc6dd5eb0285efc9c
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/7d44dc9ee297680f321b2cf4dcd79f3ba6ced2470ed6439fc6dd5eb0285efc9c.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
cd00c2c | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T14:22 CET (sv-comp) | ||
b49f5c8 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2018-12-06T21:18 CET (sv-comp) |
Found 4 witnesses for program sv-benchmarks/c/termination-memory-alloca/HarrisLalNoriRajamani-2010SAS-Fig1-alloca_true-termination.c.i, 7d44dc9ee297680f321b2cf4dcd79f3ba6ced2470ed6439fc6dd5eb0285efc9c
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/7d44dc9ee297680f321b2cf4dcd79f3ba6ced2470ed6439fc6dd5eb0285efc9c.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
7e05550 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T20:43:29.500841 | ||
feb1e78 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T14:05:25.742535 | ||
1d4402a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 3.1 | 14 | 2017-12-01T16:31 CET (sv-comp) | ||
6f5d61a | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 25 | 2017-12-01T15:31 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/termination-memory-alloca/HarrisLalNoriRajamani-2010SAS-Fig1-alloca_true-termination.c.i, 7d44dc9ee297680f321b2cf4dcd79f3ba6ced2470ed6439fc6dd5eb0285efc9c
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/7d44dc9ee297680f321b2cf4dcd79f3ba6ced2470ed6439fc6dd5eb0285efc9c.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |