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/twisted-alloca_true-termination.c.i |
programSHA | e028c51cfa02b345902e1292d1a644c7ee4a15183825ee6e2ec2fc316df147e6 |
witnessName | results-verified/cbmc-path.2018-12-04_2245.logfiles/sv-comp19_prop-termination.twisted-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 23 witnesses for program sv-benchmarks/c/termination-memory-alloca/twisted-alloca_true-termination.c.i, e028c51cfa02b345902e1292d1a644c7ee4a15183825ee6e2ec2fc316df147e6
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/e028c51cfa02b345902e1292d1a644c7ee4a15183825ee6e2ec2fc316df147e6.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
3263902 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2023-12-18T09:09:04+01:00 | ||
37ded22 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 3 | 2023-11-29T22:23:46Z | ||
232335a | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-18T12:04:33+01:00 | 3263902 | |
c98f336 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-11-30T08:51:18+01:00 | ||
6280348 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2.1-svn-e677b7cd46+ | 6 | 2023-12-03T22:08:53+01:00 | ||
8cfe971 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-38892M | 10 | 2023-12-18T02:05:49+01:00 | ||
d507abc | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Bubaak | 3 | 2023-12-05T07:18:05Z | ||
aa843bb | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Bubaak | 3 | 2023-12-04T13:24:24Z | ||
9d87ee4 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Bubaak | 3 | 2023-12-01T20:23:30Z | ||
71425f9 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 7.4.0 incr | 3 | 2023-12-01T10:46:49Z | ||
4d4deb0 | 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 | 21 | 2023-12-02T12:59:55Z | ||
8ac2b74 | 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:46Z | ||
35c57d4 | 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-29T16:15:27Z | ||
f743777 | 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 | 21 | 2023-12-02T20:07:10Z | ||
2984dd1 | 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) | 12 | 2023-12-01T02:03:18Z | ||
42daf6d | 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 | 13 | 2023-12-17T10:36:02+01:00 | ||
240f6a8 | 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 | 21 | 2023-11-28T19:20:47Z | ||
953e57f | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 6 | 2023-12-19T01:07:48+01:00 | ||
044ca1a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 7.4.0 | 3 | 2023-12-01T03:19:58Z | ||
4e7f473 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 3 | 2023-11-29T23:28:06Z | ||
bc6344e | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2023-12-19T21:15:56 | ||
e743c67 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 13 | 2023-12-17T12:32:30+01:00 | ||
c5b065e | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Bubaak | 3 | 2023-12-01T21:05:06Z |
Found 20 witnesses for program sv-benchmarks/c/termination-memory-alloca/twisted-alloca_true-termination.c.i, e028c51cfa02b345902e1292d1a644c7ee4a15183825ee6e2ec2fc316df147e6
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/e028c51cfa02b345902e1292d1a644c7ee4a15183825ee6e2ec2fc316df147e6.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
0bab5dc | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2022-12-09T06:45:03+01:00 | ||
6872430 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-28T14:14:49+01:00 | 0bab5dc | |
0d3cd8f | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 6 | 2022-12-10T14:59:38+01:00 | ||
009a90a | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2.1-svn-1715bd67dc+ | 6 | 2022-12-11T20:24:29+01:00 | ||
8ae1cf6 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 6 | 2022-12-10T03:43:24+01:00 | ||
271ba87 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-38892M | 10 | 2022-12-09T03:26:56+01:00 | ||
5760ea0 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Bubaak | 3 | 2022-12-08T13:03:09Z | ||
b7d60fe | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 7.0.0 incr | 3 | 2022-12-18T16:52:42Z | ||
4aac126 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 6.8.0 incr | 3 | 2022-12-25T11:32:12Z | ||
e9d633d | 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 | 20 | 2022-12-14T13:43:29Z | ||
0e1c273 | 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-11T12:20:35Z | ||
3845299 | 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 | 20 | 2022-12-15T00:00:52Z | ||
ab22711 | 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 | 13 | 2022-12-08T04:53:42+01:00 | ||
3b00ebb | 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 | 20 | 2022-12-13T10:21:37Z | ||
b4415c7 | Inspect | CHECK( init(main()), LTL(G ! call(reach_error())) ) | correctness_witness | ESBMC 6.8.0 | 3 | 2022-12-25T12:16:58Z | ||
504483e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 7.0.0 | 3 | 2022-12-18T23:35:27Z | ||
4312417 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 3 | 2022-12-12T16:08:40Z | ||
cf43a39 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2022-12-11T18:02:04 | ||
6402d08 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 13 | 2022-12-08T08:08:00+01:00 | ||
1ce6ed0 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Bubaak | 3 | 2022-12-08T17:36:38Z |
Found 4 witnesses for program sv-benchmarks/c/termination-memory-alloca/twisted-alloca_true-termination.c.i, e028c51cfa02b345902e1292d1a644c7ee4a15183825ee6e2ec2fc316df147e6
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/e028c51cfa02b345902e1292d1a644c7ee4a15183825ee6e2ec2fc316df147e6.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
40b2b46 | Inspect | CHECK( init(main()), LTL(G ! call(reach_error())) ) | correctness_witness | ESBMC 6.8.0 | 3 | 2021-12-08T03:37:38Z | ||
aa5a918 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 3 | 2021-12-07T12:19:48Z | ||
162eb92 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2021-12-09T07:07:32 | ||
82701b5 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 11 | 2021-12-06T10:05:32+01:00 |
Found 3 witnesses for program sv-benchmarks/c/termination-memory-alloca/twisted-alloca_true-termination.c.i, e028c51cfa02b345902e1292d1a644c7ee4a15183825ee6e2ec2fc316df147e6
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/e028c51cfa02b345902e1292d1a644c7ee4a15183825ee6e2ec2fc316df147e6.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
3c4e291 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2020-12-11T14:29:36 | ||
4837b7a | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2020-12-08T20:13:16 | ||
82cb86a | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2020-12-08T09:05:32 |
Found 1 witnesses for program sv-benchmarks/c/termination-memory-alloca/twisted-alloca_true-termination.c.i, e028c51cfa02b345902e1292d1a644c7ee4a15183825ee6e2ec2fc316df147e6
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/e028c51cfa02b345902e1292d1a644c7ee4a15183825ee6e2ec2fc316df147e6.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
37eaaa4 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2019-12-04T01:13 CET (comp) |
Found 2 witnesses for program sv-benchmarks/c/termination-memory-alloca/twisted-alloca_true-termination.c.i, e028c51cfa02b345902e1292d1a644c7ee4a15183825ee6e2ec2fc316df147e6
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/e028c51cfa02b345902e1292d1a644c7ee4a15183825ee6e2ec2fc316df147e6.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
0686f61 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T12:40 CET (sv-comp) | ||
e6ae084 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2018-12-07T05:12 CET (sv-comp) |
Found 4 witnesses for program sv-benchmarks/c/termination-memory-alloca/twisted-alloca_true-termination.c.i, e028c51cfa02b345902e1292d1a644c7ee4a15183825ee6e2ec2fc316df147e6
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/e028c51cfa02b345902e1292d1a644c7ee4a15183825ee6e2ec2fc316df147e6.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
f213331 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-03T02:19:58.587222 | ||
b8acfc1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T10:28:11.584394 | ||
bb32eb4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 3.1 | 7 | 2017-12-01T18:34 CET (sv-comp) | ||
ccb0767 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 12 | 2017-12-01T18:06 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/termination-memory-alloca/twisted-alloca_true-termination.c.i, e028c51cfa02b345902e1292d1a644c7ee4a15183825ee6e2ec2fc316df147e6
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/e028c51cfa02b345902e1292d1a644c7ee4a15183825ee6e2ec2fc316df147e6.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |