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 (377aee86f3d25151744ba97c5be1cc51175a6c56601277d198adc5214d6e67f8, sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3_false-valid-deref.i).

Found 27 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3_false-valid-deref.i, 377aee86f3d25151744ba97c5be1cc51175a6c56601277d198adc5214d6e67f8
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/377aee86f3d25151744ba97c5be1cc51175a6c56601277d198adc5214d6e67f8.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 98f4537 Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2023-12-18T09:12:53+01:00
Download 5cc9e88 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 3 2023-11-29T20:18:33Z
Download db1cf47 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-19T15:33:54+01:00 Download b5ef6ed
Download bd9a99d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-19T05:27:14+01:00 Download 272356a
Download c90f5f2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-18T12:02:06+01:00 Download 98f4537
Download 2b512d8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-18T03:09:52+01:00 Download c4243ca
Download 71f60ca Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-17T22:10:48+01:00 Download cf63783
Download 314d8de Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-05T14:37:41+01:00 Download 58418ca
Download 2dc698f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-04T16:43:07+01:00 Download d2486f4
Download f78a2ad Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-04T02:27:35+01:00 Download 19e5689
Download 8fe20a5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-01T22:53:33+01:00 Download 90e2114
Download 54614fd Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-11-30T13:42:46+01:00 Download 0c92acd
Download 0c92acd Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-11-30T09:10:18+01:00
Download cdf0c25 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-11-30T03:01:22+01:00 Download 5cc9e88
Download 1767083 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-11-28T23:49:49+01:00 Download 5d0c10e
Download 19e5689 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2.1-svn-e677b7cd46+ 3 2023-12-04T00:41:49+01:00
Download c4243ca Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-38892M 4 2023-12-18T01:34:57+01:00
Download ff77329 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.3 8 2023-12-01T18:27:16+01:00 Download e19cdba
Download e19cdba Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 7.4.0 incr 4 2023-12-01T10:49:32Z
Download b5ef6ed Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 2.0 3 2023-12-19T12:30:12+01:00
Download cf63783 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CBMC 3 2023-12-17T19:29:19+01:00
Download 5d0c10e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness sv-sanitizers 0.1.1 3 2023-11-28T22:17:24Z
Download 272356a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0.1-svn-a45b42da2f+ 3 2023-12-18T20:14:06+01:00
Download 58418ca Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness Bubaak 3 2023-12-05T11:40:32Z
Download d2486f4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness Bubaak 3 2023-12-04T09:53:12Z
Download 90e2114 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness Bubaak 3 2023-12-01T19:38:58Z
Download 636a4eb Inspect Inspect
Validate
- content: - segment: - waypoint: action: follow location: column: 2 file_name: vcloud_worker_vcloud-master_on_vcloud-master/run_dir_97b054c5-7637-49b4-bb32-10ae097d106b/sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3-2.i line: 41 type: target entry_type: violation_sequence metadata: creation_time: '2023-11-29T20:18:33Z' format_version: '0.1' producer: name: symbiotic task: data_model: ILP32 input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_97b054c5-7637-49b4-bb32-10ae097d106b/sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3-2.i : 377aee86f3d25151744ba97c5be1cc51175a6c56601277d198adc5214d6e67f8 input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_97b054c5-7637-49b4-bb32-10ae097d106b/sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3-2.i language: C specification: CHECK( init(main()), LTL(G valid-free) ),CHECK( init(main()), LTL(G valid-deref) ),CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 4 2023-11-30T02:58:45+01:00

Available Results for the Program from Witness Store SV-COMP '23

Trying to find witnesses for program (377aee86f3d25151744ba97c5be1cc51175a6c56601277d198adc5214d6e67f8, sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3_false-valid-deref.i).

Found 22 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3_false-valid-deref.i, 377aee86f3d25151744ba97c5be1cc51175a6c56601277d198adc5214d6e67f8
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/377aee86f3d25151744ba97c5be1cc51175a6c56601277d198adc5214d6e67f8.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download ee44764 Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2022-12-09T05:10:41+01:00
Download 118bb31 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 3 2022-12-12T12:11:35Z
Download d674ad2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-29T05:58:24+01:00 Download 118bb31
Download 695598e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-29T01:30:17+01:00 Download a6b7fba
Download 2b0c4e6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-29T00:54:36+01:00 Download da36b51
Download 0091ae7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-28T21:08:09+01:00 Download 91cf44b
Download bcad851 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-28T14:20:24+01:00 Download ee44764
Download eca75a4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-28T08:54:05+01:00 Download 6fec853
Download f29520b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-28T06:01:06+01:00 Download a7dee7d
Download 11ebe20 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-28T04:23:12+01:00 Download 5e514c2
Download 29b1aba Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-28T00:29:30+01:00 Download 641a1d0
Download 6fec853 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2022-12-10T20:43:58+01:00
Download a6b7fba Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2.1-svn-1715bd67dc+ 3 2022-12-12T00:48:53+01:00
Download 91cf44b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-a45b42da2f+ 3 2022-12-09T23:36:43+01:00
Download a7dee7d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-38892M 4 2022-12-09T02:28:07+01:00
Download 391b9b1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2 8 2023-01-28T15:45:11+01:00 Download 4098bc0
Download af88681 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2 8 2023-01-28T02:20:10+01:00 Download 33d278b
Download 4098bc0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 7.0.0 incr 4 2022-12-18T15:54:13Z
Download 33d278b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 6.8.0 incr 4 2022-12-25T08:50:23Z
Download 5e514c2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CBMC 3 2022-12-08T08:37:14+01:00
Download da36b51 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0 3 2022-12-11T02:09:55+01:00
Download 641a1d0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness Bubaak 3 2022-12-08T15:18:21Z

Available Results for the Program from Witness Store SV-COMP '22

Trying to find witnesses for program (377aee86f3d25151744ba97c5be1cc51175a6c56601277d198adc5214d6e67f8, sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3_false-valid-deref.i).

Found 20 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3_false-valid-deref.i, 377aee86f3d25151744ba97c5be1cc51175a6c56601277d198adc5214d6e67f8
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/377aee86f3d25151744ba97c5be1cc51175a6c56601277d198adc5214d6e67f8.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 72f8fad Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2021-12-07T09:19:38+01:00
Download d4a81bd Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 2 2021-12-10T18:10:38
Download 865aad9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 3 2021-12-07T14:04:30Z
Download bca652f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-09T16:00:36+01:00 Download c75911e
Download 2024650 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-08T21:06:49+01:00 Download e1a6f0f
Download b9db0a8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-07T19:11:48+01:00 Download 865aad9
Download 1daee13 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-07T11:24:51+01:00 Download 72f8fad
Download a79764d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-07T04:55:52+01:00 Download 6bfba35
Download ebaf831 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-06T12:47:29+01:00 Download b30b980
Download 2cb8fa5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-06T11:46:24+01:00 Download b1a320d
Download addeeb3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-05T20:39:05+01:00 Download 2077092
Download 2077092 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-05T18:30:57+01:00
Download 6bfba35 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-38892M 4 2021-12-07T01:56:48+01:00
Download 7929750 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.1 8 2021-12-10T21:25:38+01:00 Download 6e5f1a6
Download 630369b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.1 8 2021-12-08T13:49:35+01:00 Download e4475fb
Download e4475fb Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 6.8.0 incr 4 2021-12-08T04:54:32Z
Download e1a6f0f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 2.0.1-svn-fe6f522dd3+ 3 2021-12-08T20:06:41+01:00
Download b1a320d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CBMC 4 2021-12-06T07:39:17+01:00
Download b30b980 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness SESL 3 2021-12-06T11:28:06+01:00
Download c75911e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0.1-svn-eda176372c+ 3 2021-12-09T13:02:54+01:00

Available Results for the Program from Witness Store SV-COMP '21

Trying to find witnesses for program (377aee86f3d25151744ba97c5be1cc51175a6c56601277d198adc5214d6e67f8, sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3_false-valid-deref.i).

Found 14 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3_false-valid-deref.i, 377aee86f3d25151744ba97c5be1cc51175a6c56601277d198adc5214d6e67f8
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/377aee86f3d25151744ba97c5be1cc51175a6c56601277d198adc5214d6e67f8.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download c9edf43 Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2020-12-06T18:06:46+01:00
Download 6c4c285 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 2 2020-12-11T19:24:38
Download 0f235af Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 2 2020-12-09T00:30:12
Download 3c05f91 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 3 2020-12-12T01:20:21+01:00 Download 6c4c285
Download e0b14b2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 3 2020-12-09T03:59:01+01:00 Download 0f235af
Download 0027e40 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 3 2020-12-08T06:48:22+01:00 Download a8a4ccd
Download 84afcaf Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 3 2020-12-06T19:40:30+01:00 Download c9edf43
Download 5440c03 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 3 2020-12-06T18:25:27+01:00 Download af95878
Download f70114a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 3 2020-12-06T07:49:42+01:00 Download af95878
Download a8a4ccd Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-eda176372c+ 3 2020-12-08T03:07:58+01:00
Download 616122c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0 8 2020-12-07T16:34:56+01:00 Download ebfd887
Download c4208e9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 2.0 3 2020-12-06T18:00:26+01:00 Download c9caea0
Download 602d4ba Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0 3 2020-12-05T17:59:04+01:00 Download c9caea0
Download c9caea0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0 3 2020-12-05T17:11:55+01:00

Available Results for the Program from Witness Store SV-COMP '20

Trying to find witnesses for program (377aee86f3d25151744ba97c5be1cc51175a6c56601277d198adc5214d6e67f8, sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3_false-valid-deref.i).

Found 10 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3_false-valid-deref.i, 377aee86f3d25151744ba97c5be1cc51175a6c56601277d198adc5214d6e67f8
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/377aee86f3d25151744ba97c5be1cc51175a6c56601277d198adc5214d6e67f8.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download ca63a28 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 1 2019-12-01 14:24:25
Download 55e71c5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 3 2019-12-11T21:54:25+01:00 Download 2eb4708
Download 3dbb775 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 3 2019-12-06T02:38:02+01:00 Download e319b8f
Download 164d88f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 3 2019-12-03T08:10:15+01:00 Download e275e74
Download e275e74 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 3 2019-11-29T14:43:42+01:00
Download 2eb4708 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ 3 2019-12-01T01:47:56+01:00
Download d2aff32 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.9 3 2019-12-11T21:09:45+01:00 Download ca63a28
Download e978991 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.9 3 2019-12-05T20:20:30+01:00 Download 62e0cca
Download 66d8c2d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.9 3 2019-12-03T08:57:50+01:00 Download 3f57a79
Download c4cc3f7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) correctness_witness CPAchecker 1.9 8 2019-12-11T20:54:59+01:00 Download f9373e5

Available Results for the Program from Witness Store SV-COMP '19

Trying to find witnesses for program (377aee86f3d25151744ba97c5be1cc51175a6c56601277d198adc5214d6e67f8, sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3_false-valid-deref.i).

Found 15 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3_false-valid-deref.i, 377aee86f3d25151744ba97c5be1cc51175a6c56601277d198adc5214d6e67f8
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/377aee86f3d25151744ba97c5be1cc51175a6c56601277d198adc5214d6e67f8.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download d260e76 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 1 2018-12-08T03:18 CET (sv-comp)
Download bd34c58 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 3 2018-12-07T20:28:57+01:00
Download a5d58eb Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-10T10:48:54+01:00 Download 7ac8600
Download d5878db Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-08T23:44:42+01:00 Download d260e76
Download cc3611b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-08T08:49:37+01:00 Download bd34c58
Download c6e3272 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-06T09:48:10+01:00 Download a6acc9c
Download 1517697 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-06T09:18:33+01:00 Download a6bb557
Download 61c397b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-06T09:17:22+01:00 Download 7535854
Download a6acc9c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-06T02:11:31+01:00
Download 44b71ff Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.7-svn 29852 8 2018-12-06T10:20:09+01:00 Download 64779a5
Download 376450c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness SMACK 1.9.3 3 2018-12-08T11:00:58
Download c90406f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-08T22:11:04+01:00 Download 376450c
Download b511d68 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-08T04:12:57+01:00 Download 7ac8600
Download 50aa4e0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-07T01:18:41+01:00 Download 0968068
Download 9e6c929 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 1.7-svn 29852 8 2018-12-08T04:56:50+01:00 Download 0debcee

Available Results for the Program from Witness Store SV-COMP '18

Trying to find witnesses for program (377aee86f3d25151744ba97c5be1cc51175a6c56601277d198adc5214d6e67f8, sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3_false-valid-deref.i).

Found 6 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3_false-valid-deref.i, 377aee86f3d25151744ba97c5be1cc51175a6c56601277d198adc5214d6e67f8
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/377aee86f3d25151744ba97c5be1cc51175a6c56601277d198adc5214d6e67f8.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 3cce530 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 1 2017-12-03T00:25 CET (sv-comp)
Download 665ea4c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.6.1-svn 26773 3 2017-12-01T08:23:34+01:00
Download 6201f8c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 4.6.0 kind 4 2017-12-02T12:01:25.111407
Download 93855b1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 4.6.0 incr 4 2017-12-01T23:31:42.336180
Download 007f036 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 3.1 7 2017-12-01T09:24 CET (sv-comp)
Download fd2f33f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CBMC 4 2017-12-01T08:22 CET (sv-comp)

Available Results for the Program from Witness Store SV-COMP '17

Trying to find witnesses for program (377aee86f3d25151744ba97c5be1cc51175a6c56601277d198adc5214d6e67f8, sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3_false-valid-deref.i).

Found 0 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3_false-valid-deref.i, 377aee86f3d25151744ba97c5be1cc51175a6c56601277d198adc5214d6e67f8
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/377aee86f3d25151744ba97c5be1cc51175a6c56601277d198adc5214d6e67f8.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness