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-3_true-valid-memsafety_true-termination.i |
programSHA |
aa52a50db96d55b59d19995958546e1bde20387ce0b816cd9ff33848cc2087c5 |
witnessName |
results-verified/depthk.2017-12-01_0905.logfiles/sv-comp18.test-bitfields-3_true-valid-memsafety_true-termination.i.files/witness.graphml |
witnessSHA |
a7ee1046103018fac3355f654d27379be0a5b9ac3dd8badb6659a5aba4d2c324 |
Information about the Witness from Competition Database
from https://sv-comp.sosy-lab.org/2018/results/witnessInfoByHash/a7ee1046103018fac3355f654d27379be0a5b9ac3dd8badb6659a5aba4d2c324.json
Key |
Value |
architecture |
32bit |
creationtime |
2017-12-01T09:09 CET (sv-comp) |
memoryModel |
precise |
producer |
ESBMC 3.1 |
program-sha256 |
aa52a50db96d55b59d19995958546e1bde20387ce0b816cd9ff33848cc2087c5 |
programfile |
/tmp/vcloud-vcloud-master/worker/working_dir_0864ebd7-1e56-46f2-8e00-13529e77f818/sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3_true-valid-memsafety_true-termination.i |
programhash |
2187ad12904216f135de1d4e0a00e45b56b4da69 |
sourcecodelang |
C |
specification |
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) |
witness-file |
witnessFileByHash/a7ee1046103018fac3355f654d27379be0a5b9ac3dd8badb6659a5aba4d2c324.graphml |
witness-sha256 |
a7ee1046103018fac3355f654d27379be0a5b9ac3dd8badb6659a5aba4d2c324 |
witness-size |
6868 |
witness-type |
violation_witness |
Available Results for the Program from Witness Store SV-COMP '24
Trying to find witnesses for program (aa52a50db96d55b59d19995958546e1bde20387ce0b816cd9ff33848cc2087c5, sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3_true-valid-memsafety_true-termination.i).
Found 19 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3_true-valid-memsafety_true-termination.i, aa52a50db96d55b59d19995958546e1bde20387ce0b816cd9ff33848cc2087c5
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/aa52a50db96d55b59d19995958546e1bde20387ce0b816cd9ff33848cc2087c5.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
c7cbffa |
Inspect |
|
valid-memsafety |
correctness_witness |
DIVINE 4 |
2 |
2023-12-18T07:58:40+01:00 |
|
6896d67 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
Symbiotic |
3 |
2023-11-29T19:19:08Z |
|
5771d23 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.3 |
8 |
2023-11-30T08:33:29+01:00 |
|
c6efb39 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.2.1-svn-e677b7cd46+ |
8 |
2023-12-03T23:15:39+01:00 |
|
1277758 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.0 |
8 |
2023-12-19T14:00:54+01:00 |
|
042496b |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.0.1-svn-38892M |
13 |
2023-12-18T02:00:40+01:00 |
|
1ad44b2 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
Bubaak |
3 |
2023-12-05T09:05:38Z |
|
8afd827 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
Bubaak |
3 |
2023-12-04T12:49:14Z |
|
30de3e8 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
Bubaak |
3 |
2023-12-01T21:13:53Z |
|
8f434ee |
Inspect |
|
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) |
correctness_witness |
ESBMC 7.4.0 incr |
3 |
2023-12-01T13:02:36Z |
|
4d87616 |
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-17T13:43:08+01:00 |
|
b784d14 |
Inspect |
|
CHECK( init(main()), LTL(G valid-deref) ) |
correctness_witness |
CPAchecker 2.0.1-svn-a45b42da2f+ |
8 |
2023-12-18T19:26:22+01:00 |
|
4c23eb6 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
ESBMC 7.4.0 |
3 |
2023-12-01T14:31:26Z |
|
0c45988 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
Symbiotic |
3 |
2023-11-29T16:47:04Z |
|
fa4564d |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
Goblint (tags/svcomp24-0-gc2e9465a7) |
3 |
2023-12-01T02:00:51Z |
|
18cbc0a |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
CBMC |
7 |
2023-12-17T11:44:44+01:00 |
|
727100e |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
Bubaak |
3 |
2023-12-05T09:48:28Z |
|
2069602 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
Bubaak |
3 |
2023-12-04T14:12:32Z |
|
698fdc9 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
Bubaak |
3 |
2023-12-01T19:51:26Z |
|
Available Results for the Program from Witness Store SV-COMP '23
Trying to find witnesses for program (aa52a50db96d55b59d19995958546e1bde20387ce0b816cd9ff33848cc2087c5, sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3_true-valid-memsafety_true-termination.i).
Found 15 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3_true-valid-memsafety_true-termination.i, aa52a50db96d55b59d19995958546e1bde20387ce0b816cd9ff33848cc2087c5
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/aa52a50db96d55b59d19995958546e1bde20387ce0b816cd9ff33848cc2087c5.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
7da02be |
Inspect |
|
valid-memsafety |
correctness_witness |
DIVINE 4 |
2 |
2022-12-09T07:04:06+01:00 |
|
35daadd |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.2 |
8 |
2022-12-10T21:19:33+01:00 |
|
b3270aa |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.2.1-svn-1715bd67dc+ |
8 |
2022-12-11T19:41:37+01:00 |
|
2f2d84a |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.0 |
8 |
2022-12-11T02:16:40+01:00 |
|
ba113ca |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.0.1-svn-a45b42da2f+ |
8 |
2022-12-09T17:40:51+01:00 |
|
c47f80f |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.0.1-svn-38892M |
13 |
2022-12-09T03:01:42+01:00 |
|
a681a8a |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
Bubaak |
3 |
2022-12-08T12:53:03Z |
|
2d0fa07 |
Inspect |
|
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) |
correctness_witness |
ESBMC 7.0.0 incr |
3 |
2022-12-18T22:28:00Z |
|
635204a |
Inspect |
|
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) |
correctness_witness |
ESBMC 6.8.0 incr |
3 |
2022-12-25T10:11:01Z |
|
e17b29b |
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-08T11:06:46+01:00 |
|
74ded1a |
Inspect |
|
CHECK( init(main()), LTL(G ! call(reach_error())) ) |
correctness_witness |
ESBMC 6.8.0 |
3 |
2022-12-25T09:56:18Z |
|
3c0dabc |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
ESBMC 7.0.0 |
3 |
2022-12-18T23:13:53Z |
|
55dca0f |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
Symbiotic |
3 |
2022-12-12T16:04:25Z |
|
ec3c2c5 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
CBMC |
7 |
2022-12-08T13:33:54+01:00 |
|
4f2f68f |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
Bubaak |
3 |
2022-12-08T14:51:07Z |
|
Available Results for the Program from Witness Store SV-COMP '22
Trying to find witnesses for program (aa52a50db96d55b59d19995958546e1bde20387ce0b816cd9ff33848cc2087c5, sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3_true-valid-memsafety_true-termination.i).
Found 10 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3_true-valid-memsafety_true-termination.i, aa52a50db96d55b59d19995958546e1bde20387ce0b816cd9ff33848cc2087c5
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/aa52a50db96d55b59d19995958546e1bde20387ce0b816cd9ff33848cc2087c5.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
8c51bc0 |
Inspect |
|
valid-memsafety |
correctness_witness |
DIVINE 4 |
2 |
2021-12-07T07:52:00+01:00 |
|
f9ed0ba |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.1 |
8 |
2021-12-05T15:21:16+01:00 |
|
f19bca7 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.0.1-svn-eda176372c+ |
8 |
2021-12-09T12:02:50+01:00 |
|
fe2315c |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.0.1-svn-38892M |
13 |
2021-12-07T01:57:28+01:00 |
|
d11a7b5 |
Inspect |
|
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) |
correctness_witness |
ESBMC 6.8.0 incr |
3 |
2021-12-08T08:30:56Z |
|
dbe81b5 |
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-06T03:37:08+01:00 |
|
e4065e8 |
Inspect |
|
CHECK( init(main()), LTL(G valid-deref) ) |
correctness_witness |
CPAchecker 2.0.1-svn-fe6f522dd3+ |
8 |
2021-12-08T18:10:06+01:00 |
|
956df79 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(reach_error())) ) |
correctness_witness |
ESBMC 6.8.0 |
3 |
2021-12-08T03:33:23Z |
|
d686b65 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
Symbiotic |
3 |
2021-12-07T14:29:33Z |
|
e4898af |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
CBMC |
7 |
2021-12-06T07:47:45+01:00 |
|
Available Results for the Program from Witness Store SV-COMP '21
Trying to find witnesses for program (aa52a50db96d55b59d19995958546e1bde20387ce0b816cd9ff33848cc2087c5, sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3_true-valid-memsafety_true-termination.i).
Found 5 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3_true-valid-memsafety_true-termination.i, aa52a50db96d55b59d19995958546e1bde20387ce0b816cd9ff33848cc2087c5
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/aa52a50db96d55b59d19995958546e1bde20387ce0b816cd9ff33848cc2087c5.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
873e310 |
Inspect |
|
valid-memsafety |
correctness_witness |
DIVINE 4 |
2 |
2020-12-06T18:46:24+01:00 |
|
5427830 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.0 |
8 |
2020-12-05T15:54:29+01:00 |
|
f1b51ec |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.0.1-svn-eda176372c+ |
8 |
2020-12-08T00:40:25+01:00 |
|
c0eee24 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
Symbiotic |
2 |
2020-12-11T21:38:18 |
|
eb0808e |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
Symbiotic |
2 |
2020-12-09T02:36:53 |
|
Available Results for the Program from Witness Store SV-COMP '20
Trying to find witnesses for program (aa52a50db96d55b59d19995958546e1bde20387ce0b816cd9ff33848cc2087c5, sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3_true-valid-memsafety_true-termination.i).
Found 2 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3_true-valid-memsafety_true-termination.i, aa52a50db96d55b59d19995958546e1bde20387ce0b816cd9ff33848cc2087c5
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/aa52a50db96d55b59d19995958546e1bde20387ce0b816cd9ff33848cc2087c5.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
3a43cc0 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 1.9 |
8 |
2019-11-30T00:10:22+01:00 |
|
add402b |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 1.8-svn-35b8bb3bb3+ |
8 |
2019-12-01T03:46:32+01:00 |
|
Available Results for the Program from Witness Store SV-COMP '19
Trying to find witnesses for program (aa52a50db96d55b59d19995958546e1bde20387ce0b816cd9ff33848cc2087c5, sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3_true-valid-memsafety_true-termination.i).
Found 4 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3_true-valid-memsafety_true-termination.i, aa52a50db96d55b59d19995958546e1bde20387ce0b816cd9ff33848cc2087c5
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/aa52a50db96d55b59d19995958546e1bde20387ce0b816cd9ff33848cc2087c5.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
9e9b286 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
Symbiotic |
1 |
2018-12-08T14:01 CET (sv-comp) |
|
8c15e15 |
Inspect |
|
CHECK( init(main()), LTL(G valid-deref) ) |
correctness_witness |
CPAchecker 1.7-svn b8d6131600+ |
8 |
2018-12-06T13:18:43+01:00 |
|
dcb8780 |
Inspect |
|
CHECK( init(main()), LTL(G valid-deref) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
8 |
2018-12-05T18:29:26+01:00 |
|
a9b60f5 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
Symbiotic |
1 |
2018-12-08T09:12 CET (sv-comp) |
|
Available Results for the Program from Witness Store SV-COMP '18
Trying to find witnesses for program (aa52a50db96d55b59d19995958546e1bde20387ce0b816cd9ff33848cc2087c5, sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3_true-valid-memsafety_true-termination.i).
Found 11 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3_true-valid-memsafety_true-termination.i, aa52a50db96d55b59d19995958546e1bde20387ce0b816cd9ff33848cc2087c5
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/aa52a50db96d55b59d19995958546e1bde20387ce0b816cd9ff33848cc2087c5.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
35f9c86 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
Symbiotic |
1 |
2017-12-03T00:18 CET (sv-comp) |
|
a7ee104 |
Inspect |
|
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) |
violation_witness |
ESBMC 3.1 |
7 |
2017-12-01T09:09 CET (sv-comp) |
|
f891e72 |
Inspect |
|
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) |
correctness_witness |
ESBMC 4.6.0 kind |
3 |
2017-12-02T10:59:41.603388 |
|
2f2015c |
Inspect |
|
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) |
correctness_witness |
ESBMC 4.6.0 incr |
3 |
2017-12-01T23:58:39.284892 |
|
8c86436 |
Inspect |
|
CHECK( init(main()), LTL(G valid-free) ) |
correctness_witness |
CPAchecker 1.6.1-svn 26773 |
8 |
2017-12-01T08:24:16+01:00 |
|
c3e3f50 |
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 |
4 |
2017-12-01T23:54 CET (sv-comp) |
|
b99477a |
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 |
19 |
2017-12-01T08:27 CET (sv-comp) |
|
061c3e5 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
ESBMC 4.6.0 |
3 |
2017-12-02T20:01:22.523406 |
|
5e87081 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
ESBMC 4.6.0 |
3 |
2017-12-02T08:11:18.262408 |
|
25d56da |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
ESBMC 3.1 |
7 |
2017-12-01T16:39 CET (sv-comp) |
|
e63b03d |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
CBMC |
11 |
2017-12-01T19:16 CET (sv-comp) |
|
Available Results for the Program from Witness Store SV-COMP '17
Trying to find witnesses for program (aa52a50db96d55b59d19995958546e1bde20387ce0b816cd9ff33848cc2087c5, sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3_true-valid-memsafety_true-termination.i).
Found 0 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3_true-valid-memsafety_true-termination.i, aa52a50db96d55b59d19995958546e1bde20387ce0b816cd9ff33848cc2087c5
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/aa52a50db96d55b59d19995958546e1bde20387ce0b816cd9ff33848cc2087c5.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |