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/ldv-memsafety-bitfields/test-bitfields-2_true-valid-memsafety_true-termination.i |
programSHA |
b2b89b39c45546a854d6b4da4c390f65e7d0d3d3f22aabf536ab9bd132630b5c |
witnessName |
results-verified/map2check.2017-12-01_2312.logfiles/sv-comp18.test-bitfields-2_true-valid-memsafety_true-termination.i.files/witness.graphml |
witnessSHA |
c879eda0fdbebbf212c281100140c891deb51dedd8b79f90be233a2fe405a51c |
Information about the Witness from Competition Database
from https://sv-comp.sosy-lab.org/2018/results/witnessInfoByHash/c879eda0fdbebbf212c281100140c891deb51dedd8b79f90be233a2fe405a51c.json
Key |
Value |
architecture |
32bit |
creationtime |
2017-12-01T23:20 CET (sv-comp) |
error-specification-length |
Key 'specification' longer than 100 characters. |
producer |
Map2Check |
program-sha256 |
b2b89b39c45546a854d6b4da4c390f65e7d0d3d3f22aabf536ab9bd132630b5c |
programfile |
../../sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-2_true-valid-memsafety_true-termination.i |
programhash |
3dbc6bab9a799b7f4b90bf959cd96947d3b192e5 |
sourcecodelang |
C |
specification |
CHECK( init(main()), LTL(G valid-free) )
CHECK( init(main()), LTL(G valid-deref) )
CHECK( init(main()), LTL(G valid-memtrack) ) |
witness-file |
witnessFileByHash/c879eda0fdbebbf212c281100140c891deb51dedd8b79f90be233a2fe405a51c.graphml |
witness-sha256 |
c879eda0fdbebbf212c281100140c891deb51dedd8b79f90be233a2fe405a51c |
witness-size |
3485 |
witness-type |
correctness_witness |
Available Results for the Program from Witness Store SV-COMP '24
Trying to find witnesses for program (b2b89b39c45546a854d6b4da4c390f65e7d0d3d3f22aabf536ab9bd132630b5c, sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-2_true-valid-memsafety_true-termination.i).
Found 18 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-2_true-valid-memsafety_true-termination.i, b2b89b39c45546a854d6b4da4c390f65e7d0d3d3f22aabf536ab9bd132630b5c
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/b2b89b39c45546a854d6b4da4c390f65e7d0d3d3f22aabf536ab9bd132630b5c.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
a85265a |
Inspect |
|
valid-memsafety |
correctness_witness |
DIVINE 4 |
2 |
2023-12-18T10:18:33+01:00 |
|
93c46e7 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
Symbiotic |
3 |
2023-11-30T00:08:59Z |
|
b91de5f |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.3 |
5 |
2023-11-30T05:48:20+01:00 |
|
f9806fc |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.2.1-svn-e677b7cd46+ |
5 |
2023-12-03T20:39:00+01:00 |
|
a5885bf |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.0.1-svn-38892M |
10 |
2023-12-18T02:00:47+01:00 |
|
a06fa47 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
Bubaak |
3 |
2023-12-05T09:55:17Z |
|
9b6eaf1 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
Bubaak |
3 |
2023-12-04T09:53:36Z |
|
f451cd6 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
Bubaak |
3 |
2023-12-01T20:04:48Z |
|
b6b906e |
Inspect |
|
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) |
correctness_witness |
ESBMC 7.4.0 incr |
3 |
2023-12-01T03:31:10Z |
|
5b593bd |
Inspect |
|
CHECK( init(main()), LTL(G valid-free) )
CHECK( init(main()), LTL(G valid-deref) )
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CBMC |
9 |
2023-12-17T10:40:20+01:00 |
|
210ec53 |
Inspect |
|
CHECK( init(main()), LTL(G valid-deref) ) |
correctness_witness |
CPAchecker 2.0.1-svn-a45b42da2f+ |
5 |
2023-12-18T18:34:07+01:00 |
|
11cc5bb |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
ESBMC 7.4.0 |
3 |
2023-12-01T14:56:24Z |
|
3813cdc |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
Symbiotic |
3 |
2023-11-29T19:37:55Z |
|
3a1a662 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
Goblint (tags/svcomp24-0-gc2e9465a7) |
3 |
2023-12-01T01:45:48Z |
|
2b2f83b |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
CBMC |
7 |
2023-12-17T20:13:08+01:00 |
|
2f0d21b |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
Bubaak |
3 |
2023-12-05T12:08:15Z |
|
6b6609c |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
Bubaak |
3 |
2023-12-04T08:50:05Z |
|
e3bdf66 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
Bubaak |
3 |
2023-12-01T20:06:14Z |
|
Available Results for the Program from Witness Store SV-COMP '23
Trying to find witnesses for program (b2b89b39c45546a854d6b4da4c390f65e7d0d3d3f22aabf536ab9bd132630b5c, sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-2_true-valid-memsafety_true-termination.i).
Found 14 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-2_true-valid-memsafety_true-termination.i, b2b89b39c45546a854d6b4da4c390f65e7d0d3d3f22aabf536ab9bd132630b5c
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/b2b89b39c45546a854d6b4da4c390f65e7d0d3d3f22aabf536ab9bd132630b5c.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
ce1bc9e |
Inspect |
|
valid-memsafety |
correctness_witness |
DIVINE 4 |
2 |
2022-12-09T06:45:55+01:00 |
|
e0c4f3e |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.2 |
5 |
2022-12-10T18:38:31+01:00 |
|
c0cec93 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.2.1-svn-1715bd67dc+ |
5 |
2022-12-11T23:27:40+01:00 |
|
bc7fb77 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.0.1-svn-38892M |
10 |
2022-12-09T03:26:31+01:00 |
|
81f7d01 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
Bubaak |
3 |
2022-12-08T18:20:55Z |
|
fb0a5ba |
Inspect |
|
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) |
correctness_witness |
ESBMC 7.0.0 incr |
3 |
2022-12-19T00:14:09Z |
|
a083d75 |
Inspect |
|
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) |
correctness_witness |
ESBMC 6.8.0 incr |
3 |
2022-12-25T09:43:35Z |
|
338019b |
Inspect |
|
CHECK( init(main()), LTL(G valid-free) ) |
correctness_witness |
CPAchecker 2.0.1-svn-a45b42da2f+ |
5 |
2022-12-09T17:17:52+01:00 |
|
843fd23 |
Inspect |
|
CHECK( init(main()), LTL(G valid-free) )
CHECK( init(main()), LTL(G valid-deref) )
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CBMC |
9 |
2022-12-08T12:40:15+01:00 |
|
0c82b72 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(reach_error())) ) |
correctness_witness |
ESBMC 6.8.0 |
3 |
2022-12-25T08:29:37Z |
|
d34db41 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
ESBMC 7.0.0 |
3 |
2022-12-19T02:35:01Z |
|
8e32ee6 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
Symbiotic |
3 |
2022-12-12T15:46:56Z |
|
464a382 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
CBMC |
7 |
2022-12-08T05:23:38+01:00 |
|
dceda53 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
Bubaak |
3 |
2022-12-08T16:12:56Z |
|
Available Results for the Program from Witness Store SV-COMP '22
Trying to find witnesses for program (b2b89b39c45546a854d6b4da4c390f65e7d0d3d3f22aabf536ab9bd132630b5c, sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-2_true-valid-memsafety_true-termination.i).
Found 11 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-2_true-valid-memsafety_true-termination.i, b2b89b39c45546a854d6b4da4c390f65e7d0d3d3f22aabf536ab9bd132630b5c
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/b2b89b39c45546a854d6b4da4c390f65e7d0d3d3f22aabf536ab9bd132630b5c.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
e9b7c00 |
Inspect |
|
valid-memsafety |
correctness_witness |
DIVINE 4 |
2 |
2021-12-07T09:24:16+01:00 |
|
66ad77a |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.1 |
5 |
2021-12-05T17:20:53+01:00 |
|
728815d |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.0.1-svn-fe6f522dd3+ |
5 |
2021-12-08T16:44:34+01:00 |
|
cdcd4f4 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.0.1-svn-eda176372c+ |
5 |
2021-12-09T12:47:39+01:00 |
|
67f2df0 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.0.1-svn-38892M |
10 |
2021-12-07T03:38:17+01:00 |
|
49a9372 |
Inspect |
|
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) |
correctness_witness |
ESBMC 6.8.0 incr |
3 |
2021-12-08T09:12:59Z |
|
0ca5c2c |
Inspect |
|
CHECK( init(main()), LTL(G valid-free) )
CHECK( init(main()), LTL(G valid-deref) )
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CBMC |
7 |
2021-12-06T08:41:29+01:00 |
|
7fe1e5b |
Inspect |
|
CHECK( init(main()), LTL(G valid-deref) ) |
violation_witness |
SESL |
3 |
2021-12-06T11:55:53+01:00 |
|
6446eb7 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(reach_error())) ) |
correctness_witness |
ESBMC 6.8.0 |
3 |
2021-12-08T03:39:54Z |
|
0563f1f |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
Symbiotic |
3 |
2021-12-07T13:56:25Z |
|
0e76a36 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
CBMC |
7 |
2021-12-06T03:23:52+01:00 |
|
Available Results for the Program from Witness Store SV-COMP '21
Trying to find witnesses for program (b2b89b39c45546a854d6b4da4c390f65e7d0d3d3f22aabf536ab9bd132630b5c, sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-2_true-valid-memsafety_true-termination.i).
Found 5 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-2_true-valid-memsafety_true-termination.i, b2b89b39c45546a854d6b4da4c390f65e7d0d3d3f22aabf536ab9bd132630b5c
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/b2b89b39c45546a854d6b4da4c390f65e7d0d3d3f22aabf536ab9bd132630b5c.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
6c4db3a |
Inspect |
|
valid-memsafety |
correctness_witness |
DIVINE 4 |
2 |
2020-12-06T17:48:30+01:00 |
|
50a74df |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.0 |
5 |
2020-12-05T13:43:44+01:00 |
|
fd8ff38 |
Inspect |
|
CHECK( init(main()), LTL(G valid-deref) ) |
correctness_witness |
CPAchecker 2.0.1-svn-eda176372c+ |
5 |
2020-12-07T22:41:17+01:00 |
|
1279a84 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
Symbiotic |
2 |
2020-12-11T19:16:59 |
|
d9c46d1 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
Symbiotic |
2 |
2020-12-08T22:41:05 |
|
Available Results for the Program from Witness Store SV-COMP '20
Trying to find witnesses for program (b2b89b39c45546a854d6b4da4c390f65e7d0d3d3f22aabf536ab9bd132630b5c, sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-2_true-valid-memsafety_true-termination.i).
Found 2 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-2_true-valid-memsafety_true-termination.i, b2b89b39c45546a854d6b4da4c390f65e7d0d3d3f22aabf536ab9bd132630b5c
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/b2b89b39c45546a854d6b4da4c390f65e7d0d3d3f22aabf536ab9bd132630b5c.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
8de241d |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 1.8-svn-35b8bb3bb3+ |
5 |
2019-12-01T00:22:52+01:00 |
|
240a990 |
Inspect |
|
CHECK( init(main()), LTL(G valid-deref) ) |
correctness_witness |
CPAchecker 1.9 |
5 |
2019-11-30T08:04:38+01:00 |
|
Available Results for the Program from Witness Store SV-COMP '19
Trying to find witnesses for program (b2b89b39c45546a854d6b4da4c390f65e7d0d3d3f22aabf536ab9bd132630b5c, sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-2_true-valid-memsafety_true-termination.i).
Found 4 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-2_true-valid-memsafety_true-termination.i, b2b89b39c45546a854d6b4da4c390f65e7d0d3d3f22aabf536ab9bd132630b5c
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/b2b89b39c45546a854d6b4da4c390f65e7d0d3d3f22aabf536ab9bd132630b5c.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
e18b616 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
Symbiotic |
1 |
2018-12-08T06:31 CET (sv-comp) |
|
5b841f6 |
Inspect |
|
CHECK( init(main()), LTL(G valid-deref) ) |
correctness_witness |
CPAchecker 1.7-svn b8d6131600+ |
5 |
2018-12-07T12:10:20+01:00 |
|
a4f5822 |
Inspect |
|
CHECK( init(main()), LTL(G valid-deref) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
5 |
2018-12-05T22:06:43+01:00 |
|
85bf6a8 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
Symbiotic |
1 |
2018-12-08T09:51 CET (sv-comp) |
|
Available Results for the Program from Witness Store SV-COMP '18
Trying to find witnesses for program (b2b89b39c45546a854d6b4da4c390f65e7d0d3d3f22aabf536ab9bd132630b5c, sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-2_true-valid-memsafety_true-termination.i).
Found 9 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-2_true-valid-memsafety_true-termination.i, b2b89b39c45546a854d6b4da4c390f65e7d0d3d3f22aabf536ab9bd132630b5c
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/b2b89b39c45546a854d6b4da4c390f65e7d0d3d3f22aabf536ab9bd132630b5c.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
0957242 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
Symbiotic |
1 |
2017-12-03T00:11 CET (sv-comp) |
|
ee720d8 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 1.6.1-svn 26773 |
5 |
2017-12-01T08:34:27+01:00 |
|
afab639 |
Inspect |
|
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) |
correctness_witness |
ESBMC 4.6.0 kind |
3 |
2017-12-02T11:08:41.245423 |
|
49329e8 |
Inspect |
|
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) |
correctness_witness |
ESBMC 4.6.0 incr |
3 |
2017-12-01T23:50:29.854920 |
|
c879eda |
Inspect |
|
CHECK( init(main()), LTL(G valid-free) )
CHECK( init(main()), LTL(G valid-deref) )
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
Map2Check |
3 |
2017-12-01T23:20 CET (sv-comp) |
|
35071df |
Inspect |
|
CHECK( init(main()), LTL(G valid-free) )
CHECK( init(main()), LTL(G valid-deref) )
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CBMC |
13 |
2017-12-01T08:21 CET (sv-comp) |
|
9014726 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
ESBMC 4.6.0 |
3 |
2017-12-02T23:55:34.750961 |
|
6b80140 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
ESBMC 4.6.0 |
3 |
2017-12-02T12:07:10.153147 |
|
d125b35 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
CBMC |
10 |
2017-12-01T15:04 CET (sv-comp) |
|
Available Results for the Program from Witness Store SV-COMP '17
Trying to find witnesses for program (b2b89b39c45546a854d6b4da4c390f65e7d0d3d3f22aabf536ab9bd132630b5c, sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-2_true-valid-memsafety_true-termination.i).
Found 0 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-2_true-valid-memsafety_true-termination.i, b2b89b39c45546a854d6b4da4c390f65e7d0d3d3f22aabf536ab9bd132630b5c
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/b2b89b39c45546a854d6b4da4c390f65e7d0d3d3f22aabf536ab9bd132630b5c.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |