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 (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
Download a85265a Inspect Inspect
Validate
valid-memsafety correctness_witness DIVINE 4 2 2023-12-18T10:18:33+01:00
Download 93c46e7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Symbiotic 3 2023-11-30T00:08:59Z
Download b91de5f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.3 5 2023-11-30T05:48:20+01:00
Download f9806fc Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2.1-svn-e677b7cd46+ 5 2023-12-03T20:39:00+01:00
Download a5885bf Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0.1-svn-38892M 10 2023-12-18T02:00:47+01:00
Download a06fa47 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Bubaak 3 2023-12-05T09:55:17Z
Download 9b6eaf1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Bubaak 3 2023-12-04T09:53:36Z
Download f451cd6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Bubaak 3 2023-12-01T20:04:48Z
Download b6b906e 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:31:10Z
Download 5b593bd 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 9 2023-12-17T10:40:20+01:00
Download 210ec53 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 5 2023-12-18T18:34:07+01:00
Download 11cc5bb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 7.4.0 3 2023-12-01T14:56:24Z
Download 3813cdc Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 3 2023-11-29T19:37:55Z
Download 3a1a662 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Goblint (tags/svcomp24-0-gc2e9465a7) 3 2023-12-01T01:45:48Z
Download 2b2f83b Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 7 2023-12-17T20:13:08+01:00
Download 2f0d21b Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Bubaak 3 2023-12-05T12:08:15Z
Download 6b6609c Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Bubaak 3 2023-12-04T08:50:05Z
Download e3bdf66 Inspect Inspect
Validate
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
Download ce1bc9e Inspect Inspect
Validate
valid-memsafety correctness_witness DIVINE 4 2 2022-12-09T06:45:55+01:00
Download e0c4f3e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2 5 2022-12-10T18:38:31+01:00
Download c0cec93 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2.1-svn-1715bd67dc+ 5 2022-12-11T23:27:40+01:00
Download bc7fb77 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0.1-svn-38892M 10 2022-12-09T03:26:31+01:00
Download 81f7d01 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Bubaak 3 2022-12-08T18:20:55Z
Download fb0a5ba Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) correctness_witness ESBMC 7.0.0 incr 3 2022-12-19T00:14:09Z
Download a083d75 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:43:35Z
Download 338019b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 5 2022-12-09T17:17:52+01:00
Download 843fd23 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 9 2022-12-08T12:40:15+01:00
Download 0c82b72 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(reach_error())) ) correctness_witness ESBMC 6.8.0 3 2022-12-25T08:29:37Z
Download d34db41 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 7.0.0 3 2022-12-19T02:35:01Z
Download 8e32ee6 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 3 2022-12-12T15:46:56Z
Download 464a382 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 7 2022-12-08T05:23:38+01:00
Download dceda53 Inspect Inspect
Validate
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
Download e9b7c00 Inspect Inspect
Validate
valid-memsafety correctness_witness DIVINE 4 2 2021-12-07T09:24:16+01:00
Download 66ad77a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.1 5 2021-12-05T17:20:53+01:00
Download 728815d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0.1-svn-fe6f522dd3+ 5 2021-12-08T16:44:34+01:00
Download cdcd4f4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0.1-svn-eda176372c+ 5 2021-12-09T12:47:39+01:00
Download 67f2df0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0.1-svn-38892M 10 2021-12-07T03:38:17+01:00
Download 49a9372 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) correctness_witness ESBMC 6.8.0 incr 3 2021-12-08T09:12:59Z
Download 0ca5c2c 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 7 2021-12-06T08:41:29+01:00
Download 7fe1e5b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness SESL 3 2021-12-06T11:55:53+01:00
Download 6446eb7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(reach_error())) ) correctness_witness ESBMC 6.8.0 3 2021-12-08T03:39:54Z
Download 0563f1f Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 3 2021-12-07T13:56:25Z
Download 0e76a36 Inspect Inspect
Validate
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
Download 6c4db3a Inspect Inspect
Validate
valid-memsafety correctness_witness DIVINE 4 2 2020-12-06T17:48:30+01:00
Download 50a74df Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0 5 2020-12-05T13:43:44+01:00
Download fd8ff38 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 2.0.1-svn-eda176372c+ 5 2020-12-07T22:41:17+01:00
Download 1279a84 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 2 2020-12-11T19:16:59
Download d9c46d1 Inspect Inspect
Validate
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
Download 8de241d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ 5 2019-12-01T00:22:52+01:00
Download 240a990 Inspect Inspect
Validate
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
Download e18b616 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Symbiotic 1 2018-12-08T06:31 CET (sv-comp)
Download 5b841f6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 5 2018-12-07T12:10:20+01:00
Download a4f5822 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-05T22:06:43+01:00
Download 85bf6a8 Inspect Inspect
Validate
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
Download 0957242 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Symbiotic 1 2017-12-03T00:11 CET (sv-comp)
Download ee720d8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T08:34:27+01:00
Download afab639 Inspect Inspect
Validate
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
Download 49329e8 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:50:29.854920
Download c879eda 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 3 2017-12-01T23:20 CET (sv-comp)
Download 35071df 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:21 CET (sv-comp)
Download 9014726 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T23:55:34.750961
Download 6b80140 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T12:07:10.153147
Download d125b35 Inspect Inspect
Validate
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