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).

This link does not point to a witness, but below is a list of witnesses for the same program.

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
Download a5a8039 Inspect Inspect
Validate
valid-memsafety correctness_witness DIVINE 4 2 2023-12-18T09:50:47+01:00
Download 4ab7532 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Symbiotic 3 2023-11-29T23:25:26Z
Download 63c213d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.3 6 2023-11-30T05:15:03+01:00
Download bccda4b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2.1-svn-e677b7cd46+ 6 2023-12-03T23:04:29+01:00
Download 56ef23b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0.1-svn-38892M 9 2023-12-18T02:13:21+01:00
Download 730265b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Bubaak 3 2023-12-05T10:24:07Z
Download 8522521 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Bubaak 3 2023-12-04T14:28:20Z
Download 9436f80 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Bubaak 3 2023-12-01T20:50:40Z
Download 65cb3e7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) correctness_witness ESBMC 7.4.0 incr 3 2023-12-01T03:24:35Z
Download 37c9e65 Inspect Inspect
Validate
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
Download e567e36 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 2.0 6 2023-12-19T10:48:44+01:00
Download 3a8f1c6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 6 2023-12-19T01:52:36+01:00
Download 8055fae Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 7.4.0 3 2023-12-01T10:11:08Z
Download ca74d93 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 3 2023-11-29T20:54:29Z
Download c47910d Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Goblint (tags/svcomp24-0-gc2e9465a7) 3 2023-11-30T22:33:36Z
Download 196567f Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 6 2023-12-17T08:55:21+01:00
Download ba5f98d Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Bubaak 3 2023-12-05T12:34:23Z
Download 411311a Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Bubaak 3 2023-12-04T09:09:50Z
Download 3df6c78 Inspect Inspect
Validate
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
Download 7dcb6b8 Inspect Inspect
Validate
valid-memsafety correctness_witness DIVINE 4 2 2022-12-09T05:09:10+01:00
Download 8492843 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Symbiotic 3 2022-12-12T11:52:53Z
Download a5c8368 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2 6 2022-12-10T17:52:02+01:00
Download 01019e6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2.1-svn-1715bd67dc+ 6 2022-12-12T02:14:37+01:00
Download e489937 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0 6 2022-12-11T03:54:07+01:00
Download fbb87e6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 6 2022-12-10T01:25:08+01:00
Download 0c3ba03 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0.1-svn-38892M 9 2022-12-09T03:25:35+01:00
Download 1135d7b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Bubaak 3 2022-12-08T21:12:32Z
Download f551f1e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) correctness_witness ESBMC 7.0.0 incr 3 2022-12-18T21:39:24Z
Download 75e57af Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) correctness_witness ESBMC 6.8.0 incr 3 2022-12-25T09:36:15Z
Download f97b1a8 Inspect Inspect
Validate
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
Download 5cff0e7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(reach_error())) ) correctness_witness ESBMC 6.8.0 3 2022-12-25T09:48:39Z
Download d9871c1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 7.0.0 3 2022-12-19T02:40:13Z
Download f8b3aa8 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 3 2022-12-12T14:33:39Z
Download 46c71d2 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 6 2022-12-08T07:25:59+01:00
Download 445b609 Inspect Inspect
Validate
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
Download 2da0e94 Inspect Inspect
Validate
valid-memsafety correctness_witness DIVINE 4 2 2021-12-07T09:12:55+01:00
Download e4e7075 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Symbiotic 3 2021-12-07T15:33:35Z
Download 672fc96 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.1 6 2021-12-05T17:23:03+01:00
Download 2f50c25 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0.1-svn-38892M 9 2021-12-07T02:03:40+01:00
Download 554b6d7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) correctness_witness ESBMC 6.8.0 incr 3 2021-12-08T06:24:03Z
Download a50bbc7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) correctness_witness CPAchecker 2.0.1-svn-fe6f522dd3+ 6 2021-12-08T19:34:11+01:00
Download 80b26dc Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) correctness_witness CPAchecker 2.0.1-svn-eda176372c+ 6 2021-12-09T11:50:17+01:00
Download 895893c Inspect Inspect
Validate
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
Download d06c781 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(reach_error())) ) correctness_witness ESBMC 6.8.0 3 2021-12-08T03:38:52Z
Download 15aa312 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 3 2021-12-07T12:06:21Z
Download 02ed330 Inspect Inspect
Validate
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
Download d0ab158 Inspect Inspect
Validate
valid-memsafety correctness_witness DIVINE 4 2 2020-12-06T18:45:55+01:00
Download fff151c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Symbiotic 2 2020-12-11T21:05:06
Download 40f6068 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Symbiotic 2 2020-12-09T02:25:57
Download 7649277 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) correctness_witness CPAchecker 2.0 6 2020-12-05T12:58:46+01:00
Download e2ea0f6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) correctness_witness CPAchecker 2.0.1-svn-eda176372c+ 6 2020-12-08T05:19:49+01:00
Download 6a6555b Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 2 2020-12-11T23:07:08
Download 6ec8c93 Inspect Inspect
Validate
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
Download 6b4f8a5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.9 6 2019-11-29T22:57:01+01:00
Download b26fc16 Inspect Inspect
Validate
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
Download 1c0b37c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Symbiotic 1 2018-12-08T16:53 CET (sv-comp)
Download 9d85aea Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 6 2018-12-08T00:52:03+01:00
Download d7baaa1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-05T20:20:02+01:00
Download 56fe724 Inspect Inspect
Validate
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
Download b6fe4fc Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Symbiotic 1 2017-12-03T00:05 CET (sv-comp)
Download 10f370c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 3.1 7 2017-12-01T09:16 CET (sv-comp)
Download a4c28c9 Inspect Inspect
Validate
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
Download ae2f75c Inspect Inspect
Validate
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
Download 2e88be7 Inspect Inspect
Validate
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)
Download 9875812 Inspect Inspect
Validate
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)
Download dd7d909 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-01T08:29:31+01:00
Download 78dfd27 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T19:42:33.483531
Download eface54 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T09:48:49.425197
Download 30bd90e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 6 2017-12-01T21:27 CET (sv-comp)
Download 41d86ce Inspect Inspect
Validate
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