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 6 witnesses for program sv-benchmarks/c/termination-numeric/rec_counter3_true-termination_true-no-overflow.c, d7b4f33979632a981e739ff06b52fe01aa9fb175d5e5193b145052887f22f8a3
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/d7b4f33979632a981e739ff06b52fe01aa9fb175d5e5193b145052887f22f8a3.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
c331a9d | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | frama-c-sv version 0.4.0 | 3 | 2023-12-03T06:03:02Z | ||
9ac5b0c | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | sv-comp-24 | 4 | 2023-12-03T18:02:20+01:00 | ||
5e598c7 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | VeriOover | 1 | 2023-12-20T03:38 CET (comp) | ||
0fff0b3 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Pinaka | 3 | 2023-12-19T23:51:15 | ||
55b55a4 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 4472 | 2023-12-20T03:55:40+01:00 | 5e598c7 | |
61c992e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 4130 | 2023-11-30T06:03:48+01:00 |
Found 7 witnesses for program sv-benchmarks/c/termination-numeric/rec_counter3_true-termination_true-no-overflow.c, d7b4f33979632a981e739ff06b52fe01aa9fb175d5e5193b145052887f22f8a3
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/d7b4f33979632a981e739ff06b52fe01aa9fb175d5e5193b145052887f22f8a3.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
3f2b1fa | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | frama-c-sv version 0.4.0 | 3 | 2022-12-09T13:46:23Z | ||
dbed781 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | sv-comp-22 | 4 | 2022-12-10T22:04:36+01:00 | ||
5e598c7 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | VeriOover | 1 | 2022-12-12T10:59 CET (comp) | ||
3cdcd71 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Pinaka | 3 | 2022-12-11T15:14:41 | ||
dab66c3 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 4833 | 2023-01-29T11:46:34+01:00 | 5e598c7 | |
91796bd | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 4650 | 2023-01-29T05:05:49+01:00 | 3cdcd71 | |
34fafdb | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 5020 | 2023-01-28T23:07:53+01:00 | dbed781 |
Found 5 witnesses for program sv-benchmarks/c/termination-numeric/rec_counter3_true-termination_true-no-overflow.c, d7b4f33979632a981e739ff06b52fe01aa9fb175d5e5193b145052887f22f8a3
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/d7b4f33979632a981e739ff06b52fe01aa9fb175d5e5193b145052887f22f8a3.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
ea0fe17 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | frama-c-sv version 0.2.8 | 3 | 2021-12-13T21:03:32Z | ||
8aec4ba | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | sv-comp-22 | 4 | 2021-12-06T14:19:52+01:00 | ||
c601df5 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Pinaka | 3 | 2021-12-09T07:05:29 | ||
8724d1b | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0.1-svn-fe6f522dd3+ | 6030 | 2021-12-08T19:02:05+01:00 | ||
cd65592 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0.1-svn-eda176372c+ | 6030 | 2021-12-09T09:56:30+01:00 |
Found 4 witnesses for program sv-benchmarks/c/termination-numeric/rec_counter3_true-termination_true-no-overflow.c, d7b4f33979632a981e739ff06b52fe01aa9fb175d5e5193b145052887f22f8a3
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/d7b4f33979632a981e739ff06b52fe01aa9fb175d5e5193b145052887f22f8a3.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
cfda7b8 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | frama-c-sv version 0.2.1 | 3 | 2020-12-06T23:35:22 | ||
f4d57c7 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Pinaka | 3 | 2020-12-08T11:06:08 | ||
bfa8a43 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0 | 6030 | 2020-12-05T16:23:31+01:00 | ||
6403972 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0.1-svn-eda176372c+ | 6030 | 2020-12-08T00:24:48+01:00 |
Found 1 witnesses for program sv-benchmarks/c/termination-numeric/rec_counter3_true-termination_true-no-overflow.c, d7b4f33979632a981e739ff06b52fe01aa9fb175d5e5193b145052887f22f8a3
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/d7b4f33979632a981e739ff06b52fe01aa9fb175d5e5193b145052887f22f8a3.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
aff8a57 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 6015 | 2019-12-01T13:09:14+01:00 |
Found 2 witnesses for program sv-benchmarks/c/termination-numeric/rec_counter3_true-termination_true-no-overflow.c, d7b4f33979632a981e739ff06b52fe01aa9fb175d5e5193b145052887f22f8a3
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/d7b4f33979632a981e739ff06b52fe01aa9fb175d5e5193b145052887f22f8a3.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
eee59ac | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | SMACK 1.9.3 | 3 | 2018-12-08T08:15:56 | ||
f002659 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 6681 | 2018-12-08T02:29:30+01:00 |
Found 2 witnesses for program sv-benchmarks/c/termination-numeric/rec_counter3_true-termination_true-no-overflow.c, d7b4f33979632a981e739ff06b52fe01aa9fb175d5e5193b145052887f22f8a3
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/d7b4f33979632a981e739ff06b52fe01aa9fb175d5e5193b145052887f22f8a3.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
7ff0b52 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | ESBMC 3.1 | 7 | 2017-12-01T14:05 CET (sv-comp) | ||
4c8143e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 3.1 | 8 | 2017-12-01T21:43 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/termination-numeric/rec_counter3_true-termination_true-no-overflow.c, d7b4f33979632a981e739ff06b52fe01aa9fb175d5e5193b145052887f22f8a3
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/d7b4f33979632a981e739ff06b52fe01aa9fb175d5e5193b145052887f22f8a3.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |