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-crafted/NestedRecursion_1d_true-no-overflow_true-termination_true-valid-memsafety.c |
programSHA | 9c9c032ca120503dfa93615a57a0bb47775014248f579f3a3fd38a4985b2298b |
witnessName | results-verified/depthk.2018-12-05_0936.logfiles/sv-comp19_prop-termination.NestedRecursion_1d_true-no-overflow_true-termination_true-valid-memsafety.c.files/witness.graphml |
witnessSHA | bc6329610723f563ebf2ca7b7a8a760a33c64a99f38db6d2bf711b9246c34981 |
Key | Value |
architecture | 32bit |
creationtime | 2018-12-05T17:02:45.478129 |
producer | DepthK v3.0 |
programfile | /tmp/vcloud-vcloud-master/worker/working_dir_0322bec2-5d64-467e-824e-9158ea77ccf8/sv-benchmarks/c/termination-crafted/NestedRecursion_1d_true-no-overflow_true-termination_true-valid-memsafety.c |
programhash | 0837a1e1d82be1b28ccf3514392f1b01c88a9160 |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/bc6329610723f563ebf2ca7b7a8a760a33c64a99f38db6d2bf711b9246c34981.graphml |
witness-sha256 | bc6329610723f563ebf2ca7b7a8a760a33c64a99f38db6d2bf711b9246c34981 |
witness-size | 3520 |
witness-type | correctness_witness |
Found 17 witnesses for program sv-benchmarks/c/termination-crafted/NestedRecursion_1d_true-no-overflow_true-termination_true-valid-memsafety.c, 9c9c032ca120503dfa93615a57a0bb47775014248f579f3a3fd38a4985b2298b
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/9c9c032ca120503dfa93615a57a0bb47775014248f579f3a3fd38a4985b2298b.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
1ebbec3 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | frama-c-sv version 0.4.0 | 3 | 2023-12-03T06:03:15Z | ||
c2d4f3f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | sv-comp-24 | 4 | 2023-12-03T17:46:48+01:00 | ||
b1a5123 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | VeriOover | 1 | 2023-12-20T03:37 CET (comp) | ||
bd3722e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Taipan | 13 | 2023-12-02T07:29:30Z | ||
ff9dfae | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Pinaka | 3 | 2023-12-19T19:32:06 | ||
79546a1 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 7 | 2023-12-20T03:55:26+01:00 | b1a5123 | |
5d8f449 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 7 | 2023-12-20T02:46:40+01:00 | ff9dfae | |
96d46a9 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 7 | 2023-12-03T18:44:28+01:00 | c2d4f3f | |
1eee9c2 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 7 | 2023-12-03T10:01:50+01:00 | 1ebbec3 | |
50e0f2c | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 7 | 2023-11-30T07:00:03+01:00 | ||
586cb5e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2.1-svn-e677b7cd46+ | 7 | 2023-12-03T20:57:54+01:00 | ||
6e614b3 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 7 | 2023-12-19T01:18:29+01:00 | ||
74d1750 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Automizer | 13 | 2023-11-29T04:07:34Z | ||
aad5ca2 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 2.1 | 7 | 2023-12-17T00:01:49+01:00 | ||
2c42124 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 7 | 2023-12-18T18:58:21+01:00 | ||
5af923c | Inspect | - entry_type: invariant_set metadata: format_version: '2.0' uuid: dce7c09d-cb4c-4e6b-91cd-021664e0e8de creation_time: '2023-11-29T05:07:34+01:00' producer: name: Automizer version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_91cfbc73-7fb7-407f-b97b-75a715f375bb/sv-benchmarks/c/termination-crafted/NestedRecursion_1d.c input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_91cfbc73-7fb7-407f-b97b-75a715f375bb/sv-benchmarks/c/termination-crafted/NestedRecursion_1d.c : 9c9c032ca120503dfa93615a57a0bb47775014248f579f3a3fd38a4985b2298b specification: |+ CHECK( init(main()), LTL(G ! overflow) ) data_model: 64bit language: C content: [ ] | correctness_witness | CPAchecker 2.3 | 8 | 2023-11-29T07:57:35+01:00 | ||
a40e3ec | Inspect | - entry_type: invariant_set metadata: format_version: '2.0' uuid: 36dc607b-a17c-42d3-90d5-bef38659f4e2 creation_time: '2023-12-02T08:29:30+01:00' producer: name: Taipan version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_4cde9bf1-6227-4cdb-bba9-110d669832fe/sv-benchmarks/c/termination-crafted/NestedRecursion_1d.c input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_4cde9bf1-6227-4cdb-bba9-110d669832fe/sv-benchmarks/c/termination-crafted/NestedRecursion_1d.c : 9c9c032ca120503dfa93615a57a0bb47775014248f579f3a3fd38a4985b2298b specification: |+ CHECK( init(main()), LTL(G ! overflow) ) data_model: 64bit language: C content: [ ] | correctness_witness | CPAchecker 2.3 | 8 | 2023-12-04T12:11:49+01:00 |
Found 11 witnesses for program sv-benchmarks/c/termination-crafted/NestedRecursion_1d_true-no-overflow_true-termination_true-valid-memsafety.c, 9c9c032ca120503dfa93615a57a0bb47775014248f579f3a3fd38a4985b2298b
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/9c9c032ca120503dfa93615a57a0bb47775014248f579f3a3fd38a4985b2298b.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
7380941 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | frama-c-sv version 0.4.0 | 3 | 2022-12-09T13:50:36Z | ||
4745de4 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | sv-comp-22 | 4 | 2022-12-11T01:52:17+01:00 | ||
b1a5123 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | VeriOover | 1 | 2022-12-12T11:00 CET (comp) | ||
81d39ac | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Taipan | 13 | 2022-12-14T04:31:12Z | ||
fc8f3c3 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Pinaka | 3 | 2022-12-11T15:02:07 | ||
499926d | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 7 | 2023-01-29T11:45:44+01:00 | b1a5123 | |
a864010 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 7 | 2023-01-29T11:19:08+01:00 | 81d39ac | |
d07856e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 7 | 2023-01-28T17:47:26+01:00 | 7380941 | |
375c49c | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Automizer | 13 | 2022-12-13T17:03:14Z | ||
84f326c | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 2.1 | 7 | 2022-12-25T12:29:06+01:00 | ||
aca441c | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 7 | 2022-12-10T04:13:44+01:00 |
Found 14 witnesses for program sv-benchmarks/c/termination-crafted/NestedRecursion_1d_true-no-overflow_true-termination_true-valid-memsafety.c, 9c9c032ca120503dfa93615a57a0bb47775014248f579f3a3fd38a4985b2298b
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/9c9c032ca120503dfa93615a57a0bb47775014248f579f3a3fd38a4985b2298b.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
18b4655 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | frama-c-sv version 0.2.8 | 3 | 2021-12-13T20:15:01Z | ||
873253d | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | sv-comp-22 | 4 | 2021-12-06T13:35:51+01:00 | ||
907d30e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Taipan | 13 | 2021-12-10T05:54:48Z | ||
a08568d | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Pinaka | 3 | 2021-12-09T05:10:11 | ||
689c460 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 7 | 2021-12-09T10:19:39+01:00 | a08568d | |
978ace0 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 7 | 2021-12-07T02:55:22+01:00 | ef7dca7 | |
c2d8e7f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 7 | 2021-12-06T15:19:28+01:00 | 873253d | |
383f43b | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 7 | 2021-12-05T15:11:53+01:00 | ||
e91766d | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0.1-svn-eda176372c+ | 7 | 2021-12-09T12:38:25+01:00 | ||
ef7dca7 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Automizer | 13 | 2021-12-06T16:48:11Z | ||
b36689f | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 2.1 | 7 | 2021-12-05T17:43:25+01:00 | ||
e91958e | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 2.0.1-svn-fe6f522dd3+ | 7 | 2021-12-08T19:30:02+01:00 | ||
dc73c3c | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 2.0.1-svn-eda176372c+ | 7 | 2021-12-09T12:55:21+01:00 | ||
b09c893 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2021-12-10T17:12:33 |
Found 10 witnesses for program sv-benchmarks/c/termination-crafted/NestedRecursion_1d_true-no-overflow_true-termination_true-valid-memsafety.c, 9c9c032ca120503dfa93615a57a0bb47775014248f579f3a3fd38a4985b2298b
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/9c9c032ca120503dfa93615a57a0bb47775014248f579f3a3fd38a4985b2298b.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
8faa632 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | frama-c-sv version 0.2.1 | 3 | 2020-12-06T23:35:12 | ||
a994010 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Pinaka | 3 | 2020-12-08T05:36:07 | ||
b7aa08a | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0 | 7 | 2020-12-09T21:46:55+01:00 | 0447fa7 | |
e07c8b5 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0 | 7 | 2020-12-09T02:43:18+01:00 | e2f0356 | |
6d52027 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0 | 7 | 2020-12-08T14:09:42+01:00 | a994010 | |
4393eef | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0.1-svn-eda176372c+ | 7 | 2020-12-08T05:39:20+01:00 | ||
2fb70cf | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 2.0 | 7 | 2020-12-05T15:39:25+01:00 | ||
30e5590 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 2.0.1-svn-eda176372c+ | 7 | 2020-12-07T22:29:57+01:00 | ||
05ea0b4 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2020-12-11T19:53:45 | ||
8dc003b | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2020-12-09T00:28:00 |
Found 2 witnesses for program sv-benchmarks/c/termination-crafted/NestedRecursion_1d_true-no-overflow_true-termination_true-valid-memsafety.c, 9c9c032ca120503dfa93615a57a0bb47775014248f579f3a3fd38a4985b2298b
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/9c9c032ca120503dfa93615a57a0bb47775014248f579f3a3fd38a4985b2298b.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
d8179ff | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.9 | 6 | 2019-11-30T07:03:38+01:00 | ||
c51be09 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 6 | 2019-12-01T00:49:07+01:00 |
Found 2 witnesses for program sv-benchmarks/c/termination-crafted/NestedRecursion_1d_true-no-overflow_true-termination_true-valid-memsafety.c, 9c9c032ca120503dfa93615a57a0bb47775014248f579f3a3fd38a4985b2298b
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/9c9c032ca120503dfa93615a57a0bb47775014248f579f3a3fd38a4985b2298b.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
9d819f0 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | SMACK 1.9.3 | 3 | 2018-12-08T12:40:34 | ||
c5db536 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 216 | 2018-12-08T03:40:52+01:00 |
Found 4 witnesses for program sv-benchmarks/c/termination-crafted/NestedRecursion_1d_true-no-overflow_true-termination_true-valid-memsafety.c, 9c9c032ca120503dfa93615a57a0bb47775014248f579f3a3fd38a4985b2298b
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/9c9c032ca120503dfa93615a57a0bb47775014248f579f3a3fd38a4985b2298b.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
2098090 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Taipan | 13 | 2017-12-03T07:43Z | ||
62a395a | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | ESBMC 3.1 | 11 | 2017-12-01T14:34 CET (sv-comp) | ||
62b60d3 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Automizer | 13 | 2017-12-03T10:17Z | ||
2e88af5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 3.1 | 11 | 2017-12-01T17:27 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/termination-crafted/NestedRecursion_1d_true-no-overflow_true-termination_true-valid-memsafety.c, 9c9c032ca120503dfa93615a57a0bb47775014248f579f3a3fd38a4985b2298b
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/9c9c032ca120503dfa93615a57a0bb47775014248f579f3a3fd38a4985b2298b.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |