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).
Found 29 witnesses for program sv-benchmarks/c/termination-libowfat/strcat_true-termination.c.i, 02cb0b7d003c65b862775c945403a999f88317049d254b45ea895999d5c859dc
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/02cb0b7d003c65b862775c945403a999f88317049d254b45ea895999d5c859dc.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
c0e899f | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2023-12-18T10:31:16+01:00 | ||
a994ef6 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 3 | 2023-11-29T20:23:32Z | ||
6b37338 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 11 | 2023-12-18T12:03:18+01:00 | c0e899f | |
3559949 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 11 | 2023-12-17T22:09:03+01:00 | b188c53 | |
7a720f3 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 11 | 2023-12-05T14:37:30+01:00 | 566d8dd | |
036518d | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 11 | 2023-12-04T16:45:53+01:00 | 66cfb01 | |
3911a4b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 11 | 2023-12-04T12:13:23+01:00 | ec14234 | |
d2d593f | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 11 | 2023-12-03T06:18:25+01:00 | b7540ad | |
fbfe210 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 11 | 2023-12-01T22:54:16+01:00 | 90a0548 | |
9e612d2 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 11 | 2023-12-01T18:29:09+01:00 | db8ef81 | |
900733c | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 11 | 2023-11-30T09:44:16+01:00 | 26b3216 | |
ba62666 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 11 | 2023-11-30T08:18:51+01:00 | ||
6752224 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 11 | 2023-11-30T03:05:45+01:00 | a994ef6 | |
56f5108 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 11 | 2023-11-29T08:33:14+01:00 | ab04c77 | |
15c8169 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 11 | 2023-11-28T23:49:36+01:00 | 4cd8359 | |
ab7b955 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2.1-svn-e677b7cd46+ | 11 | 2023-12-03T20:26:14+01:00 | ||
9473fed | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-38892M | 18 | 2023-12-18T02:05:23+01:00 | ||
db8ef81 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 7.4.0 incr | 5 | 2023-12-01T16:48:53Z | ||
1fb5897 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 11 | 2023-12-19T02:10:04+01:00 | ||
ec14234 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Taipan | 7 | 2023-12-02T18:05:31Z | ||
b7540ad | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Kojak | 7 | 2023-12-02T20:46:32Z | ||
b188c53 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CBMC | 6 | 2023-12-17T09:28:23+01:00 | ||
ab04c77 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Automizer | 7 | 2023-11-29T03:44:14Z | ||
4cd8359 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | sv-sanitizers 0.1.1 | 3 | 2023-11-28T21:57:14Z | ||
26b3216 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | PredatorHP | 4 | 2023-11-30T08:26:03Z | ||
566d8dd | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | Bubaak | 3 | 2023-12-05T11:18:06Z | ||
66cfb01 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | Bubaak | 3 | 2023-12-04T12:37:32Z | ||
90a0548 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | Bubaak | 3 | 2023-12-01T20:25:24Z | ||
fce3888 | Inspect | - content: - segment: - waypoint: action: follow constraint: format: C value: \result == 1 location: column: 38 file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_96cbff59-3ce2-45bd-b0e4-7cbf2ccfa1b1/sv-benchmarks/c/termination-dietlibc/strcat.i line: 525 type: function_return - segment: - waypoint: action: follow constraint: format: C value: \result == 1 location: column: 39 file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_96cbff59-3ce2-45bd-b0e4-7cbf2ccfa1b1/sv-benchmarks/c/termination-dietlibc/strcat.i line: 529 type: function_return - segment: - waypoint: action: follow constraint: format: C value: \result == 2147483647 location: column: 39 file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_96cbff59-3ce2-45bd-b0e4-7cbf2ccfa1b1/sv-benchmarks/c/termination-dietlibc/strcat.i line: 531 type: function_return - segment: - waypoint: action: follow location: column: 3 file_name: vcloud_worker_vcloud-master_on_vcloud-master/run_dir_96cbff59-3ce2-45bd-b0e4-7cbf2ccfa1b1/sv-benchmarks/c/termination-dietlibc/strcat.i line: 534 type: target entry_type: violation_sequence metadata: creation_time: '2023-11-29T20:23:32Z' format_version: '0.1' producer: name: symbiotic task: data_model: LP64 input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_96cbff59-3ce2-45bd-b0e4-7cbf2ccfa1b1/sv-benchmarks/c/termination-dietlibc/strcat.i : 02cb0b7d003c65b862775c945403a999f88317049d254b45ea895999d5c859dc input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_96cbff59-3ce2-45bd-b0e4-7cbf2ccfa1b1/sv-benchmarks/c/termination-dietlibc/strcat.i language: C specification: CHECK( init(main()), LTL(G valid-free) ),CHECK( init(main()), LTL(G valid-deref) ),CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 13 | 2023-11-30T02:56:29+01:00 |
Found 23 witnesses for program sv-benchmarks/c/termination-libowfat/strcat_true-termination.c.i, 02cb0b7d003c65b862775c945403a999f88317049d254b45ea895999d5c859dc
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/02cb0b7d003c65b862775c945403a999f88317049d254b45ea895999d5c859dc.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
1717e01 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2022-12-09T07:02:27+01:00 | ||
cfd4e0c | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 3 | 2022-12-12T10:50:15Z | ||
18896ce | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 6 | 2023-01-29T05:56:39+01:00 | cfd4e0c | |
72bedfd | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 6 | 2023-01-28T00:30:20+01:00 | b56fb4e | |
247cc51 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 11 | 2023-01-29T10:44:33+01:00 | c329d75 | |
d9582fb | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 11 | 2023-01-29T06:54:25+01:00 | a294e94 | |
d332bcc | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 11 | 2023-01-29T06:38:44+01:00 | 6b7db67 | |
dc4c77f | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 11 | 2023-01-29T04:19:18+01:00 | cdea870 | |
6d811db | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 11 | 2023-01-28T15:43:59+01:00 | 43b9244 | |
1d52d99 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 11 | 2023-01-28T14:17:19+01:00 | 1717e01 | |
2b61b17 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 11 | 2023-01-28T04:21:41+01:00 | 73948e6 | |
0f1f652 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 11 | 2023-01-28T02:25:23+01:00 | c07b8c4 | |
a10bf1b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 11 | 2022-12-10T15:34:47+01:00 | ||
d9f990c | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2.1-svn-1715bd67dc+ | 11 | 2022-12-11T21:15:17+01:00 | ||
d26e4fa | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-38892M | 18 | 2022-12-09T03:02:28+01:00 | ||
43b9244 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 7.0.0 incr | 4 | 2022-12-18T23:50:00Z | ||
c07b8c4 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 6.8.0 incr | 4 | 2022-12-25T10:45:46Z | ||
c329d75 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Taipan | 7 | 2022-12-14T12:32:47Z | ||
6b7db67 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Kojak | 7 | 2022-12-14T23:41:27Z | ||
73948e6 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CBMC | 6 | 2022-12-08T06:00:55+01:00 | ||
a294e94 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Automizer | 7 | 2022-12-13T21:12:10Z | ||
b56fb4e | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | Bubaak | 3 | 2022-12-08T19:23:06Z | ||
4b03497 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 11 | 2022-12-10T02:48:52+01:00 |
Found 1 witnesses for program sv-benchmarks/c/termination-libowfat/strcat_true-termination.c.i, 02cb0b7d003c65b862775c945403a999f88317049d254b45ea895999d5c859dc
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/02cb0b7d003c65b862775c945403a999f88317049d254b45ea895999d5c859dc.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
3c37528 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2021-12-10T17:23:47 |
Found 2 witnesses for program sv-benchmarks/c/termination-libowfat/strcat_true-termination.c.i, 02cb0b7d003c65b862775c945403a999f88317049d254b45ea895999d5c859dc
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/02cb0b7d003c65b862775c945403a999f88317049d254b45ea895999d5c859dc.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
743b82b | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2020-12-11T16:28:56 | ||
da135f5 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2020-12-08T17:36:57 |
Found 0 witnesses for program sv-benchmarks/c/termination-libowfat/strcat_true-termination.c.i, 02cb0b7d003c65b862775c945403a999f88317049d254b45ea895999d5c859dc
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/02cb0b7d003c65b862775c945403a999f88317049d254b45ea895999d5c859dc.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/termination-libowfat/strcat_true-termination.c.i, 02cb0b7d003c65b862775c945403a999f88317049d254b45ea895999d5c859dc
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/02cb0b7d003c65b862775c945403a999f88317049d254b45ea895999d5c859dc.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/termination-libowfat/strcat_true-termination.c.i, 02cb0b7d003c65b862775c945403a999f88317049d254b45ea895999d5c859dc
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/02cb0b7d003c65b862775c945403a999f88317049d254b45ea895999d5c859dc.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/termination-libowfat/strcat_true-termination.c.i, 02cb0b7d003c65b862775c945403a999f88317049d254b45ea895999d5c859dc
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/02cb0b7d003c65b862775c945403a999f88317049d254b45ea895999d5c859dc.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |