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.1_true-valid-memsafety_true-termination.i |
programSHA |
c8e6193201f070e4e8fd99485640ffa2e10139023e39442c320d13bfe62360e5 |
witnessName |
results-verified/depthk.2017-12-01_0905.logfiles/sv-comp18.test-bitfields-3.1_true-valid-memsafety_true-termination.i.files/witness.graphml |
witnessSHA |
10f370cc208b57111f697b8212e115cdac6ecb98be50aa378bd302abe389e8f9 |
Information about the Witness from Competition Database
from https://sv-comp.sosy-lab.org/2018/results/witnessInfoByHash/10f370cc208b57111f697b8212e115cdac6ecb98be50aa378bd302abe389e8f9.json
Key |
Value |
architecture |
32bit |
creationtime |
2017-12-01T09:16 CET (sv-comp) |
memoryModel |
precise |
producer |
ESBMC 3.1 |
program-sha256 |
c8e6193201f070e4e8fd99485640ffa2e10139023e39442c320d13bfe62360e5 |
programfile |
/tmp/vcloud-vcloud-master/worker/working_dir_a7b63aa5-f222-41b3-99d8-3c878be45876/sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3.1_true-valid-memsafety_true-termination.i |
programhash |
72da1f6907bc4b842c40cca6c3dd762e325d6dec |
sourcecodelang |
C |
specification |
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) |
witness-file |
witnessFileByHash/10f370cc208b57111f697b8212e115cdac6ecb98be50aa378bd302abe389e8f9.graphml |
witness-sha256 |
10f370cc208b57111f697b8212e115cdac6ecb98be50aa378bd302abe389e8f9 |
witness-size |
6675 |
witness-type |
violation_witness |
Available Results for the Program from Witness Store SV-COMP '24
Trying to find witnesses for program (c8e6193201f070e4e8fd99485640ffa2e10139023e39442c320d13bfe62360e5, sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3.1_true-valid-memsafety_true-termination.i).
Found 19 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3.1_true-valid-memsafety_true-termination.i, c8e6193201f070e4e8fd99485640ffa2e10139023e39442c320d13bfe62360e5
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/c8e6193201f070e4e8fd99485640ffa2e10139023e39442c320d13bfe62360e5.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
a5a8039 |
Inspect |
|
valid-memsafety |
correctness_witness |
DIVINE 4 |
2 |
2023-12-18T09:50:47+01:00 |
|
4ab7532 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
Symbiotic |
3 |
2023-11-29T23:25:26Z |
|
63c213d |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.3 |
6 |
2023-11-30T05:15:03+01:00 |
|
bccda4b |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.2.1-svn-e677b7cd46+ |
6 |
2023-12-03T23:04:29+01:00 |
|
56ef23b |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.0.1-svn-38892M |
9 |
2023-12-18T02:13:21+01:00 |
|
730265b |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
Bubaak |
3 |
2023-12-05T10:24:07Z |
|
8522521 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
Bubaak |
3 |
2023-12-04T14:28:20Z |
|
9436f80 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
Bubaak |
3 |
2023-12-01T20:50:40Z |
|
65cb3e7 |
Inspect |
|
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) |
correctness_witness |
ESBMC 7.4.0 incr |
3 |
2023-12-01T03:24:35Z |
|
37c9e65 |
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 |
8 |
2023-12-17T12:41:37+01:00 |
|
e567e36 |
Inspect |
|
CHECK( init(main()), LTL(G valid-deref) ) |
correctness_witness |
CPAchecker 2.0 |
6 |
2023-12-19T10:48:44+01:00 |
|
3a8f1c6 |
Inspect |
|
CHECK( init(main()), LTL(G valid-deref) ) |
correctness_witness |
CPAchecker 2.0.1-svn-a45b42da2f+ |
6 |
2023-12-19T01:52:36+01:00 |
|
8055fae |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
ESBMC 7.4.0 |
3 |
2023-12-01T10:11:08Z |
|
ca74d93 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
Symbiotic |
3 |
2023-11-29T20:54:29Z |
|
c47910d |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
Goblint (tags/svcomp24-0-gc2e9465a7) |
3 |
2023-11-30T22:33:36Z |
|
196567f |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
CBMC |
6 |
2023-12-17T08:55:21+01:00 |
|
ba5f98d |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
Bubaak |
3 |
2023-12-05T12:34:23Z |
|
411311a |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
Bubaak |
3 |
2023-12-04T09:09:50Z |
|
3df6c78 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
Bubaak |
3 |
2023-12-01T19:45:36Z |
|
Available Results for the Program from Witness Store SV-COMP '23
Trying to find witnesses for program (c8e6193201f070e4e8fd99485640ffa2e10139023e39442c320d13bfe62360e5, sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3.1_true-valid-memsafety_true-termination.i).
Found 16 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3.1_true-valid-memsafety_true-termination.i, c8e6193201f070e4e8fd99485640ffa2e10139023e39442c320d13bfe62360e5
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/c8e6193201f070e4e8fd99485640ffa2e10139023e39442c320d13bfe62360e5.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
7dcb6b8 |
Inspect |
|
valid-memsafety |
correctness_witness |
DIVINE 4 |
2 |
2022-12-09T05:09:10+01:00 |
|
8492843 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
Symbiotic |
3 |
2022-12-12T11:52:53Z |
|
a5c8368 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.2 |
6 |
2022-12-10T17:52:02+01:00 |
|
01019e6 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.2.1-svn-1715bd67dc+ |
6 |
2022-12-12T02:14:37+01:00 |
|
e489937 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.0 |
6 |
2022-12-11T03:54:07+01:00 |
|
fbb87e6 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.0.1-svn-a45b42da2f+ |
6 |
2022-12-10T01:25:08+01:00 |
|
0c3ba03 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.0.1-svn-38892M |
9 |
2022-12-09T03:25:35+01:00 |
|
1135d7b |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
Bubaak |
3 |
2022-12-08T21:12:32Z |
|
f551f1e |
Inspect |
|
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) |
correctness_witness |
ESBMC 7.0.0 incr |
3 |
2022-12-18T21:39:24Z |
|
75e57af |
Inspect |
|
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) |
correctness_witness |
ESBMC 6.8.0 incr |
3 |
2022-12-25T09:36:15Z |
|
f97b1a8 |
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 |
8 |
2022-12-08T04:31:18+01:00 |
|
5cff0e7 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(reach_error())) ) |
correctness_witness |
ESBMC 6.8.0 |
3 |
2022-12-25T09:48:39Z |
|
d9871c1 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
ESBMC 7.0.0 |
3 |
2022-12-19T02:40:13Z |
|
f8b3aa8 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
Symbiotic |
3 |
2022-12-12T14:33:39Z |
|
46c71d2 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
CBMC |
6 |
2022-12-08T07:25:59+01:00 |
|
445b609 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
Bubaak |
3 |
2022-12-08T16:25:42Z |
|
Available Results for the Program from Witness Store SV-COMP '22
Trying to find witnesses for program (c8e6193201f070e4e8fd99485640ffa2e10139023e39442c320d13bfe62360e5, sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3.1_true-valid-memsafety_true-termination.i).
Found 11 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3.1_true-valid-memsafety_true-termination.i, c8e6193201f070e4e8fd99485640ffa2e10139023e39442c320d13bfe62360e5
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/c8e6193201f070e4e8fd99485640ffa2e10139023e39442c320d13bfe62360e5.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
2da0e94 |
Inspect |
|
valid-memsafety |
correctness_witness |
DIVINE 4 |
2 |
2021-12-07T09:12:55+01:00 |
|
e4e7075 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
Symbiotic |
3 |
2021-12-07T15:33:35Z |
|
672fc96 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.1 |
6 |
2021-12-05T17:23:03+01:00 |
|
2f50c25 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.0.1-svn-38892M |
9 |
2021-12-07T02:03:40+01:00 |
|
554b6d7 |
Inspect |
|
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) |
correctness_witness |
ESBMC 6.8.0 incr |
3 |
2021-12-08T06:24:03Z |
|
a50bbc7 |
Inspect |
|
CHECK( init(main()), LTL(G valid-free) ) |
correctness_witness |
CPAchecker 2.0.1-svn-fe6f522dd3+ |
6 |
2021-12-08T19:34:11+01:00 |
|
80b26dc |
Inspect |
|
CHECK( init(main()), LTL(G valid-free) ) |
correctness_witness |
CPAchecker 2.0.1-svn-eda176372c+ |
6 |
2021-12-09T11:50:17+01:00 |
|
895893c |
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 |
6 |
2021-12-06T10:58:42+01:00 |
|
d06c781 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(reach_error())) ) |
correctness_witness |
ESBMC 6.8.0 |
3 |
2021-12-08T03:38:52Z |
|
15aa312 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
Symbiotic |
3 |
2021-12-07T12:06:21Z |
|
02ed330 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
CBMC |
6 |
2021-12-06T10:27:09+01:00 |
|
Available Results for the Program from Witness Store SV-COMP '21
Trying to find witnesses for program (c8e6193201f070e4e8fd99485640ffa2e10139023e39442c320d13bfe62360e5, sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3.1_true-valid-memsafety_true-termination.i).
Found 7 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3.1_true-valid-memsafety_true-termination.i, c8e6193201f070e4e8fd99485640ffa2e10139023e39442c320d13bfe62360e5
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/c8e6193201f070e4e8fd99485640ffa2e10139023e39442c320d13bfe62360e5.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
d0ab158 |
Inspect |
|
valid-memsafety |
correctness_witness |
DIVINE 4 |
2 |
2020-12-06T18:45:55+01:00 |
|
fff151c |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
Symbiotic |
2 |
2020-12-11T21:05:06 |
|
40f6068 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
Symbiotic |
2 |
2020-12-09T02:25:57 |
|
7649277 |
Inspect |
|
CHECK( init(main()), LTL(G valid-free) ) |
correctness_witness |
CPAchecker 2.0 |
6 |
2020-12-05T12:58:46+01:00 |
|
e2ea0f6 |
Inspect |
|
CHECK( init(main()), LTL(G valid-free) ) |
correctness_witness |
CPAchecker 2.0.1-svn-eda176372c+ |
6 |
2020-12-08T05:19:49+01:00 |
|
6a6555b |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
Symbiotic |
2 |
2020-12-11T23:07:08 |
|
6ec8c93 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
Symbiotic |
2 |
2020-12-08T23:47:02 |
|
Available Results for the Program from Witness Store SV-COMP '20
Trying to find witnesses for program (c8e6193201f070e4e8fd99485640ffa2e10139023e39442c320d13bfe62360e5, sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3.1_true-valid-memsafety_true-termination.i).
Found 2 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3.1_true-valid-memsafety_true-termination.i, c8e6193201f070e4e8fd99485640ffa2e10139023e39442c320d13bfe62360e5
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/c8e6193201f070e4e8fd99485640ffa2e10139023e39442c320d13bfe62360e5.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
6b4f8a5 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 1.9 |
6 |
2019-11-29T22:57:01+01:00 |
|
b26fc16 |
Inspect |
|
CHECK( init(main()), LTL(G valid-free) ) |
correctness_witness |
CPAchecker 1.8-svn-35b8bb3bb3+ |
6 |
2019-12-01T04:40:19+01:00 |
|
Available Results for the Program from Witness Store SV-COMP '19
Trying to find witnesses for program (c8e6193201f070e4e8fd99485640ffa2e10139023e39442c320d13bfe62360e5, sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3.1_true-valid-memsafety_true-termination.i).
Found 4 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3.1_true-valid-memsafety_true-termination.i, c8e6193201f070e4e8fd99485640ffa2e10139023e39442c320d13bfe62360e5
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/c8e6193201f070e4e8fd99485640ffa2e10139023e39442c320d13bfe62360e5.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
1c0b37c |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
Symbiotic |
1 |
2018-12-08T16:53 CET (sv-comp) |
|
9d85aea |
Inspect |
|
CHECK( init(main()), LTL(G valid-deref) ) |
correctness_witness |
CPAchecker 1.7-svn b8d6131600+ |
6 |
2018-12-08T00:52:03+01:00 |
|
d7baaa1 |
Inspect |
|
CHECK( init(main()), LTL(G valid-deref) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
6 |
2018-12-05T20:20:02+01:00 |
|
56fe724 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
Symbiotic |
1 |
2018-12-08T04:42 CET (sv-comp) |
|
Available Results for the Program from Witness Store SV-COMP '18
Trying to find witnesses for program (c8e6193201f070e4e8fd99485640ffa2e10139023e39442c320d13bfe62360e5, sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3.1_true-valid-memsafety_true-termination.i).
Found 11 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3.1_true-valid-memsafety_true-termination.i, c8e6193201f070e4e8fd99485640ffa2e10139023e39442c320d13bfe62360e5
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/c8e6193201f070e4e8fd99485640ffa2e10139023e39442c320d13bfe62360e5.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
b6fe4fc |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
Symbiotic |
1 |
2017-12-03T00:05 CET (sv-comp) |
|
10f370c |
Inspect |
|
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) |
violation_witness |
ESBMC 3.1 |
7 |
2017-12-01T09:16 CET (sv-comp) |
|
a4c28c9 |
Inspect |
|
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) |
correctness_witness |
ESBMC 4.6.0 kind |
3 |
2017-12-02T10:38:57.100653 |
|
ae2f75c |
Inspect |
|
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) |
correctness_witness |
ESBMC 4.6.0 incr |
3 |
2017-12-01T23:05:36.102980 |
|
2e88be7 |
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:26 CET (sv-comp) |
|
9875812 |
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:30 CET (sv-comp) |
|
dd7d909 |
Inspect |
|
CHECK( init(main()), LTL(G valid-deref) ) |
correctness_witness |
CPAchecker 1.6.1-svn 26773 |
6 |
2017-12-01T08:29:31+01:00 |
|
78dfd27 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
ESBMC 4.6.0 |
3 |
2017-12-02T19:42:33.483531 |
|
eface54 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
ESBMC 4.6.0 |
3 |
2017-12-02T09:48:49.425197 |
|
30bd90e |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
ESBMC 3.1 |
6 |
2017-12-01T21:27 CET (sv-comp) |
|
41d86ce |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
CBMC |
8 |
2017-12-01T13:28 CET (sv-comp) |
|
Available Results for the Program from Witness Store SV-COMP '17
Trying to find witnesses for program (c8e6193201f070e4e8fd99485640ffa2e10139023e39442c320d13bfe62360e5, sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3.1_true-valid-memsafety_true-termination.i).
Found 0 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3.1_true-valid-memsafety_true-termination.i, c8e6193201f070e4e8fd99485640ffa2e10139023e39442c320d13bfe62360e5
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/c8e6193201f070e4e8fd99485640ffa2e10139023e39442c320d13bfe62360e5.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |