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 31 witnesses for program sv-benchmarks/c/termination-libowfat/strpbrk_true-termination.c.i, edf491a8dfccfa6378da1f67984511795182afc470c7adf35a0acc959fae5609
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/edf491a8dfccfa6378da1f67984511795182afc470c7adf35a0acc959fae5609.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
5591318 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | sv-comp-24 | 4 | 2023-12-03T17:58:32+01:00 | ||
70544d5 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | frama-c-sv version 0.4.0 | 3 | 2023-12-03T04:16:15Z | ||
5ef20ee | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Taipan | 15 | 2023-12-02T13:49:40Z | ||
9ee3ff1 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Symbiotic | 3 | 2023-12-17T04:17:28Z | ||
2d5482f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Symbiotic | 3 | 2023-11-29T23:24:35Z | ||
b8ea4f1 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Pinaka | 3 | 2023-12-19T20:48:36 | ||
db9a241 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Kojak | 15 | 2023-12-03T00:47:57Z | ||
4f08e75 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Goblint (tags/svcomp24-0-gc2e9465a7) | 9 | 2023-11-30T22:36:01Z | ||
268f04c | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 8 | 2023-12-20T02:30:27+01:00 | b8ea4f1 | |
2495183 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 8 | 2023-12-19T14:31:23+01:00 | fd6c56d | |
0ce67c7 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 8 | 2023-12-19T04:13:24+01:00 | 9f587cb | |
a2a8dfb | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 8 | 2023-12-17T06:10:09+01:00 | 9ee3ff1 | |
b90ab0c | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 8 | 2023-12-04T11:27:47+01:00 | 5ef20ee | |
8e69997 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 8 | 2023-12-04T01:39:20+01:00 | aa4ff6e | |
0d71cf1 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 8 | 2023-12-03T18:36:39+01:00 | 5591318 | |
c09f695 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 8 | 2023-12-03T09:53:58+01:00 | 70544d5 | |
d314695 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 8 | 2023-12-03T06:00:58+01:00 | db9a241 | |
3d40bfd | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 8 | 2023-12-01T03:50:35+01:00 | 4f08e75 | |
54c7d7b | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 8 | 2023-11-30T12:26:18+01:00 | 1dfde87 | |
1dfde87 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 8 | 2023-11-30T08:36:35+01:00 | ||
45ee781 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 8 | 2023-11-30T02:38:41+01:00 | 2d5482f | |
7f298fd | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 8 | 2023-11-29T07:52:18+01:00 | 127256f | |
aa4ff6e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2.1-svn-e677b7cd46+ | 8 | 2023-12-03T21:28:29+01:00 | ||
fd6c56d | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0 | 8 | 2023-12-19T12:52:47+01:00 | ||
9f587cb | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 8 | 2023-12-19T01:52:24+01:00 | ||
127256f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Automizer | 15 | 2023-11-29T01:10:14Z | ||
7c695c4 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Goblint (tags/svcomp24-0-gc2e9465a7) | 3 | 2023-12-01T01:01:46Z | ||
4b570ab | Inspect | - entry_type: invariant_set metadata: format_version: '2.0' uuid: c1db75df-b8c4-4623-ad37-42d2a88319a5 creation_time: '2023-12-02T14:49:40+01:00' producer: name: Taipan version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_8ca10637-2479-41e5-9b7c-02e9ff0ede21/sv-benchmarks/c/termination-dietlibc/strpbrk.i input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_8ca10637-2479-41e5-9b7c-02e9ff0ede21/sv-benchmarks/c/termination-dietlibc/strpbrk.i : edf491a8dfccfa6378da1f67984511795182afc470c7adf35a0acc959fae5609 specification: |+ CHECK( init(main()), LTL(G ! overflow) ) data_model: 64bit language: C content: [ ] | correctness_witness | CPAchecker 2.3 | 9 | 2023-12-04T11:56:33+01:00 | ||
0b4b344 | Inspect | - entry_type: invariant_set metadata: format_version: '2.0' uuid: bf1b0add-02dc-42de-b7ec-3bf9be26dc93 creation_time: '2023-11-29T02:10:14+01:00' producer: name: Automizer version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_7615f5b5-3fea-45e0-9eff-b266a3361457/sv-benchmarks/c/termination-dietlibc/strpbrk.i input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_7615f5b5-3fea-45e0-9eff-b266a3361457/sv-benchmarks/c/termination-dietlibc/strpbrk.i : edf491a8dfccfa6378da1f67984511795182afc470c7adf35a0acc959fae5609 specification: |+ CHECK( init(main()), LTL(G ! overflow) ) data_model: 64bit language: C content: [ ] | correctness_witness | CPAchecker 2.3 | 9 | 2023-11-29T07:48:39+01:00 | ||
5c4c7a5 | Inspect | - entry_type: invariant_set metadata: format_version: '2.0' uuid: 05129f7e-5b1c-4be0-9767-57d51cfa010b creation_time: '2023-12-03T01:47:57+01:00' producer: name: Kojak version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_f72adba6-4aab-4202-a466-40f5fe95a8c9/sv-benchmarks/c/termination-dietlibc/strpbrk.i input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_f72adba6-4aab-4202-a466-40f5fe95a8c9/sv-benchmarks/c/termination-dietlibc/strpbrk.i : edf491a8dfccfa6378da1f67984511795182afc470c7adf35a0acc959fae5609 specification: |+ CHECK( init(main()), LTL(G ! overflow) ) data_model: 64bit language: C content: [ ] | correctness_witness | CPAchecker 2.3 | 9 | 2023-12-03T05:45:58+01:00 | ||
965cee5 | Inspect | - entry_type: invariant_set metadata: format_version: "2.0" uuid: 5f8d39e2-08cb-4c8a-b582-f9f61b683ab9 creation_time: 2023-11-30T22:36:01Z producer: name: Goblint version: tags/svcomp24-0-gc2e9465a7 command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--sets'' ''ana.specification'' ''../../sv-benchmarks/c/properties/no-overflow.prp'' ''--sets'' ''exp.architecture'' ''64bit'' ''../../sv-benchmarks/c/termination-dietlibc/strpbrk.i''' task: input_files: - ../../sv-benchmarks/c/termination-dietlibc/strpbrk.i input_file_hashes: ../../sv-benchmarks/c/termination-dietlibc/strpbrk.i: edf491a8dfccfa6378da1f67984511795182afc470c7adf35a0acc959fae5609 data_model: LP64 language: C specification: CHECK( init(main()), LTL(G ! overflow) ) content: [] | correctness_witness | CPAchecker 2.3 | 9 | 2023-12-01T05:05:27+01:00 |
Found 26 witnesses for program sv-benchmarks/c/termination-libowfat/strpbrk_true-termination.c.i, edf491a8dfccfa6378da1f67984511795182afc470c7adf35a0acc959fae5609
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/edf491a8dfccfa6378da1f67984511795182afc470c7adf35a0acc959fae5609.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
875085e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | sv-comp-22 | 4 | 2022-12-10T22:03:10+01:00 | ||
b7f739e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | frama-c-sv version 0.4.0 | 3 | 2022-12-09T13:16:58Z | ||
d63bc76 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Taipan | 14 | 2022-12-14T06:54:52Z | ||
ef994bf | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Symbiotic | 3 | 2022-12-25T08:36:13Z | ||
494f14b | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Symbiotic | 3 | 2022-12-12T12:39:38Z | ||
de038d3 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Pinaka | 3 | 2022-12-11T17:58:43 | ||
4d524af | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Kojak | 14 | 2022-12-14T18:22:24Z | ||
752fdfa | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Goblint (tags/svcomp23-0-g4f5dcf38f) | 13 | 2022-12-10T08:21:19Z | ||
cfc984b | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 8 | 2023-01-29T10:51:31+01:00 | d63bc76 | |
cfd705d | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 8 | 2023-01-29T07:41:07+01:00 | 8c063e5 | |
c4c4f9a | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 8 | 2023-01-29T06:23:30+01:00 | 4d524af | |
a9d1d7a | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 8 | 2023-01-29T05:24:39+01:00 | 494f14b | |
74db149 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 8 | 2023-01-29T04:46:54+01:00 | de038d3 | |
e891114 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 8 | 2023-01-29T03:04:18+01:00 | b6ae760 | |
0a90425 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 8 | 2023-01-29T00:07:01+01:00 | f1c732d | |
3ec81a2 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 8 | 2023-01-28T22:50:36+01:00 | 875085e | |
e070a35 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 8 | 2023-01-28T22:43:39+01:00 | 752fdfa | |
46a60b4 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 8 | 2023-01-28T18:35:01+01:00 | 300ba2a | |
25a0379 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 8 | 2023-01-28T17:38:37+01:00 | b7f739e | |
b2b5d73 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 8 | 2023-01-28T11:38:24+01:00 | 32e5f62 | |
431c431 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 8 | 2023-01-28T00:30:39+01:00 | ef994bf | |
32e5f62 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 8 | 2022-12-10T18:44:37+01:00 | ||
b6ae760 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2.1-svn-1715bd67dc+ | 8 | 2022-12-12T01:39:48+01:00 | ||
f1c732d | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0 | 8 | 2022-12-11T05:34:18+01:00 | ||
300ba2a | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 8 | 2022-12-10T03:31:30+01:00 | ||
8c063e5 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Automizer | 14 | 2022-12-13T15:57:57Z |
Found 1 witnesses for program sv-benchmarks/c/termination-libowfat/strpbrk_true-termination.c.i, edf491a8dfccfa6378da1f67984511795182afc470c7adf35a0acc959fae5609
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/edf491a8dfccfa6378da1f67984511795182afc470c7adf35a0acc959fae5609.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
266188c | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2021-12-10T16:24:16 |
Found 2 witnesses for program sv-benchmarks/c/termination-libowfat/strpbrk_true-termination.c.i, edf491a8dfccfa6378da1f67984511795182afc470c7adf35a0acc959fae5609
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/edf491a8dfccfa6378da1f67984511795182afc470c7adf35a0acc959fae5609.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
f15966f | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2020-12-11T14:38:42 | ||
79e95cd | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2020-12-08T17:38:29 |
Found 0 witnesses for program sv-benchmarks/c/termination-libowfat/strpbrk_true-termination.c.i, edf491a8dfccfa6378da1f67984511795182afc470c7adf35a0acc959fae5609
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/edf491a8dfccfa6378da1f67984511795182afc470c7adf35a0acc959fae5609.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/strpbrk_true-termination.c.i, edf491a8dfccfa6378da1f67984511795182afc470c7adf35a0acc959fae5609
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/edf491a8dfccfa6378da1f67984511795182afc470c7adf35a0acc959fae5609.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/strpbrk_true-termination.c.i, edf491a8dfccfa6378da1f67984511795182afc470c7adf35a0acc959fae5609
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/edf491a8dfccfa6378da1f67984511795182afc470c7adf35a0acc959fae5609.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/strpbrk_true-termination.c.i, edf491a8dfccfa6378da1f67984511795182afc470c7adf35a0acc959fae5609
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/edf491a8dfccfa6378da1f67984511795182afc470c7adf35a0acc959fae5609.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |