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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 4fbbb0d Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2023-12-18T08:58:50+01:00
Download 369eb99 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 3 2023-11-29T19:01:04Z
Download 9e04605 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-19T15:32:30+01:00 Download bff5042
Download 222e34b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-19T05:27:00+01:00 Download 5bb0ddc
Download 4e46153 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-18T12:05:12+01:00 Download 4fbbb0d
Download 3f56afb Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-18T03:09:48+01:00 Download 1e8bbf3
Download 5c8b337 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-17T22:07:35+01:00 Download a782499
Download d8671b3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-05T14:37:41+01:00 Download 82b1d8d
Download 502e806 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-04T16:39:23+01:00 Download ff6d6e8
Download 965386a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-04T02:26:11+01:00 Download 343fa00
Download 1588bc2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-01T22:53:45+01:00 Download 2b143ce
Download aed2e6e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-11-30T13:44:18+01:00 Download 5dfc125
Download 5dfc125 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-11-30T08:05:42+01:00
Download 96713b0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-11-30T03:04:55+01:00 Download 369eb99
Download dcd2be2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-11-28T23:49:41+01:00 Download 1d127a7
Download 343fa00 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2.1-svn-e677b7cd46+ 3 2023-12-03T22:10:43+01:00
Download bff5042 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 3 2023-12-19T10:39:18+01:00
Download 1e8bbf3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-38892M 4 2023-12-18T01:33:29+01:00
Download 97fc7e4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.3 6 2023-12-01T18:27:31+01:00 Download fd801f9
Download fd801f9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 7.4.0 incr 4 2023-12-01T13:17:26Z
Download a782499 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-17T12:12:06+01:00
Download 1d127a7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness sv-sanitizers 0.1.1 3 2023-11-28T21:52:06Z
Download 5bb0ddc Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0.1-svn-a45b42da2f+ 3 2023-12-19T00:56:43+01:00
Download 82b1d8d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness Bubaak 3 2023-12-05T09:25:47Z
Download ff6d6e8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness Bubaak 3 2023-12-04T05:21:53Z
Download 2b143ce Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness Bubaak 3 2023-12-01T20:51:04Z
Download 1b69ebd Inspect Inspect
Validate
- content: - segment: - waypoint: action: follow location: column: 2 file_name: vcloud_worker_vcloud-master_on_vcloud-master/run_dir_c7367ec9-4137-4685-90f1-5b72ee0d85c7/sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3.1-2.i line: 42 type: target entry_type: violation_sequence metadata: creation_time: '2023-11-29T19:01:04Z' format_version: '0.1' producer: name: symbiotic task: data_model: ILP32 input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_c7367ec9-4137-4685-90f1-5b72ee0d85c7/sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3.1-2.i : b1b021e6d9a2738a433255a5090e8bc6a16512946b766dfe0e7714e9e7b1f123 input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_c7367ec9-4137-4685-90f1-5b72ee0d85c7/sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3.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 4 2023-11-30T02:56:43+01:00

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 257f9df Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2022-12-09T06:52:26+01:00
Download f13de33 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 3 2022-12-12T10:41:01Z
Download 1511c2b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-29T05:58:41+01:00 Download f13de33
Download 7d51ad3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-29T01:31:08+01:00 Download 9403797
Download 3ca9d67 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-29T00:55:02+01:00 Download 4f09348
Download caced13 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-28T21:08:36+01:00 Download 3f481f2
Download 78f3090 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-28T14:13:06+01:00 Download 257f9df
Download d42e9da Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-28T08:56:19+01:00 Download 9e3b4ed
Download 380463e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-28T06:01:18+01:00 Download 9fb8409
Download 4357e47 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-28T04:23:14+01:00 Download 174e5a2
Download 763fb80 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-28T00:28:02+01:00 Download 32b52d5
Download 9e3b4ed Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2022-12-10T17:43:06+01:00
Download 9403797 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2.1-svn-1715bd67dc+ 3 2022-12-11T20:55:26+01:00
Download 4f09348 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 3 2022-12-11T05:59:16+01:00
Download 3f481f2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-a45b42da2f+ 3 2022-12-10T04:19:27+01:00
Download 9fb8409 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-38892M 4 2022-12-09T02:56:05+01:00
Download d346e8e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2 6 2023-01-28T15:45:25+01:00 Download 083db42
Download e16072b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2 6 2023-01-28T02:24:42+01:00 Download b65ea28
Download 083db42 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 7.0.0 incr 4 2022-12-18T16:38:38Z
Download b65ea28 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 6.8.0 incr 4 2022-12-25T11:51:23Z
Download 174e5a2 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-08T02:32:08+01:00
Download 32b52d5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness Bubaak 3 2022-12-08T15:39:58Z

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download e28c850 Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2021-12-07T09:18:52+01:00
Download c608f99 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 2 2021-12-10T19:18:21
Download da77726 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 3 2021-12-07T15:31:01Z
Download 2478edd Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-09T16:02:56+01:00 Download 88eeb26
Download 6547000 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-08T21:09:28+01:00 Download f0e5580
Download e03f66b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-07T19:14:04+01:00 Download da77726
Download 198b934 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-07T11:24:31+01:00 Download e28c850
Download dc97940 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-07T04:55:34+01:00 Download 95d90f8
Download 729e435 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-06T12:47:38+01:00 Download 1961c85
Download 75e3b6f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-06T11:49:34+01:00 Download 2f5d85a
Download 7f010ab Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-05T20:38:44+01:00 Download 282f171
Download 282f171 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-05T14:52:36+01:00
Download 88eeb26 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-eda176372c+ 3 2021-12-09T13:43:42+01:00
Download 95d90f8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-38892M 4 2021-12-07T02:30:26+01:00
Download 1647584 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.1 6 2021-12-10T21:27:18+01:00 Download e9b2060
Download 38b0b90 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.1 6 2021-12-08T13:49:44+01:00 Download 2719b6d
Download 2719b6d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 6.8.0 incr 4 2021-12-08T08:36:35Z
Download 2f5d85a 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-06T02:44:08+01:00
Download 1961c85 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness SESL 3 2021-12-06T11:40:00+01:00
Download f0e5580 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0.1-svn-fe6f522dd3+ 3 2021-12-08T18:46:03+01:00

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 76e7dff Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2020-12-06T18:42:02+01:00
Download 90af137 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 2 2020-12-11T14:40:47
Download 3a72ac9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 2 2020-12-08T15:03:25
Download e4a32e4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 3 2020-12-12T01:42:19+01:00 Download 90af137
Download 15fe4fb Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 3 2020-12-09T03:58:59+01:00 Download 3a72ac9
Download edcee6c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 3 2020-12-08T07:32:36+01:00 Download 28d9cbd
Download 91cd143 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 3 2020-12-06T18:26:29+01:00 Download 56c93f4
Download 09e1759 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 3 2020-12-06T18:01:48+01:00 Download 76d88b0
Download c5adce6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 3 2020-12-06T07:54:42+01:00 Download 56c93f4
Download 76d88b0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 3 2020-12-05T17:05:18+01:00
Download 28d9cbd Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-eda176372c+ 3 2020-12-08T00:01:54+01:00
Download 5c71ef5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0 6 2020-12-07T16:43:39+01:00 Download 2025d08
Download 5c739cf Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0 3 2020-12-06T19:16:45+01:00 Download 76e7dff
Download 54bd7c5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0 3 2020-12-05T18:42:49+01:00 Download 76d88b0

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 3670a5a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 1 2019-12-01 04:48:00
Download baa3646 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 3 2019-12-06T02:39:24+01:00 Download e2594db
Download 9986154 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 3 2019-12-03T08:10:35+01:00 Download f47287b
Download 9dd95b3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ 3 2019-12-01T00:11:50+01:00
Download c5c24cb Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.9 6 2019-12-11T20:54:19+01:00 Download c318cad
Download f47287b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.9 3 2019-11-29T14:50:00+01:00
Download dbb5994 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.9 3 2019-12-11T21:41:53+01:00 Download 9dd95b3
Download 0b06757 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.9 3 2019-12-11T21:09:21+01:00 Download 3670a5a
Download 4abb338 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.9 3 2019-12-05T20:20:12+01:00 Download 61ebb63
Download 85fb616 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.9 3 2019-12-03T08:57:48+01:00 Download 4b72209

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download b32668f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 1 2018-12-08T07:37 CET (sv-comp)
Download 6ff0ae1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-10T10:48:50+01:00 Download ae5b12c
Download 85962a7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-08T23:44:48+01:00 Download b32668f
Download beeac0d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-08T08:24:17+01:00 Download c551e1c
Download 20c745a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-06T09:00:30+01:00 Download fb00a18
Download 5c82bc6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-06T07:24:42+01:00
Download f6c584f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-06T10:09:40+01:00 Download 6724cc8
Download e880386 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-06T09:48:06+01:00 Download 5c82bc6
Download 3c674f5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-06T09:19:31+01:00 Download b8df7a6
Download bed3fa4 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-08T06:45:51
Download c551e1c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 3 2018-12-07T01:37:29+01:00
Download 25a6b6b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-08T22:09:44+01:00 Download bed3fa4
Download f71cc6b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-08T03:45:29+01:00 Download ae5b12c
Download 158327b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-07T01:08:15+01:00 Download 18e30eb
Download 6450743 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-08T04:55:03+01:00 Download 2d24f47

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download abcf523 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 1 2017-12-03T00:27 CET (sv-comp)
Download 50bb843 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.6.1-svn 26773 3 2017-12-01T08:26:50+01:00
Download e9c9973 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 4.6.0 kind 4 2017-12-02T10:34:07.349692
Download 16c7b8f 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:40:36.988615
Download 02f8330 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 (b1b021e6d9a2738a433255a5090e8bc6a16512946b766dfe0e7714e9e7b1f123, sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3.1_false-valid-deref.i).

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

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