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/RecursiveNonterminating_false-termination_true-valid-memsafety.c |
programSHA |
fc6cfc9bc139db752e72885619d5342f9725bf67cec8b7ca9da9022c75c17b44 |
witnessName |
results-verified/depthk.2018-12-05_0936.logfiles/sv-comp19_prop-termination.RecursiveNonterminating_false-termination_true-valid-memsafety.c.files/witness.graphml |
witnessSHA |
9cab58d7e4ef5b63ea8700955f1eab5421bbac2c72ff04036c6c2ed0aa5a4d47 |
Information about the Witness from Competition Database
from https://sv-comp.sosy-lab.org/2019/results/witnessInfoByHash/9cab58d7e4ef5b63ea8700955f1eab5421bbac2c72ff04036c6c2ed0aa5a4d47.json
Key |
Value |
architecture |
32bit |
creationtime |
2018-12-06T00:21:35.305565 |
producer |
DepthK v3.0 |
programfile |
/tmp/vcloud-vcloud-master/worker/working_dir_9eaa1f31-811f-4d35-9234-79e1624321d5/sv-benchmarks/c/termination-crafted/RecursiveNonterminating_false-termination_true-valid-memsafety.c |
programhash |
f21f1881350863de740f7b7321104b53617dd8ce |
sourcecodelang |
C |
specification |
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file |
witnessFileByHash/9cab58d7e4ef5b63ea8700955f1eab5421bbac2c72ff04036c6c2ed0aa5a4d47.graphml |
witness-sha256 |
9cab58d7e4ef5b63ea8700955f1eab5421bbac2c72ff04036c6c2ed0aa5a4d47 |
witness-size |
3509 |
witness-type |
correctness_witness |
Available Results for the Program from Witness Store SV-COMP '24
Trying to find witnesses for program (fc6cfc9bc139db752e72885619d5342f9725bf67cec8b7ca9da9022c75c17b44, sv-benchmarks/c/termination-crafted/RecursiveNonterminating_false-termination_true-valid-memsafety.c).
Found 16 witnesses for program sv-benchmarks/c/termination-crafted/RecursiveNonterminating_false-termination_true-valid-memsafety.c, fc6cfc9bc139db752e72885619d5342f9725bf67cec8b7ca9da9022c75c17b44
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/fc6cfc9bc139db752e72885619d5342f9725bf67cec8b7ca9da9022c75c17b44.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
424352d |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
sv-comp-24 |
4 |
2023-12-03T17:21:05+01:00 |
|
a8841b0 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
frama-c-sv version 0.4.0 |
3 |
2023-12-03T04:07:54Z |
|
1b59cec |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
VeriOover |
1 |
2023-12-20T03:37 CET (comp) |
|
422801e |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Taipan |
8 |
2023-12-02T17:34:45Z |
|
3f5a571 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Kojak |
8 |
2023-12-03T01:53:16Z |
|
5e5c8d0 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
5 |
2023-12-03T18:52:18+01:00 |
424352d |
484d189 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
5 |
2023-12-03T06:06:54+01:00 |
3f5a571 |
981696e |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
5 |
2023-11-30T06:09:23+01:00 |
|
dea9ca4 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
5 |
2023-11-29T08:09:20+01:00 |
66b987e |
2229f4c |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.2.1-svn-e677b7cd46+ |
5 |
2023-12-04T00:28:37+01:00 |
|
66b987e |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Automizer |
8 |
2023-11-28T22:39:55Z |
|
1859f71 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
violation_witness |
CPAchecker 2.1 |
5 |
2023-12-17T03:11:56+01:00 |
|
96493e5 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
violation_witness |
CPAchecker 2.0.1-svn-a45b42da2f+ |
5 |
2023-12-19T01:25:48+01:00 |
|
08afe7c |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
violation_witness |
Automizer |
5 |
2023-11-29T00:10:28Z |
|
f496c3c |
Inspect |
|
- entry_type: invariant_set
metadata:
format_version: '2.0'
uuid: 9358edfe-7209-4049-aa8d-721e7182807b
creation_time: '2023-12-03T02:53:16+01:00'
producer:
name: Kojak
version: 0.2.4-dev-0e0057c
task:
input_files:
- /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_30224c26-144e-43ac-861d-f55100a3e1c4/sv-benchmarks/c/termination-crafted/RecursiveNonterminating-1.c
input_file_hashes:
? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_30224c26-144e-43ac-861d-f55100a3e1c4/sv-benchmarks/c/termination-crafted/RecursiveNonterminating-1.c
: fc6cfc9bc139db752e72885619d5342f9725bf67cec8b7ca9da9022c75c17b44
specification: |+
CHECK( init(main()), LTL(G ! overflow) )
data_model: 64bit
language: C
content: [
] |
correctness_witness |
CPAchecker 2.3 |
6 |
2023-12-03T05:54:41+01:00 |
|
cf25749 |
Inspect |
|
- entry_type: invariant_set
metadata:
format_version: '2.0'
uuid: 3cbf3d55-f412-4fdf-9c0c-562c92a87c42
creation_time: '2023-12-02T18:34:45+01:00'
producer:
name: Taipan
version: 0.2.4-dev-0e0057c
task:
input_files:
- /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_ff050a1a-0982-4124-928a-3e8bea2f3673/sv-benchmarks/c/termination-crafted/RecursiveNonterminating-1.c
input_file_hashes:
? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_ff050a1a-0982-4124-928a-3e8bea2f3673/sv-benchmarks/c/termination-crafted/RecursiveNonterminating-1.c
: fc6cfc9bc139db752e72885619d5342f9725bf67cec8b7ca9da9022c75c17b44
specification: |+
CHECK( init(main()), LTL(G ! overflow) )
data_model: 64bit
language: C
content: [
] |
correctness_witness |
CPAchecker 2.3 |
6 |
2023-12-04T12:08:32+01:00 |
|
Available Results for the Program from Witness Store SV-COMP '23
Trying to find witnesses for program (fc6cfc9bc139db752e72885619d5342f9725bf67cec8b7ca9da9022c75c17b44, sv-benchmarks/c/termination-crafted/RecursiveNonterminating_false-termination_true-valid-memsafety.c).
Found 12 witnesses for program sv-benchmarks/c/termination-crafted/RecursiveNonterminating_false-termination_true-valid-memsafety.c, fc6cfc9bc139db752e72885619d5342f9725bf67cec8b7ca9da9022c75c17b44
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/fc6cfc9bc139db752e72885619d5342f9725bf67cec8b7ca9da9022c75c17b44.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
5576bed |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
sv-comp-22 |
4 |
2022-12-11T01:46:03+01:00 |
|
4ec7275 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
frama-c-sv version 0.4.0 |
3 |
2022-12-09T10:02:23Z |
|
1b59cec |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
VeriOover |
1 |
2022-12-12T10:59 CET (comp) |
|
a022cdc |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Taipan |
8 |
2022-12-14T10:10:46Z |
|
9952c4c |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Kojak |
8 |
2022-12-14T23:24:54Z |
|
17f8a23 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.2 |
5 |
2023-01-29T11:17:53+01:00 |
a022cdc |
ad1ef3f |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.2 |
5 |
2023-01-29T07:54:34+01:00 |
26fb8fd |
26fb8fd |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Automizer |
8 |
2022-12-13T20:19:17Z |
|
ea6b7f8 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
violation_witness |
CPAchecker 2.1 |
5 |
2022-12-25T09:49:36+01:00 |
|
3ccb52e |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
violation_witness |
CPAchecker 2.0.1-svn-a45b42da2f+ |
5 |
2022-12-09T23:35:26+01:00 |
|
42e545e |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
violation_witness |
Automizer |
5 |
2022-12-13T15:48:30Z |
|
fd2b7f0 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
Bubaak |
3 |
2022-12-08T16:35:31Z |
|
Available Results for the Program from Witness Store SV-COMP '22
Trying to find witnesses for program (fc6cfc9bc139db752e72885619d5342f9725bf67cec8b7ca9da9022c75c17b44, sv-benchmarks/c/termination-crafted/RecursiveNonterminating_false-termination_true-valid-memsafety.c).
Found 6 witnesses for program sv-benchmarks/c/termination-crafted/RecursiveNonterminating_false-termination_true-valid-memsafety.c, fc6cfc9bc139db752e72885619d5342f9725bf67cec8b7ca9da9022c75c17b44
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/fc6cfc9bc139db752e72885619d5342f9725bf67cec8b7ca9da9022c75c17b44.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
f5b6a95 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
violation_witness |
CPAchecker 2.1 |
5 |
2021-12-05T18:57:59+01:00 |
|
bcbf833 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
violation_witness |
CPAchecker 2.0.1-svn-fe6f522dd3+ |
5 |
2021-12-08T18:49:57+01:00 |
|
9b8eb4c |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
violation_witness |
CPAchecker 2.0.1-svn-eda176372c+ |
5 |
2021-12-09T13:41:18+01:00 |
|
a3ec092 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
violation_witness |
Automizer |
5 |
2021-12-06T23:57:49Z |
|
1c4e479 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
violation_witness |
AProVE |
4 |
2021-12-05T11:39:42Z |
|
b7b2180 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
Symbiotic |
2 |
2021-12-10T17:00:07 |
|
Available Results for the Program from Witness Store SV-COMP '21
Trying to find witnesses for program (fc6cfc9bc139db752e72885619d5342f9725bf67cec8b7ca9da9022c75c17b44, sv-benchmarks/c/termination-crafted/RecursiveNonterminating_false-termination_true-valid-memsafety.c).
Found 4 witnesses for program sv-benchmarks/c/termination-crafted/RecursiveNonterminating_false-termination_true-valid-memsafety.c, fc6cfc9bc139db752e72885619d5342f9725bf67cec8b7ca9da9022c75c17b44
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/fc6cfc9bc139db752e72885619d5342f9725bf67cec8b7ca9da9022c75c17b44.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
eae7df6 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
violation_witness |
CPAchecker 2.0 |
5 |
2020-12-05T16:50:27+01:00 |
|
8ae0a56 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
violation_witness |
CPAchecker 2.0.1-svn-eda176372c+ |
5 |
2020-12-07T22:35:20+01:00 |
|
b4c65c4 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
Symbiotic |
2 |
2020-12-11T20:17:26 |
|
6812e42 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
Symbiotic |
2 |
2020-12-09T02:32:24 |
|
Available Results for the Program from Witness Store SV-COMP '20
Trying to find witnesses for program (fc6cfc9bc139db752e72885619d5342f9725bf67cec8b7ca9da9022c75c17b44, sv-benchmarks/c/termination-crafted/RecursiveNonterminating_false-termination_true-valid-memsafety.c).
Found 4 witnesses for program sv-benchmarks/c/termination-crafted/RecursiveNonterminating_false-termination_true-valid-memsafety.c, fc6cfc9bc139db752e72885619d5342f9725bf67cec8b7ca9da9022c75c17b44
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/fc6cfc9bc139db752e72885619d5342f9725bf67cec8b7ca9da9022c75c17b44.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
ebb5fe8 |
Inspect |
|
CHECK( init(main()), LTL(G valid-free) ) |
correctness_witness |
CPAchecker 1.8-svn-35b8bb3bb3+ |
5 |
2019-12-01T00:41:03+01:00 |
|
94c6812 |
Inspect |
|
CHECK( init(main()), LTL(G valid-deref) ) |
correctness_witness |
CPAchecker 1.9 |
5 |
2019-11-29T14:23:39+01:00 |
|
1e0d146 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
violation_witness |
CPAchecker 1.9 |
5 |
2019-11-30T09:35:13+01:00 |
|
c636c8a |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
violation_witness |
CPAchecker 1.8-svn-35b8bb3bb3+ |
5 |
2019-12-01T08:39:02+01:00 |
|
Available Results for the Program from Witness Store SV-COMP '19
Trying to find witnesses for program (fc6cfc9bc139db752e72885619d5342f9725bf67cec8b7ca9da9022c75c17b44, sv-benchmarks/c/termination-crafted/RecursiveNonterminating_false-termination_true-valid-memsafety.c).
Found 1 witnesses for program sv-benchmarks/c/termination-crafted/RecursiveNonterminating_false-termination_true-valid-memsafety.c, fc6cfc9bc139db752e72885619d5342f9725bf67cec8b7ca9da9022c75c17b44
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/fc6cfc9bc139db752e72885619d5342f9725bf67cec8b7ca9da9022c75c17b44.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
a0564c3 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
5 |
2018-12-06T07:54:37+01:00 |
|
Available Results for the Program from Witness Store SV-COMP '18
Trying to find witnesses for program (fc6cfc9bc139db752e72885619d5342f9725bf67cec8b7ca9da9022c75c17b44, sv-benchmarks/c/termination-crafted/RecursiveNonterminating_false-termination_true-valid-memsafety.c).
Found 2 witnesses for program sv-benchmarks/c/termination-crafted/RecursiveNonterminating_false-termination_true-valid-memsafety.c, fc6cfc9bc139db752e72885619d5342f9725bf67cec8b7ca9da9022c75c17b44
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/fc6cfc9bc139db752e72885619d5342f9725bf67cec8b7ca9da9022c75c17b44.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
7c96385 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
ESBMC 3.1 |
4 |
2017-12-01T16:35 CET (sv-comp) |
|
e8c8a4e |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
violation_witness |
Automizer |
5 |
2017-12-03T11:12Z |
|
Available Results for the Program from Witness Store SV-COMP '17
Trying to find witnesses for program (fc6cfc9bc139db752e72885619d5342f9725bf67cec8b7ca9da9022c75c17b44, sv-benchmarks/c/termination-crafted/RecursiveNonterminating_false-termination_true-valid-memsafety.c).
Found 0 witnesses for program sv-benchmarks/c/termination-crafted/RecursiveNonterminating_false-termination_true-valid-memsafety.c, fc6cfc9bc139db752e72885619d5342f9725bf67cec8b7ca9da9022c75c17b44
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/fc6cfc9bc139db752e72885619d5342f9725bf67cec8b7ca9da9022c75c17b44.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |