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_counter3_true-termination_true-no-overflow.c |
programSHA |
d7b4f33979632a981e739ff06b52fe01aa9fb175d5e5193b145052887f22f8a3 |
witnessName |
results-verified/depthk.2017-12-01_1515.logfiles/sv-comp18.rec_counter3_true-termination_true-no-overflow.c.files/witness.graphml |
witnessSHA |
4c8143ef98b91ea494083e50119c16ed2cfe3ed1e2ae5045357ee215b3cdd9ed |
Information about the Witness from Competition Database
from https://sv-comp.sosy-lab.org/2018/results/witnessInfoByHash/4c8143ef98b91ea494083e50119c16ed2cfe3ed1e2ae5045357ee215b3cdd9ed.json
Key |
Value |
architecture |
32bit |
creationtime |
2017-12-01T21:43 CET (sv-comp) |
memoryModel |
precise |
producer |
ESBMC 3.1 |
program-sha256 |
d7b4f33979632a981e739ff06b52fe01aa9fb175d5e5193b145052887f22f8a3 |
programfile |
/tmp/vcloud-vcloud-master/worker/working_dir_967c5167-6b99-481f-a0e0-52586fb04661/sv-benchmarks/c/termination-numeric/rec_counter3_true-termination_true-no-overflow.c |
programhash |
639f18bc5de28da6eb107c1e55f1eb45909efdef |
sourcecodelang |
C |
specification |
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file |
witnessFileByHash/4c8143ef98b91ea494083e50119c16ed2cfe3ed1e2ae5045357ee215b3cdd9ed.graphml |
witness-sha256 |
4c8143ef98b91ea494083e50119c16ed2cfe3ed1e2ae5045357ee215b3cdd9ed |
witness-size |
8087 |
witness-type |
correctness_witness |
Available Results for the Program from Witness Store SV-COMP '24
Trying to find witnesses for program (d7b4f33979632a981e739ff06b52fe01aa9fb175d5e5193b145052887f22f8a3, sv-benchmarks/c/termination-numeric/rec_counter3_true-termination_true-no-overflow.c).
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 |
|
Available Results for the Program from Witness Store SV-COMP '23
Trying to find witnesses for program (d7b4f33979632a981e739ff06b52fe01aa9fb175d5e5193b145052887f22f8a3, sv-benchmarks/c/termination-numeric/rec_counter3_true-termination_true-no-overflow.c).
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 |
Available Results for the Program from Witness Store SV-COMP '22
Trying to find witnesses for program (d7b4f33979632a981e739ff06b52fe01aa9fb175d5e5193b145052887f22f8a3, sv-benchmarks/c/termination-numeric/rec_counter3_true-termination_true-no-overflow.c).
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 |
|
Available Results for the Program from Witness Store SV-COMP '21
Trying to find witnesses for program (d7b4f33979632a981e739ff06b52fe01aa9fb175d5e5193b145052887f22f8a3, sv-benchmarks/c/termination-numeric/rec_counter3_true-termination_true-no-overflow.c).
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 |
|
Available Results for the Program from Witness Store SV-COMP '20
Trying to find witnesses for program (d7b4f33979632a981e739ff06b52fe01aa9fb175d5e5193b145052887f22f8a3, sv-benchmarks/c/termination-numeric/rec_counter3_true-termination_true-no-overflow.c).
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 |
|
Available Results for the Program from Witness Store SV-COMP '19
Trying to find witnesses for program (d7b4f33979632a981e739ff06b52fe01aa9fb175d5e5193b145052887f22f8a3, sv-benchmarks/c/termination-numeric/rec_counter3_true-termination_true-no-overflow.c).
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 |
|
Available Results for the Program from Witness Store SV-COMP '18
Trying to find witnesses for program (d7b4f33979632a981e739ff06b52fe01aa9fb175d5e5193b145052887f22f8a3, sv-benchmarks/c/termination-numeric/rec_counter3_true-termination_true-no-overflow.c).
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) |
|
Available Results for the Program from Witness Store SV-COMP '17
Trying to find witnesses for program (d7b4f33979632a981e739ff06b52fe01aa9fb175d5e5193b145052887f22f8a3, sv-benchmarks/c/termination-numeric/rec_counter3_true-termination_true-no-overflow.c).
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 |