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-memory-alloca/java_AG313-alloca_true-termination.c.i |
programSHA |
2bfa9ea18c3859fb14daaafa2138a5573eef07b7f87afeb019dc7effa80c928b |
witnessName |
results-verified/depthk.2018-12-05_0936.logfiles/sv-comp19_prop-termination.java_AG313-alloca_true-termination.c.i.files/witness.graphml |
witnessSHA |
796f7cbc4275dde400c91a4b703d87fe0c8dc6248363bd592de19cecd3c63cbd |
Information about the Witness from Competition Database
from https://sv-comp.sosy-lab.org/2019/results/witnessInfoByHash/796f7cbc4275dde400c91a4b703d87fe0c8dc6248363bd592de19cecd3c63cbd.json
Key |
Value |
architecture |
32bit |
creationtime |
2018-12-06T05:39:01.446827 |
producer |
DepthK v3.0 |
programfile |
/tmp/vcloud-vcloud-master/worker/working_dir_6b1b10fe-315c-4771-a1c9-a9ad45d733d3/sv-benchmarks/c/termination-memory-alloca/java_AG313-alloca_true-termination.c.i |
programhash |
b64613d278f1b2a5aec6d84cb3470147257700f5 |
sourcecodelang |
C |
specification |
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file |
witnessFileByHash/796f7cbc4275dde400c91a4b703d87fe0c8dc6248363bd592de19cecd3c63cbd.graphml |
witness-sha256 |
796f7cbc4275dde400c91a4b703d87fe0c8dc6248363bd592de19cecd3c63cbd |
witness-size |
3489 |
witness-type |
correctness_witness |
Available Results for the Program from Witness Store SV-COMP '24
Trying to find witnesses for program (2bfa9ea18c3859fb14daaafa2138a5573eef07b7f87afeb019dc7effa80c928b, sv-benchmarks/c/termination-memory-alloca/java_AG313-alloca_true-termination.c.i).
Found 12 witnesses for program sv-benchmarks/c/termination-memory-alloca/java_AG313-alloca_true-termination.c.i, 2bfa9ea18c3859fb14daaafa2138a5573eef07b7f87afeb019dc7effa80c928b
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/2bfa9ea18c3859fb14daaafa2138a5573eef07b7f87afeb019dc7effa80c928b.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
21b35a4 |
Inspect |
|
valid-memsafety |
violation_witness |
DIVINE 4 |
2 |
2023-12-18T10:07:31+01:00 |
|
a8fc31f |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
Symbiotic |
3 |
2023-11-30T00:04:26Z |
|
571b18e |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.3 |
6 |
2023-12-18T12:07:59+01:00 |
21b35a4 |
7ba83f1 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.3 |
6 |
2023-11-30T04:54:15+01:00 |
|
b310277 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.2.1-svn-e677b7cd46+ |
6 |
2023-12-04T00:34:26+01:00 |
|
958fd18 |
Inspect |
|
CHECK( init(main()), LTL(G valid-free) )
CHECK( init(main()), LTL(G valid-deref) )
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
Taipan |
19 |
2023-12-02T17:08:08Z |
|
6ef6bcf |
Inspect |
|
CHECK( init(main()), LTL(G valid-free) )
CHECK( init(main()), LTL(G valid-deref) )
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
PredatorHP |
4 |
2023-11-30T08:25:29Z |
|
07a51a5 |
Inspect |
|
CHECK( init(main()), LTL(G valid-free) )
CHECK( init(main()), LTL(G valid-deref) )
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
Mopsa (v1.0~pre2) |
3 |
2023-11-29T16:12:36Z |
|
5f19ad9 |
Inspect |
|
CHECK( init(main()), LTL(G valid-free) )
CHECK( init(main()), LTL(G valid-deref) )
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
Kojak |
19 |
2023-12-02T23:01:07Z |
|
0e5f933 |
Inspect |
|
CHECK( init(main()), LTL(G valid-free) )
CHECK( init(main()), LTL(G valid-deref) )
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
Goblint (tags/svcomp24-0-gc2e9465a7) |
22 |
2023-11-30T22:36:31Z |
|
abeb37e |
Inspect |
|
CHECK( init(main()), LTL(G valid-free) )
CHECK( init(main()), LTL(G valid-deref) )
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
Automizer |
19 |
2023-11-29T04:34:51Z |
|
d4cebb6 |
Inspect |
|
CHECK( init(main()), LTL(G valid-deref) ) |
correctness_witness |
CPAchecker 2.0.1-svn-a45b42da2f+ |
6 |
2023-12-18T17:47:40+01:00 |
|
Available Results for the Program from Witness Store SV-COMP '23
Trying to find witnesses for program (2bfa9ea18c3859fb14daaafa2138a5573eef07b7f87afeb019dc7effa80c928b, sv-benchmarks/c/termination-memory-alloca/java_AG313-alloca_true-termination.c.i).
Found 6 witnesses for program sv-benchmarks/c/termination-memory-alloca/java_AG313-alloca_true-termination.c.i, 2bfa9ea18c3859fb14daaafa2138a5573eef07b7f87afeb019dc7effa80c928b
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/2bfa9ea18c3859fb14daaafa2138a5573eef07b7f87afeb019dc7effa80c928b.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
5039973 |
Inspect |
|
valid-memsafety |
violation_witness |
DIVINE 4 |
2 |
2022-12-09T06:49:35+01:00 |
|
0f5ddf9 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.2 |
6 |
2023-01-28T14:14:39+01:00 |
5039973 |
08154a0 |
Inspect |
|
CHECK( init(main()), LTL(G valid-free) )
CHECK( init(main()), LTL(G valid-deref) )
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
Taipan |
18 |
2022-12-14T08:48:39Z |
|
23919c5 |
Inspect |
|
CHECK( init(main()), LTL(G valid-free) )
CHECK( init(main()), LTL(G valid-deref) )
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
Mopsa (v1.0~pre2) |
3 |
2022-12-11T11:44:37Z |
|
7772fdf |
Inspect |
|
CHECK( init(main()), LTL(G valid-free) )
CHECK( init(main()), LTL(G valid-deref) )
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
Kojak |
18 |
2022-12-14T16:55:58Z |
|
3a5cea1 |
Inspect |
|
CHECK( init(main()), LTL(G valid-free) )
CHECK( init(main()), LTL(G valid-deref) )
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
Automizer |
18 |
2022-12-13T15:27:40Z |
|
Available Results for the Program from Witness Store SV-COMP '22
Trying to find witnesses for program (2bfa9ea18c3859fb14daaafa2138a5573eef07b7f87afeb019dc7effa80c928b, sv-benchmarks/c/termination-memory-alloca/java_AG313-alloca_true-termination.c.i).
Found 1 witnesses for program sv-benchmarks/c/termination-memory-alloca/java_AG313-alloca_true-termination.c.i, 2bfa9ea18c3859fb14daaafa2138a5573eef07b7f87afeb019dc7effa80c928b
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/2bfa9ea18c3859fb14daaafa2138a5573eef07b7f87afeb019dc7effa80c928b.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
f69b2d9 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
Symbiotic |
2 |
2021-12-10T17:38:25 |
|
Available Results for the Program from Witness Store SV-COMP '21
Trying to find witnesses for program (2bfa9ea18c3859fb14daaafa2138a5573eef07b7f87afeb019dc7effa80c928b, sv-benchmarks/c/termination-memory-alloca/java_AG313-alloca_true-termination.c.i).
Found 2 witnesses for program sv-benchmarks/c/termination-memory-alloca/java_AG313-alloca_true-termination.c.i, 2bfa9ea18c3859fb14daaafa2138a5573eef07b7f87afeb019dc7effa80c928b
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/2bfa9ea18c3859fb14daaafa2138a5573eef07b7f87afeb019dc7effa80c928b.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
03f779f |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
Symbiotic |
2 |
2020-12-11T18:13:38 |
|
c3b78c6 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
Symbiotic |
2 |
2020-12-08T15:37:09 |
|
Available Results for the Program from Witness Store SV-COMP '20
Trying to find witnesses for program (2bfa9ea18c3859fb14daaafa2138a5573eef07b7f87afeb019dc7effa80c928b, sv-benchmarks/c/termination-memory-alloca/java_AG313-alloca_true-termination.c.i).
Found 0 witnesses for program sv-benchmarks/c/termination-memory-alloca/java_AG313-alloca_true-termination.c.i, 2bfa9ea18c3859fb14daaafa2138a5573eef07b7f87afeb019dc7effa80c928b
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/2bfa9ea18c3859fb14daaafa2138a5573eef07b7f87afeb019dc7effa80c928b.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
Available Results for the Program from Witness Store SV-COMP '19
Trying to find witnesses for program (2bfa9ea18c3859fb14daaafa2138a5573eef07b7f87afeb019dc7effa80c928b, sv-benchmarks/c/termination-memory-alloca/java_AG313-alloca_true-termination.c.i).
Found 0 witnesses for program sv-benchmarks/c/termination-memory-alloca/java_AG313-alloca_true-termination.c.i, 2bfa9ea18c3859fb14daaafa2138a5573eef07b7f87afeb019dc7effa80c928b
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/2bfa9ea18c3859fb14daaafa2138a5573eef07b7f87afeb019dc7effa80c928b.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
Available Results for the Program from Witness Store SV-COMP '18
Trying to find witnesses for program (2bfa9ea18c3859fb14daaafa2138a5573eef07b7f87afeb019dc7effa80c928b, sv-benchmarks/c/termination-memory-alloca/java_AG313-alloca_true-termination.c.i).
Found 2 witnesses for program sv-benchmarks/c/termination-memory-alloca/java_AG313-alloca_true-termination.c.i, 2bfa9ea18c3859fb14daaafa2138a5573eef07b7f87afeb019dc7effa80c928b
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/2bfa9ea18c3859fb14daaafa2138a5573eef07b7f87afeb019dc7effa80c928b.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
016f957 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
ESBMC 3.1 |
6 |
2017-12-01T19:26 CET (sv-comp) |
|
bab8aaa |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
2LS |
31 |
2017-12-01T16:46 CET (sv-comp) |
|
Available Results for the Program from Witness Store SV-COMP '17
Trying to find witnesses for program (2bfa9ea18c3859fb14daaafa2138a5573eef07b7f87afeb019dc7effa80c928b, sv-benchmarks/c/termination-memory-alloca/java_AG313-alloca_true-termination.c.i).
Found 0 witnesses for program sv-benchmarks/c/termination-memory-alloca/java_AG313-alloca_true-termination.c.i, 2bfa9ea18c3859fb14daaafa2138a5573eef07b7f87afeb019dc7effa80c928b
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/2bfa9ea18c3859fb14daaafa2138a5573eef07b7f87afeb019dc7effa80c928b.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |