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-crafted/NestedRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c |
programSHA |
9948dbd77aeb2de72e0bd3a3a4e22b1606b19383e4631af58adbec46ed909b6c |
witnessName |
results-verified/utaipan.2018-12-08_1419.logfiles/sv-comp19_prop-nooverflow.NestedRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c.files/witness.graphml |
witnessSHA |
d5e037fae6315fd3caf7a41918217f10c2f3f535ac901be756f605c808cf9d1a |
Information about the Witness from Competition Database
from https://sv-comp.sosy-lab.org/2019/results/witnessInfoByHash/d5e037fae6315fd3caf7a41918217f10c2f3f535ac901be756f605c808cf9d1a.json
Key |
Value |
architecture |
64bit |
creationtime |
2018-12-09T16:41Z |
producer |
Taipan |
programfile |
/tmp/vcloud-vcloud-master/worker/working_dir_8ae81811-1ecc-4665-a576-af61a2f7d15e/sv-benchmarks/c/termination-crafted/NestedRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c |
programhash |
cb528549fa76ae8087cf7043645dfa20323a0116 |
sourcecodelang |
C |
specification |
CHECK( init(main()), LTL(G ! overflow) )
|
witness-file |
witnessFileByHash/d5e037fae6315fd3caf7a41918217f10c2f3f535ac901be756f605c808cf9d1a.graphml |
witness-sha256 |
d5e037fae6315fd3caf7a41918217f10c2f3f535ac901be756f605c808cf9d1a |
witness-size |
13334 |
witness-type |
correctness_witness |
Available Results for the Program from Witness Store SV-COMP '24
Trying to find witnesses for program (9948dbd77aeb2de72e0bd3a3a4e22b1606b19383e4631af58adbec46ed909b6c, sv-benchmarks/c/termination-crafted/NestedRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c).
Found 12 witnesses for program sv-benchmarks/c/termination-crafted/NestedRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c, 9948dbd77aeb2de72e0bd3a3a4e22b1606b19383e4631af58adbec46ed909b6c
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/9948dbd77aeb2de72e0bd3a3a4e22b1606b19383e4631af58adbec46ed909b6c.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
f96ce8c |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
frama-c-sv version 0.4.0 |
3 |
2023-12-03T07:12:11Z |
|
e4ba962 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
sv-comp-24 |
4 |
2023-12-03T17:23:56+01:00 |
|
834fddc |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
VeriOover |
1 |
2023-12-20T03:37 CET (comp) |
|
5db48d6 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Taipan |
13 |
2023-12-02T11:24:55Z |
|
61a6b1d |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Pinaka |
3 |
2023-12-19T23:29:46 |
|
bb82dbb |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
7 |
2023-12-20T03:54:22+01:00 |
834fddc |
fe60cb9 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
7 |
2023-12-20T02:30:39+01:00 |
61a6b1d |
478c41a |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
7 |
2023-12-04T11:43:03+01:00 |
5db48d6 |
a6c997f |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
7 |
2023-12-03T18:47:33+01:00 |
e4ba962 |
12c313d |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
7 |
2023-12-03T10:00:41+01:00 |
f96ce8c |
dfac37b |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.0.1-svn-a45b42da2f+ |
7 |
2023-12-18T23:16:23+01:00 |
|
310d6b9 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Automizer |
13 |
2023-11-29T05:50:51Z |
|
Available Results for the Program from Witness Store SV-COMP '23
Trying to find witnesses for program (9948dbd77aeb2de72e0bd3a3a4e22b1606b19383e4631af58adbec46ed909b6c, sv-benchmarks/c/termination-crafted/NestedRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c).
Found 11 witnesses for program sv-benchmarks/c/termination-crafted/NestedRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c, 9948dbd77aeb2de72e0bd3a3a4e22b1606b19383e4631af58adbec46ed909b6c
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/9948dbd77aeb2de72e0bd3a3a4e22b1606b19383e4631af58adbec46ed909b6c.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
78a49b6 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
frama-c-sv version 0.4.0 |
3 |
2022-12-09T11:04:49Z |
|
c78c23e |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
sv-comp-22 |
4 |
2022-12-10T22:07:19+01:00 |
|
834fddc |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
VeriOover |
1 |
2022-12-12T11:02 CET (comp) |
|
69167ed |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Taipan |
13 |
2022-12-14T12:20:41Z |
|
64f9c94 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Pinaka |
3 |
2022-12-11T17:05:43 |
|
d6745e9 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.2 |
7 |
2023-01-29T11:46:26+01:00 |
834fddc |
84ad6f4 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.2 |
7 |
2023-01-29T07:30:31+01:00 |
f8bd3e4 |
643b873 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.2 |
7 |
2023-01-29T05:02:26+01:00 |
64f9c94 |
ed2bdd3 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.2.1-svn-1715bd67dc+ |
7 |
2022-12-11T20:29:46+01:00 |
|
daf2d98 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.0.1-svn-a45b42da2f+ |
7 |
2022-12-10T04:53:46+01:00 |
|
f8bd3e4 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Automizer |
13 |
2022-12-13T18:50:47Z |
|
Available Results for the Program from Witness Store SV-COMP '22
Trying to find witnesses for program (9948dbd77aeb2de72e0bd3a3a4e22b1606b19383e4631af58adbec46ed909b6c, sv-benchmarks/c/termination-crafted/NestedRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c).
Found 9 witnesses for program sv-benchmarks/c/termination-crafted/NestedRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c, 9948dbd77aeb2de72e0bd3a3a4e22b1606b19383e4631af58adbec46ed909b6c
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/9948dbd77aeb2de72e0bd3a3a4e22b1606b19383e4631af58adbec46ed909b6c.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
fcdd9fd |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
frama-c-sv version 0.2.8 |
3 |
2021-12-13T19:58:45Z |
|
5114e2e |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
sv-comp-22 |
4 |
2021-12-06T13:42:52+01:00 |
|
736b346 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Taipan |
13 |
2021-12-09T23:23:08Z |
|
df66106 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Pinaka |
3 |
2021-12-09T08:21:49 |
|
636caf7 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.1 |
7 |
2021-12-10T08:48:21+01:00 |
736b346 |
55f5af0 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.1 |
7 |
2021-12-09T10:23:01+01:00 |
df66106 |
2c6802a |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.1 |
7 |
2021-12-06T15:13:28+01:00 |
5114e2e |
ffde95c |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Automizer |
13 |
2021-12-06T16:41:04Z |
|
3ca2091 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
Symbiotic |
2 |
2021-12-10T17:34:42 |
|
Available Results for the Program from Witness Store SV-COMP '21
Trying to find witnesses for program (9948dbd77aeb2de72e0bd3a3a4e22b1606b19383e4631af58adbec46ed909b6c, sv-benchmarks/c/termination-crafted/NestedRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c).
Found 7 witnesses for program sv-benchmarks/c/termination-crafted/NestedRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c, 9948dbd77aeb2de72e0bd3a3a4e22b1606b19383e4631af58adbec46ed909b6c
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/9948dbd77aeb2de72e0bd3a3a4e22b1606b19383e4631af58adbec46ed909b6c.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
2f9c5f9 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
frama-c-sv version 0.2.1 |
3 |
2020-12-06T23:35:54 |
|
762abd6 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Pinaka |
3 |
2020-12-08T08:05:37 |
|
bb8bf78 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.0 |
7 |
2020-12-09T22:00:11+01:00 |
a78cd40 |
cab0333 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.0 |
7 |
2020-12-05T15:13:50+01:00 |
|
cc98900 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.0.1-svn-eda176372c+ |
7 |
2020-12-08T04:54:13+01:00 |
|
41a6cac |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
Symbiotic |
2 |
2020-12-11T22:42:00 |
|
b58b3d7 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
Symbiotic |
2 |
2020-12-09T00:53:19 |
|
Available Results for the Program from Witness Store SV-COMP '20
Trying to find witnesses for program (9948dbd77aeb2de72e0bd3a3a4e22b1606b19383e4631af58adbec46ed909b6c, sv-benchmarks/c/termination-crafted/NestedRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c).
Found 2 witnesses for program sv-benchmarks/c/termination-crafted/NestedRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c, 9948dbd77aeb2de72e0bd3a3a4e22b1606b19383e4631af58adbec46ed909b6c
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/9948dbd77aeb2de72e0bd3a3a4e22b1606b19383e4631af58adbec46ed909b6c.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
4ca310e |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 1.9 |
6 |
2019-11-30T01:28:50+01:00 |
|
0439f94 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 1.8-svn-35b8bb3bb3+ |
6 |
2019-12-01T03:42:29+01:00 |
|
Available Results for the Program from Witness Store SV-COMP '19
Trying to find witnesses for program (9948dbd77aeb2de72e0bd3a3a4e22b1606b19383e4631af58adbec46ed909b6c, sv-benchmarks/c/termination-crafted/NestedRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c).
Found 3 witnesses for program sv-benchmarks/c/termination-crafted/NestedRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c, 9948dbd77aeb2de72e0bd3a3a4e22b1606b19383e4631af58adbec46ed909b6c
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/9948dbd77aeb2de72e0bd3a3a4e22b1606b19383e4631af58adbec46ed909b6c.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
391a01b |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
SMACK 1.9.3 |
3 |
2018-12-08T00:21:41 |
|
809a950 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 1.7-svn b8d6131600+ |
197 |
2018-12-07T17:19:17+01:00 |
|
51571eb |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
197 |
2018-12-06T07:01:19+01:00 |
|
Available Results for the Program from Witness Store SV-COMP '18
Trying to find witnesses for program (9948dbd77aeb2de72e0bd3a3a4e22b1606b19383e4631af58adbec46ed909b6c, sv-benchmarks/c/termination-crafted/NestedRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c).
Found 4 witnesses for program sv-benchmarks/c/termination-crafted/NestedRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c, 9948dbd77aeb2de72e0bd3a3a4e22b1606b19383e4631af58adbec46ed909b6c
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/9948dbd77aeb2de72e0bd3a3a4e22b1606b19383e4631af58adbec46ed909b6c.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
67b7f92 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Taipan |
13 |
2017-12-03T07:44Z |
|
07c3331 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
ESBMC 3.1 |
11 |
2017-12-01T13:57 CET (sv-comp) |
|
bdfb002 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Automizer |
13 |
2017-12-03T10:22Z |
|
2b419e9 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
ESBMC 3.1 |
11 |
2017-12-01T17:51 CET (sv-comp) |
|
Available Results for the Program from Witness Store SV-COMP '17
Trying to find witnesses for program (9948dbd77aeb2de72e0bd3a3a4e22b1606b19383e4631af58adbec46ed909b6c, sv-benchmarks/c/termination-crafted/NestedRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c).
Found 0 witnesses for program sv-benchmarks/c/termination-crafted/NestedRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c, 9948dbd77aeb2de72e0bd3a3a4e22b1606b19383e4631af58adbec46ed909b6c
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/9948dbd77aeb2de72e0bd3a3a4e22b1606b19383e4631af58adbec46ed909b6c.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |