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 (635b18d6f80f7fb9900da8d675380fff657b914eae0cc24d65a61c9c5ee07c25, sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-2.1_false-valid-free.i).

Found 25 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-2.1_false-valid-free.i, 635b18d6f80f7fb9900da8d675380fff657b914eae0cc24d65a61c9c5ee07c25
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/635b18d6f80f7fb9900da8d675380fff657b914eae0cc24d65a61c9c5ee07c25.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 22a2322 Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2023-12-18T09:43:22+01:00
Download c04c8ab Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 3 2023-11-29T21:48:52Z
Download 86ef50a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 5 2023-12-18T12:03:59+01:00 Download 22a2322
Download d23f479 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 5 2023-12-05T14:41:09+01:00 Download e7de7c4
Download 62f83bc Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 5 2023-12-04T16:39:24+01:00 Download bf4e2d2
Download fd607c7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 5 2023-12-01T22:56:15+01:00 Download 49b472c
Download 5d009be Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 5 2023-12-01T18:28:33+01:00 Download 8049b7d
Download 1f01ac4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 6 2023-11-30T08:00:15+01:00
Download 26098d3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 5 2023-11-30T03:03:48+01:00 Download c04c8ab
Download 19e7a6b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 5 2023-11-28T23:49:39+01:00 Download bde8864
Download df6d688 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2.1-svn-e677b7cd46+ 6 2023-12-03T22:01:53+01:00
Download c761497 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-38892M 9 2023-12-18T01:44:20+01:00
Download b1172d5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.3 5 2023-12-19T05:27:28+01:00 Download 920ea36
Download 0be3503 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.3 5 2023-12-18T03:09:42+01:00 Download c761497
Download 78f0615 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.3 5 2023-12-17T22:07:29+01:00 Download 9286813
Download e379a8f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.3 5 2023-12-04T02:25:46+01:00 Download df6d688
Download 7db9798 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.3 5 2023-11-30T13:43:27+01:00 Download 1f01ac4
Download 8049b7d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 7.4.0 incr 4 2023-12-01T16:02:50Z
Download bde8864 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness sv-sanitizers 0.1.1 3 2023-11-28T21:04:26Z
Download e7de7c4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness Bubaak 3 2023-12-05T11:00:40Z
Download bf4e2d2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness Bubaak 3 2023-12-04T08:35:45Z
Download 49b472c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness Bubaak 3 2023-12-01T20:40:26Z
Download 9286813 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 2023-12-17T10:27:02+01:00
Download 920ea36 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0.1-svn-a45b42da2f+ 6 2023-12-18T19:07:58+01:00
Download 54452b1 Inspect Inspect
Validate
- content: - segment: - waypoint: action: follow location: column: 2 file_name: vcloud_worker_vcloud-master_on_vcloud-master/run_dir_b0cb3a5a-14a7-4e71-bfe0-0c2c4bf1ae22/sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-2.1-2.i line: 46 type: target entry_type: violation_sequence metadata: creation_time: '2023-11-29T21:48:52Z' format_version: '0.1' producer: name: symbiotic task: data_model: ILP32 input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_b0cb3a5a-14a7-4e71-bfe0-0c2c4bf1ae22/sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-2.1-2.i : 635b18d6f80f7fb9900da8d675380fff657b914eae0cc24d65a61c9c5ee07c25 input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_b0cb3a5a-14a7-4e71-bfe0-0c2c4bf1ae22/sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-2.1-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 6 2023-11-30T03:00:38+01:00

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

Trying to find witnesses for program (635b18d6f80f7fb9900da8d675380fff657b914eae0cc24d65a61c9c5ee07c25, sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-2.1_false-valid-free.i).

Found 20 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-2.1_false-valid-free.i, 635b18d6f80f7fb9900da8d675380fff657b914eae0cc24d65a61c9c5ee07c25
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/635b18d6f80f7fb9900da8d675380fff657b914eae0cc24d65a61c9c5ee07c25.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 73408ad Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2022-12-09T06:33:55+01:00
Download 08f3cc3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 3 2022-12-12T17:15:59Z
Download 3cb0478 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 5 2023-01-29T05:56:29+01:00 Download 08f3cc3
Download f850772 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 5 2023-01-28T15:45:13+01:00 Download b215435
Download 59531fe Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 5 2023-01-28T14:16:48+01:00 Download 73408ad
Download cc57a23 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 5 2023-01-28T02:22:32+01:00 Download 4e5552c
Download 3f093b5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 5 2023-01-28T00:29:12+01:00 Download 088941e
Download 33291c5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 6 2022-12-10T16:47:51+01:00
Download 416bfa6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2.1-svn-1715bd67dc+ 6 2022-12-11T23:23:58+01:00
Download 16dce0c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-38892M 9 2022-12-09T03:12:10+01:00
Download d3e4fe2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2 5 2023-01-29T01:31:06+01:00 Download 416bfa6
Download 010d609 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2 5 2023-01-28T21:06:37+01:00 Download c062d92
Download 01946f7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2 5 2023-01-28T08:58:37+01:00 Download 33291c5
Download f7a87c5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2 5 2023-01-28T06:01:32+01:00 Download 16dce0c
Download 0b22948 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2 5 2023-01-28T04:21:48+01:00 Download 8c822b6
Download b215435 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 7.0.0 incr 4 2022-12-18T20:22:18Z
Download 4e5552c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 6.8.0 incr 4 2022-12-25T09:43:10Z
Download 088941e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness Bubaak 3 2022-12-08T20:04:06Z
Download 8c822b6 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 2022-12-08T12:01:46+01:00
Download c062d92 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0.1-svn-a45b42da2f+ 6 2022-12-10T03:25:32+01:00

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

Trying to find witnesses for program (635b18d6f80f7fb9900da8d675380fff657b914eae0cc24d65a61c9c5ee07c25, sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-2.1_false-valid-free.i).

Found 18 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-2.1_false-valid-free.i, 635b18d6f80f7fb9900da8d675380fff657b914eae0cc24d65a61c9c5ee07c25
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/635b18d6f80f7fb9900da8d675380fff657b914eae0cc24d65a61c9c5ee07c25.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 93c6a7b Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2021-12-07T09:40:23+01:00
Download a287226 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 2 2021-12-10T17:24:24
Download 4c122fb Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 3 2021-12-07T10:12:39Z
Download 609b7dc Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 5 2021-12-10T21:24:56+01:00 Download b1d9137
Download 70c9234 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 5 2021-12-08T13:48:54+01:00 Download fb5a7db
Download 4bf5a3b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 5 2021-12-07T19:12:47+01:00 Download 4c122fb
Download 1296bc1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 5 2021-12-07T11:27:19+01:00 Download 93c6a7b
Download 797825d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 6 2021-12-05T17:33:23+01:00
Download b02e0d8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-fe6f522dd3+ 6 2021-12-08T19:20:47+01:00
Download 0bac56e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-38892M 9 2021-12-07T02:20:11+01:00
Download 5818ca8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.1 5 2021-12-09T16:00:40+01:00 Download 75fb4b3
Download e1ba6fb Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.1 5 2021-12-08T21:09:34+01:00 Download b02e0d8
Download d185475 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.1 5 2021-12-07T04:55:30+01:00 Download 0bac56e
Download f368cda Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.1 5 2021-12-06T11:48:23+01:00 Download 9687e7a
Download 8848018 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.1 5 2021-12-05T20:41:27+01:00 Download 797825d
Download fb5a7db Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 6.8.0 incr 4 2021-12-08T11:17:23Z
Download 75fb4b3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 2.0.1-svn-eda176372c+ 6 2021-12-09T11:22:09+01:00
Download 9687e7a 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 9 2021-12-06T10:30:26+01:00

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

Trying to find witnesses for program (635b18d6f80f7fb9900da8d675380fff657b914eae0cc24d65a61c9c5ee07c25, sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-2.1_false-valid-free.i).

Found 14 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-2.1_false-valid-free.i, 635b18d6f80f7fb9900da8d675380fff657b914eae0cc24d65a61c9c5ee07c25
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/635b18d6f80f7fb9900da8d675380fff657b914eae0cc24d65a61c9c5ee07c25.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download c3fcb6e Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2020-12-06T17:50:23+01:00
Download b9fd0de Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 2 2020-12-11T18:54:21
Download e9d3b1c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 2 2020-12-09T00:25:09
Download 2f84bcb Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 5 2020-12-06T19:29:11+01:00 Download c3fcb6e
Download 551b0f5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-eda176372c+ 6 2020-12-08T01:42:37+01:00
Download 3e0081b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0 5 2020-12-06T18:25:25+01:00 Download 1d3f396
Download 293cc6f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0 5 2020-12-06T18:01:43+01:00 Download b2f8211
Download af409a5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0 5 2020-12-06T07:56:20+01:00 Download 1d3f396
Download c0f64eb Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0 5 2020-12-05T18:00:34+01:00 Download b2f8211
Download eb873de Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 2.0 5 2020-12-07T16:23:13+01:00 Download 2f4fd2e
Download f1ebb34 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) correctness_witness CPAchecker 2.0 5 2020-12-08T07:50:11+01:00 Download 551b0f5
Download f6b87d6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0 5 2020-12-12T01:41:13+01:00 Download b9fd0de
Download 2566377 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0 5 2020-12-09T04:13:35+01:00 Download e9d3b1c
Download b2f8211 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0 6 2020-12-05T14:07:49+01:00

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

Trying to find witnesses for program (635b18d6f80f7fb9900da8d675380fff657b914eae0cc24d65a61c9c5ee07c25, sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-2.1_false-valid-free.i).

Found 10 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-2.1_false-valid-free.i, 635b18d6f80f7fb9900da8d675380fff657b914eae0cc24d65a61c9c5ee07c25
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/635b18d6f80f7fb9900da8d675380fff657b914eae0cc24d65a61c9c5ee07c25.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 7e26069 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 1 2019-12-01 23:02:27
Download 07f2468 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.9 5 2019-12-11T21:26:09+01:00 Download 21ed9b9
Download 7e2c8e8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.9 5 2019-12-05T20:21:15+01:00 Download 540a6c4
Download 42c224d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.9 5 2019-12-03T08:56:49+01:00 Download de790e1
Download f35936c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.9 5 2019-12-11T21:09:42+01:00 Download 7e26069
Download b7fa4cd Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.9 5 2019-12-11T20:54:22+01:00 Download e8cc4d4
Download 21ed9b9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ 6 2019-12-01T01:55:52+01:00
Download 892b094 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) correctness_witness CPAchecker 1.9 5 2019-12-03T08:00:37+01:00 Download 3612857
Download e20fc3e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.9 5 2019-12-06T02:41:23+01:00 Download 1848036
Download 3612857 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.9 6 2019-11-29T15:05:36+01:00

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

Trying to find witnesses for program (635b18d6f80f7fb9900da8d675380fff657b914eae0cc24d65a61c9c5ee07c25, sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-2.1_false-valid-free.i).

Found 13 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-2.1_false-valid-free.i, 635b18d6f80f7fb9900da8d675380fff657b914eae0cc24d65a61c9c5ee07c25
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/635b18d6f80f7fb9900da8d675380fff657b914eae0cc24d65a61c9c5ee07c25.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 51201d6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 1 2018-12-08T07:05 CET (sv-comp)
Download 3ddb909 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 7 2018-12-08T23:43:52+01:00 Download 51201d6
Download 7fe57e1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 7 2018-12-08T05:05:04+01:00 Download 43532ea
Download e56f1d0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 7 2018-12-06T09:48:15+01:00 Download 06b55ca
Download 06b55ca Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 7 2018-12-05T09:49:55+01:00
Download 7af0aee Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 7 2018-12-07T15:46:19+01:00
Download 3dd0bf6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.7-svn 29852 7 2018-12-08T22:10:56+01:00 Download 7092b8d
Download 37dddb8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.7-svn 29852 7 2018-12-08T08:00:15+01:00 Download 7af0aee
Download 54d8899 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.7-svn 29852 7 2018-12-06T10:11:46+01:00 Download 0a7d14f
Download 7092b8d 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-08T17:04:11
Download 227d965 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 7 2018-12-07T01:11:56+01:00 Download e8df6aa
Download e7ac206 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-06T09:20:23+01:00 Download 7978bf1
Download 9388533 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-06T09:10:08+01:00 Download 99d455c

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

Trying to find witnesses for program (635b18d6f80f7fb9900da8d675380fff657b914eae0cc24d65a61c9c5ee07c25, sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-2.1_false-valid-free.i).

Found 6 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-2.1_false-valid-free.i, 635b18d6f80f7fb9900da8d675380fff657b914eae0cc24d65a61c9c5ee07c25
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/635b18d6f80f7fb9900da8d675380fff657b914eae0cc24d65a61c9c5ee07c25.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download bff66d5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 1 2017-12-02T23:10 CET (sv-comp)
Download c365a8e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.6.1-svn 26773 7 2017-12-01T08:30:07+01:00
Download 1518174 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:05.236802
Download 0ce3eb8 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:15:35.771454
Download 949ac9f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness Map2Check 3 2017-12-01T23:56 CET (sv-comp)
Download 5aed543 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 10 2017-12-01T08:28 CET (sv-comp)

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

Trying to find witnesses for program (635b18d6f80f7fb9900da8d675380fff657b914eae0cc24d65a61c9c5ee07c25, sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-2.1_false-valid-free.i).

Found 0 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-2.1_false-valid-free.i, 635b18d6f80f7fb9900da8d675380fff657b914eae0cc24d65a61c9c5ee07c25
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/635b18d6f80f7fb9900da8d675380fff657b914eae0cc24d65a61c9c5ee07c25.json

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