Witness Inspection
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).
View and Validate the Witness
Input Given to this Service about the Witness (URL Query)
Key |
Value |
programName |
sv-benchmarks/c/termination-numeric/rec_counter1_true-termination_true-no-overflow.c |
programSHA |
de5b7f1cccf5c7fe435559014125bbfd73538586d5303d45f8d606cb31a4b74b |
witnessName |
results-verified/depthk.2018-12-05_0936.logfiles/sv-comp19_prop-termination.rec_counter1_true-termination_true-no-overflow.c.files/witness.graphml |
witnessSHA |
124a6076631f4cb81541bdb479287af7e3ad13e6db7b1e574b001e646ca9a569 |
Information about the Witness from Competition Database
from https://sv-comp.sosy-lab.org/2019/results/witnessInfoByHash/124a6076631f4cb81541bdb479287af7e3ad13e6db7b1e574b001e646ca9a569.json
Key |
Value |
architecture |
32bit |
creationtime |
2018-12-05T10:52:21.216287 |
producer |
DepthK v3.0 |
programfile |
/tmp/vcloud-vcloud-master/worker/working_dir_c714b517-6522-4907-9777-34a780d6b86f/sv-benchmarks/c/termination-numeric/rec_counter1_true-termination_true-no-overflow.c |
programhash |
82bd2b65619821bf052931b3532da39241349d4f |
sourcecodelang |
C |
specification |
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file |
witnessFileByHash/124a6076631f4cb81541bdb479287af7e3ad13e6db7b1e574b001e646ca9a569.graphml |
witness-sha256 |
124a6076631f4cb81541bdb479287af7e3ad13e6db7b1e574b001e646ca9a569 |
witness-size |
3493 |
witness-type |
correctness_witness |
Available Results for the Program from Witness Store SV-COMP '24
Trying to find witnesses for program (de5b7f1cccf5c7fe435559014125bbfd73538586d5303d45f8d606cb31a4b74b, sv-benchmarks/c/termination-numeric/rec_counter1_true-termination_true-no-overflow.c).
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 |
|
Available Results for the Program from Witness Store SV-COMP '23
Trying to find witnesses for program (de5b7f1cccf5c7fe435559014125bbfd73538586d5303d45f8d606cb31a4b74b, sv-benchmarks/c/termination-numeric/rec_counter1_true-termination_true-no-overflow.c).
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 |
|
Available Results for the Program from Witness Store SV-COMP '22
Trying to find witnesses for program (de5b7f1cccf5c7fe435559014125bbfd73538586d5303d45f8d606cb31a4b74b, sv-benchmarks/c/termination-numeric/rec_counter1_true-termination_true-no-overflow.c).
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 |
|
Available Results for the Program from Witness Store SV-COMP '21
Trying to find witnesses for program (de5b7f1cccf5c7fe435559014125bbfd73538586d5303d45f8d606cb31a4b74b, sv-benchmarks/c/termination-numeric/rec_counter1_true-termination_true-no-overflow.c).
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 |
|
Available Results for the Program from Witness Store SV-COMP '20
Trying to find witnesses for program (de5b7f1cccf5c7fe435559014125bbfd73538586d5303d45f8d606cb31a4b74b, sv-benchmarks/c/termination-numeric/rec_counter1_true-termination_true-no-overflow.c).
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 |
|
Available Results for the Program from Witness Store SV-COMP '19
Trying to find witnesses for program (de5b7f1cccf5c7fe435559014125bbfd73538586d5303d45f8d606cb31a4b74b, sv-benchmarks/c/termination-numeric/rec_counter1_true-termination_true-no-overflow.c).
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 |
|
Available Results for the Program from Witness Store SV-COMP '18
Trying to find witnesses for program (de5b7f1cccf5c7fe435559014125bbfd73538586d5303d45f8d606cb31a4b74b, sv-benchmarks/c/termination-numeric/rec_counter1_true-termination_true-no-overflow.c).
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) |
|
Available Results for the Program from Witness Store SV-COMP '17
Trying to find witnesses for program (de5b7f1cccf5c7fe435559014125bbfd73538586d5303d45f8d606cb31a4b74b, sv-benchmarks/c/termination-numeric/rec_counter1_true-termination_true-no-overflow.c).
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 |