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 7 witnesses for program sv-benchmarks/c/termination-numeric/rec_counter1_true-termination_true-no-overflow.c, de5b7f1cccf5c7fe435559014125bbfd73538586d5303d45f8d606cb31a4b74b
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/de5b7f1cccf5c7fe435559014125bbfd73538586d5303d45f8d606cb31a4b74b.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
2dd4a12 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | frama-c-sv version 0.4.0 | 3 | 2023-12-03T07:40:16Z | ||
70aa587 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | sv-comp-24 | 4 | 2023-12-03T17:21:57+01:00 | ||
f6487f2 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | VeriOover | 1 | 2023-12-20T03:37 CET (comp) | ||
1d976ad | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Pinaka | 3 | 2023-12-19T19:16:05 | ||
42ca9de | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 3649 | 2023-12-20T02:42:20+01:00 | 1d976ad | |
d913621 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 3649 | 2023-12-03T18:47:33+01:00 | 70aa587 | |
c9264fd | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 4129 | 2023-11-30T08:27:41+01:00 |
Found 8 witnesses for program sv-benchmarks/c/termination-numeric/rec_counter1_true-termination_true-no-overflow.c, de5b7f1cccf5c7fe435559014125bbfd73538586d5303d45f8d606cb31a4b74b
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/de5b7f1cccf5c7fe435559014125bbfd73538586d5303d45f8d606cb31a4b74b.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
fe1bec4 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | frama-c-sv version 0.4.0 | 3 | 2022-12-09T12:57:37Z | ||
8ef1686 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | sv-comp-22 | 4 | 2022-12-10T22:00:39+01:00 | ||
f6487f2 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | VeriOover | 1 | 2022-12-12T11:01 CET (comp) | ||
f6cdaf6 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Pinaka | 3 | 2022-12-11T12:44:18 | ||
0433702 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 4832 | 2023-01-29T11:46:42+01:00 | f6487f2 | |
59b3df5 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 4650 | 2023-01-28T23:06:33+01:00 | 8ef1686 | |
7b0c62e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 523 | 2023-01-28T17:49:35+01:00 | fe1bec4 | |
937bb02 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6029 | 2022-12-10T17:09:44+01:00 |
Found 5 witnesses for program sv-benchmarks/c/termination-numeric/rec_counter1_true-termination_true-no-overflow.c, de5b7f1cccf5c7fe435559014125bbfd73538586d5303d45f8d606cb31a4b74b
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/de5b7f1cccf5c7fe435559014125bbfd73538586d5303d45f8d606cb31a4b74b.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
ba6da8d | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | frama-c-sv version 0.2.8 | 3 | 2021-12-13T19:58:21Z | ||
5fdf00c | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | sv-comp-22 | 4 | 2021-12-06T13:36:01+01:00 | ||
ab6c948 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Pinaka | 3 | 2021-12-09T07:10:52 | ||
3cfb64b | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0.1-svn-eda176372c+ | 6029 | 2021-12-09T12:40:36+01:00 | ||
5d5520c | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2021-12-10T16:17:03 |
Found 6 witnesses for program sv-benchmarks/c/termination-numeric/rec_counter1_true-termination_true-no-overflow.c, de5b7f1cccf5c7fe435559014125bbfd73538586d5303d45f8d606cb31a4b74b
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/de5b7f1cccf5c7fe435559014125bbfd73538586d5303d45f8d606cb31a4b74b.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
9299be2 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | frama-c-sv version 0.2.1 | 3 | 2020-12-06T23:40:36 | ||
b474c5c | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Pinaka | 3 | 2020-12-08T10:24:07 | ||
fd73c5e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0 | 6029 | 2020-12-05T13:50:46+01:00 | ||
e2b88a9 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0.1-svn-eda176372c+ | 6029 | 2020-12-08T04:35:26+01:00 | ||
f0004ad | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2020-12-11T18:24:49 | ||
b9b0bae | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2020-12-09T02:33:22 |
Found 1 witnesses for program sv-benchmarks/c/termination-numeric/rec_counter1_true-termination_true-no-overflow.c, de5b7f1cccf5c7fe435559014125bbfd73538586d5303d45f8d606cb31a4b74b
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/de5b7f1cccf5c7fe435559014125bbfd73538586d5303d45f8d606cb31a4b74b.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
6553356 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 6015 | 2019-12-01T02:26:34+01:00 |
Found 1 witnesses for program sv-benchmarks/c/termination-numeric/rec_counter1_true-termination_true-no-overflow.c, de5b7f1cccf5c7fe435559014125bbfd73538586d5303d45f8d606cb31a4b74b
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/de5b7f1cccf5c7fe435559014125bbfd73538586d5303d45f8d606cb31a4b74b.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
f2feb85 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | SMACK 1.9.3 | 3 | 2018-12-08T18:15:31 |
Found 2 witnesses for program sv-benchmarks/c/termination-numeric/rec_counter1_true-termination_true-no-overflow.c, de5b7f1cccf5c7fe435559014125bbfd73538586d5303d45f8d606cb31a4b74b
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/de5b7f1cccf5c7fe435559014125bbfd73538586d5303d45f8d606cb31a4b74b.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
cacd77e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | ESBMC 3.1 | 7 | 2017-12-01T13:21 CET (sv-comp) | ||
648d136 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 3.1 | 8 | 2017-12-01T21:14 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/termination-numeric/rec_counter1_true-termination_true-no-overflow.c, de5b7f1cccf5c7fe435559014125bbfd73538586d5303d45f8d606cb31a4b74b
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/de5b7f1cccf5c7fe435559014125bbfd73538586d5303d45f8d606cb31a4b74b.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |