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

Found 25 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-2_false-valid-deref.i, 71977ff88a5661752c5d5a01d4769f04334116a88a2d9fa84ec77e61067c50d4
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/71977ff88a5661752c5d5a01d4769f04334116a88a2d9fa84ec77e61067c50d4.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download b5e7e67 Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2023-12-18T09:35:40+01:00
Download f057e52 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 3 2023-11-29T20:14:48Z
Download ade8075 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-19T05:26:09+01:00 Download 634b1a1
Download a6fd8e8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-18T12:05:35+01:00 Download b5e7e67
Download 71c5831 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-18T03:09:33+01:00 Download 32aa94c
Download 224ea21 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-17T22:09:02+01:00 Download fa1d731
Download 6069856 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-05T14:37:25+01:00 Download c677a4e
Download da9fccb Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-04T16:40:58+01:00 Download ac39b85
Download 32a9e30 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-04T02:26:19+01:00 Download c0a975f
Download adf3e98 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-01T22:55:05+01:00 Download b2512f7
Download 89954e0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-11-30T13:44:52+01:00 Download 8b82289
Download 8b82289 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 4 2023-11-30T07:01:34+01:00
Download 6799b63 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-11-30T03:01:09+01:00 Download f057e52
Download 899a27f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-11-28T23:49:32+01:00 Download 16804ad
Download c0a975f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2.1-svn-e677b7cd46+ 3 2023-12-03T20:32:33+01:00
Download 32aa94c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-38892M 5 2023-12-18T02:02:04+01:00
Download f6527b4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.3 5 2023-12-01T18:27:38+01:00 Download af7e10a
Download af7e10a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 7.4.0 incr 4 2023-12-01T15:57:11Z
Download fa1d731 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-17T16:59:26+01:00
Download 16804ad Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness sv-sanitizers 0.1.1 3 2023-11-28T21:05:24Z
Download 634b1a1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0.1-svn-a45b42da2f+ 3 2023-12-18T21:53:59+01:00
Download c677a4e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness Bubaak 3 2023-12-05T07:13:07Z
Download ac39b85 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness Bubaak 3 2023-12-04T08:34:59Z
Download b2512f7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness Bubaak 3 2023-12-01T20:21:40Z
Download 511dcb1 Inspect Inspect
Validate
- content: - segment: - waypoint: action: follow location: column: 2 file_name: vcloud_worker_vcloud-master_on_vcloud-master/run_dir_37fc73e8-efb7-4901-9feb-513b0cc06b5b/sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-2-1.i line: 31 type: target entry_type: violation_sequence metadata: creation_time: '2023-11-29T20:14:48Z' format_version: '0.1' producer: name: symbiotic task: data_model: ILP32 input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_37fc73e8-efb7-4901-9feb-513b0cc06b5b/sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-2-1.i : 71977ff88a5661752c5d5a01d4769f04334116a88a2d9fa84ec77e61067c50d4 input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_37fc73e8-efb7-4901-9feb-513b0cc06b5b/sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-2-1.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:56:24+01:00

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

Trying to find witnesses for program (71977ff88a5661752c5d5a01d4769f04334116a88a2d9fa84ec77e61067c50d4, sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-2_false-valid-deref.i).

Found 20 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-2_false-valid-deref.i, 71977ff88a5661752c5d5a01d4769f04334116a88a2d9fa84ec77e61067c50d4
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/71977ff88a5661752c5d5a01d4769f04334116a88a2d9fa84ec77e61067c50d4.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download b0eb3ef Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2022-12-09T06:29:04+01:00
Download fa08476 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 3 2022-12-12T13:19:53Z
Download fca9ec3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-29T05:57:35+01:00 Download fa08476
Download 56743ea Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-29T01:30:33+01:00 Download 2bb89a4
Download 3a7e784 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-28T21:05:51+01:00 Download 1d5de4b
Download 58a5532 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-28T14:16:56+01:00 Download b0eb3ef
Download a0f1365 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-28T08:54:00+01:00 Download 023bc9f
Download 281e56b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-28T06:01:00+01:00 Download 8a8476e
Download a931841 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-28T04:23:40+01:00 Download 7e164ef
Download b379350 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-28T00:28:02+01:00 Download 86c814a
Download 023bc9f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2022-12-10T19:24:53+01:00
Download 2bb89a4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2.1-svn-1715bd67dc+ 3 2022-12-11T19:41:28+01:00
Download 1d5de4b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-a45b42da2f+ 3 2022-12-10T02:55:56+01:00
Download 8a8476e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-38892M 5 2022-12-09T03:01:56+01:00
Download 79dcd4a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2 5 2023-01-28T15:44:20+01:00 Download ff960c8
Download 8efb9bf Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2 5 2023-01-28T02:24:34+01:00 Download 66a50b4
Download ff960c8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 7.0.0 incr 4 2022-12-18T23:51:20Z
Download 66a50b4 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:19:14Z
Download 7e164ef 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-08T04:13:31+01:00
Download 86c814a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness Bubaak 3 2022-12-08T13:03:30Z

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

Trying to find witnesses for program (71977ff88a5661752c5d5a01d4769f04334116a88a2d9fa84ec77e61067c50d4, sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-2_false-valid-deref.i).

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 55c480f Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2021-12-07T07:49:52+01:00
Download 420f649 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 2 2021-12-10T16:05:08
Download bf4a3dc Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 3 2021-12-07T14:23:40Z
Download 62b82e5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-09T16:03:11+01:00 Download 46fcd0d
Download 8562222 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-08T21:10:42+01:00 Download e3a3ec0
Download 4ca4de1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-07T19:11:02+01:00 Download bf4a3dc
Download 9b5c020 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-07T11:28:02+01:00 Download 55c480f
Download ff75c44 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-07T04:55:39+01:00 Download 48af3f7
Download 06611cd Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-06T12:47:38+01:00 Download 7a116d5
Download c48b654 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-06T11:46:14+01:00 Download 481c1fc
Download 5e34a16 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-05T20:41:16+01:00 Download d1e65b5
Download d1e65b5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-05T18:02:00+01:00
Download 46fcd0d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-eda176372c+ 3 2021-12-09T14:36:06+01:00
Download 48af3f7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-38892M 5 2021-12-07T02:11:45+01:00
Download 46781a8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.1 5 2021-12-10T21:26:24+01:00 Download 5b3be23
Download db67bd2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.1 5 2021-12-08T13:48:06+01:00 Download f8ebd89
Download f8ebd89 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 6.8.0 incr 4 2021-12-08T06:43:31Z
Download e3a3ec0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 2.0.1-svn-fe6f522dd3+ 3 2021-12-08T19:04:05+01:00
Download 481c1fc 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 5 2021-12-06T07:05:24+01:00
Download 7a116d5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness SESL 3 2021-12-06T11:57:09+01:00

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

Trying to find witnesses for program (71977ff88a5661752c5d5a01d4769f04334116a88a2d9fa84ec77e61067c50d4, sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-2_false-valid-deref.i).

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 543a486 Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2020-12-06T12:44:41+01:00
Download 28774e7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 2 2020-12-11T21:57:54
Download 92640de Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 2 2020-12-09T00:46:00
Download da130ef Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 3 2020-12-12T01:41:57+01:00 Download 28774e7
Download abd83c4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 3 2020-12-09T04:12:29+01:00 Download 92640de
Download a171930 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 3 2020-12-08T06:32:50+01:00 Download 143472a
Download 81fb524 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 3 2020-12-06T19:38:36+01:00 Download 543a486
Download 1c1781f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 3 2020-12-06T07:34:44+01:00 Download ad1f8fe
Download 3f587a3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 3 2020-12-05T15:18:26+01:00
Download 143472a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-eda176372c+ 3 2020-12-07T23:18:56+01:00
Download 4ccf5c5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 2.0 3 2020-12-06T18:01:46+01:00 Download 3f587a3
Download 2ebb649 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) correctness_witness CPAchecker 2.0 5 2020-12-07T16:30:11+01:00 Download acfd46c
Download c4fa6dd Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0 3 2020-12-06T18:28:30+01:00 Download ad1f8fe
Download dacc82f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0 3 2020-12-05T18:27:27+01:00 Download 3f587a3

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

Trying to find witnesses for program (71977ff88a5661752c5d5a01d4769f04334116a88a2d9fa84ec77e61067c50d4, sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-2_false-valid-deref.i).

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 679575c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 1 2019-12-01 10:09:48
Download f150a23 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 3 2019-12-11T21:09:09+01:00 Download 679575c
Download 6d3e5c9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 3 2019-12-05T20:21:39+01:00 Download f6e87a3
Download d0cb374 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 3 2019-11-30T09:53:16+01:00
Download 0409a20 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.9 3 2019-12-03T08:57:18+01:00 Download c8bd57e
Download 94b5106 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ 3 2019-11-30T21:27:21+01:00
Download c24a851 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.9 3 2019-12-11T22:00:26+01:00 Download 94b5106
Download 763eb5b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.9 3 2019-12-06T02:39:51+01:00 Download e8ed874
Download b9fbed5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.9 3 2019-12-03T08:09:02+01:00 Download d0cb374
Download 23c7b2d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 1.9 5 2019-12-11T20:54:48+01:00 Download 5b5ef41

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

Trying to find witnesses for program (71977ff88a5661752c5d5a01d4769f04334116a88a2d9fa84ec77e61067c50d4, sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-2_false-valid-deref.i).

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 0a1b8ea Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 1 2018-12-08T14:29 CET (sv-comp)
Download 105d40a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-08T22:10:08+01:00 Download 0393e62
Download 28a2c4b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-08T08:40:57+01:00 Download b6ad5ce
Download ee28607 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-06T09:48:45+01:00 Download 6821d97
Download 9e65db0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-06T09:19:58+01:00 Download 0ac0373
Download a388992 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-08T04:54:27+01:00 Download 5c4227b
Download b6ad5ce Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 5 2018-12-07T19:18:13+01:00
Download a4fe933 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-10T10:48:48+01:00 Download 01acbc7
Download 0393e62 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-08T05:37:15
Download 909ee52 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-08T23:43:42+01:00 Download 0a1b8ea
Download 3f4394e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-08T03:25:14+01:00 Download 01acbc7
Download 92d1cff Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-07T01:13:03+01:00 Download 089977d
Download f305f62 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-06T09:00:14+01:00 Download bee675f
Download 6821d97 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-06T04:05:27+01:00
Download 31a917b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-06T10:19:30+01:00 Download 761a515

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

Trying to find witnesses for program (71977ff88a5661752c5d5a01d4769f04334116a88a2d9fa84ec77e61067c50d4, sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-2_false-valid-deref.i).

Found 5 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-2_false-valid-deref.i, 71977ff88a5661752c5d5a01d4769f04334116a88a2d9fa84ec77e61067c50d4
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/71977ff88a5661752c5d5a01d4769f04334116a88a2d9fa84ec77e61067c50d4.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 5f036ad Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 1 2017-12-02T23:24 CET (sv-comp)
Download f1db14d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T08:34:20+01:00
Download 0d653a3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 4.6.0 kind 4 2017-12-02T11:47:12.164402
Download c5056fb 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:30:31.914125
Download a7e8ecb 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 6 2017-12-01T08:31 CET (sv-comp)

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

Trying to find witnesses for program (71977ff88a5661752c5d5a01d4769f04334116a88a2d9fa84ec77e61067c50d4, sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-2_false-valid-deref.i).

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

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