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 (f8b4bb9a8f404cd020a4d6119f922da096d098a1547934faf4c16f394bfab92c, sv-benchmarks/c/memsafety-ext3/scopes3_false-valid-deref.c).

Found 32 witnesses for program sv-benchmarks/c/memsafety-ext3/scopes3_false-valid-deref.c, f8b4bb9a8f404cd020a4d6119f922da096d098a1547934faf4c16f394bfab92c
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/f8b4bb9a8f404cd020a4d6119f922da096d098a1547934faf4c16f394bfab92c.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download b3c99d0 Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2023-12-18T09:01:01+01:00
Download ffe79ee Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 3 2023-11-29T16:45:05Z
Download 660e3e2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 13 2023-12-19T05:27:15+01:00 Download de8f616
Download ebbba4b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 13 2023-12-18T12:04:39+01:00 Download b3c99d0
Download 6f93a3f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 13 2023-12-18T03:08:53+01:00 Download 6c8c532
Download ad64d8c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 13 2023-12-05T14:39:33+01:00 Download ac68857
Download 1f44d43 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 13 2023-12-04T16:45:19+01:00 Download bbb0e6d
Download cb95341 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 13 2023-12-04T12:13:01+01:00 Download b475e9d
Download 4ed4cf3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 13 2023-12-04T02:27:14+01:00 Download 109049b
Download 8939363 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 13 2023-12-03T06:18:20+01:00 Download a7751bb
Download 8e458b4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 13 2023-12-01T18:29:17+01:00 Download e41ad95
Download 0c58559 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 13 2023-11-30T13:44:24+01:00 Download e724be5
Download cd16f53 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 13 2023-11-30T09:44:08+01:00 Download ef9f71a
Download e724be5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 11 2023-11-30T06:47:10+01:00
Download 616add1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 13 2023-11-30T03:05:22+01:00 Download ffe79ee
Download a3be61c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 13 2023-11-29T08:34:56+01:00 Download 6428a4b
Download 810b1c0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 13 2023-11-28T23:50:08+01:00 Download 2ef73a7
Download 109049b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2.1-svn-e677b7cd46+ 13 2023-12-03T22:48:54+01:00
Download 6c8c532 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-38892M 23 2023-12-18T01:36:47+01:00
Download 9436161 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.3 5 2023-12-17T22:06:43+01:00 Download 6c38d76
Download 164d4a7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Bubaak 3 2023-12-01T21:12:19Z
Download e41ad95 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 7.4.0 incr 4 2023-12-01T11:03:58Z
Download de8f616 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 2.0.1-svn-a45b42da2f+ 13 2023-12-18T22:47:09+01:00
Download b475e9d 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 Taipan 17 2023-12-02T17:30:39Z
Download a7751bb 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 Kojak 17 2023-12-02T20:07:19Z
Download 6c38d76 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 2023-12-17T12:50:06+01:00
Download 6428a4b 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 Automizer 17 2023-11-28T23:22:18Z
Download 2ef73a7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness sv-sanitizers 0.1.1 3 2023-11-28T21:12:08Z
Download ef9f71a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness PredatorHP 4 2023-11-30T08:24:04Z
Download ac68857 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness Bubaak 3 2023-12-05T07:29:35Z
Download bbb0e6d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness Bubaak 3 2023-12-04T10:15:03Z
Download 7bc8d15 Inspect Inspect
Validate
- content: - segment: - waypoint: action: follow location: column: 5 file_name: vcloud_worker_vcloud-master_on_vcloud-master/run_dir_7e37d35b-8542-4621-9e45-3e34fb8e3563/sv-benchmarks/c/memsafety-ext3/scopes3.c line: 8 type: target entry_type: violation_sequence metadata: creation_time: '2023-11-29T16:45:05Z' format_version: '0.1' producer: name: symbiotic task: data_model: ILP32 input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_7e37d35b-8542-4621-9e45-3e34fb8e3563/sv-benchmarks/c/memsafety-ext3/scopes3.c : f8b4bb9a8f404cd020a4d6119f922da096d098a1547934faf4c16f394bfab92c input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_7e37d35b-8542-4621-9e45-3e34fb8e3563/sv-benchmarks/c/memsafety-ext3/scopes3.c 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 14 2023-11-30T03:00:41+01:00

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

Trying to find witnesses for program (f8b4bb9a8f404cd020a4d6119f922da096d098a1547934faf4c16f394bfab92c, sv-benchmarks/c/memsafety-ext3/scopes3_false-valid-deref.c).

Found 27 witnesses for program sv-benchmarks/c/memsafety-ext3/scopes3_false-valid-deref.c, f8b4bb9a8f404cd020a4d6119f922da096d098a1547934faf4c16f394bfab92c
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/f8b4bb9a8f404cd020a4d6119f922da096d098a1547934faf4c16f394bfab92c.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 21cf315 Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2022-12-09T07:02:14+01:00
Download 7458039 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 3 2022-12-12T16:41:56Z
Download ea2cd10 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 13 2023-01-29T10:44:31+01:00 Download 108cdc7
Download 4e00484 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 13 2023-01-29T06:52:54+01:00 Download 237deed
Download 24500c4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 13 2023-01-29T06:38:43+01:00 Download f389d1f
Download 3ca3cdb Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 13 2023-01-29T05:57:49+01:00 Download 7458039
Download 0227762 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 13 2023-01-29T04:19:20+01:00 Download 5abbc77
Download 5b90d18 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 13 2023-01-29T01:31:55+01:00 Download 55ad0bb
Download 297bf29 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 13 2023-01-28T21:06:09+01:00 Download f16a594
Download c816cf7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 13 2023-01-28T15:43:12+01:00 Download 0acb381
Download 98fe3e8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 13 2023-01-28T14:18:52+01:00 Download 21cf315
Download 57c1e41 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 13 2023-01-28T08:56:45+01:00 Download 59115c5
Download 2ad737e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 13 2023-01-28T06:01:40+01:00 Download a603428
Download c8b7993 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 13 2023-01-28T02:25:10+01:00 Download aeb8db8
Download 03170f1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 13 2023-01-28T00:29:12+01:00 Download 54b650e
Download 59115c5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 13 2022-12-10T20:20:58+01:00
Download 55ad0bb Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2.1-svn-1715bd67dc+ 13 2022-12-12T01:10:37+01:00
Download f16a594 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-a45b42da2f+ 13 2022-12-10T00:56:36+01:00
Download a603428 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-38892M 23 2022-12-09T03:11:15+01:00
Download f77541e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2 5 2023-01-28T04:23:29+01:00 Download 38c078f
Download 0acb381 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 7.0.0 incr 4 2022-12-18T22:56:19Z
Download aeb8db8 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:56:33Z
Download 108cdc7 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 Taipan 17 2022-12-14T10:14:45Z
Download f389d1f 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 Kojak 17 2022-12-14T22:08:37Z
Download 38c078f 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 2022-12-08T08:38:19+01:00
Download 237deed 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 Automizer 18 2022-12-13T11:22:35Z
Download 54b650e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness Bubaak 3 2022-12-08T15:51:53Z

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

Trying to find witnesses for program (f8b4bb9a8f404cd020a4d6119f922da096d098a1547934faf4c16f394bfab92c, sv-benchmarks/c/memsafety-ext3/scopes3_false-valid-deref.c).

Found 26 witnesses for program sv-benchmarks/c/memsafety-ext3/scopes3_false-valid-deref.c, f8b4bb9a8f404cd020a4d6119f922da096d098a1547934faf4c16f394bfab92c
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/f8b4bb9a8f404cd020a4d6119f922da096d098a1547934faf4c16f394bfab92c.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 2fa4a6a Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2021-12-07T09:17:47+01:00
Download d098a68 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 2 2021-12-10T17:23:21
Download abcdd7b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 3 2021-12-07T14:02:35Z
Download 3203c76 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 13 2021-12-10T21:26:15+01:00 Download 1dfb97b
Download 0951ca6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 13 2021-12-10T17:27:14+01:00 Download 1ddf804
Download c42d73c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 13 2021-12-10T08:33:34+01:00 Download 44f6564
Download b9e367d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 13 2021-12-09T16:03:08+01:00 Download 2e7e421
Download 5411a27 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 13 2021-12-09T06:21:33+01:00 Download 5abbc77
Download 540fcd7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 13 2021-12-08T21:09:43+01:00 Download e25676d
Download a32b75f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 13 2021-12-08T13:48:53+01:00 Download a3f2031
Download 76c752c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 13 2021-12-07T19:12:53+01:00 Download abcdd7b
Download 36e9519 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 13 2021-12-07T11:26:15+01:00 Download 2fa4a6a
Download ecac29c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 13 2021-12-07T04:56:08+01:00 Download c97fdc2
Download 5d0803d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 13 2021-12-07T02:35:02+01:00 Download d93a057
Download ebec40c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 13 2021-12-05T20:41:40+01:00 Download cab8c31
Download cab8c31 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 13 2021-12-05T17:42:34+01:00
Download c97fdc2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-38892M 23 2021-12-07T02:15:57+01:00
Download 78798b7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.1 5 2021-12-06T11:46:00+01:00 Download 4c9632b
Download a3f2031 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 6.8.0 incr 4 2021-12-08T10:06:36Z
Download e25676d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 2.0.1-svn-fe6f522dd3+ 13 2021-12-08T20:21:37+01:00
Download 44f6564 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 Taipan 17 2021-12-10T02:34:40Z
Download 1ddf804 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 Kojak 17 2021-12-10T10:34:43Z
Download 4c9632b 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 19 2021-12-06T11:14:29+01:00
Download d93a057 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 Automizer 18 2021-12-06T16:15:20Z
Download ba28bdf Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness SESL 2 2021-12-06T11:50:43+01:00
Download 2e7e421 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0.1-svn-eda176372c+ 13 2021-12-09T14:43:00+01:00

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

Trying to find witnesses for program (f8b4bb9a8f404cd020a4d6119f922da096d098a1547934faf4c16f394bfab92c, sv-benchmarks/c/memsafety-ext3/scopes3_false-valid-deref.c).

Found 17 witnesses for program sv-benchmarks/c/memsafety-ext3/scopes3_false-valid-deref.c, f8b4bb9a8f404cd020a4d6119f922da096d098a1547934faf4c16f394bfab92c
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/f8b4bb9a8f404cd020a4d6119f922da096d098a1547934faf4c16f394bfab92c.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 94d33d3 Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2020-12-06T18:30:24+01:00
Download 5813f14 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 2 2020-12-11T17:37:40
Download 8ba0ac3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 2 2020-12-08T23:35:18
Download 67c1866 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 13 2020-12-12T01:27:01+01:00 Download 5813f14
Download 8ae8fca Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 13 2020-12-09T21:44:22+01:00 Download dc06c03
Download 403696c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 13 2020-12-06T19:41:00+01:00 Download 94d33d3
Download ec3b876 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 13 2020-12-05T12:17:37+01:00
Download 61849f1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-eda176372c+ 13 2020-12-07T23:41:30+01:00
Download f3b470f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0 5 2020-12-06T07:48:15+01:00 Download ab700df
Download cc9d518 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 2.0 13 2020-12-09T22:05:58+01:00 Download 94425a3
Download 22702ae Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 2.0 13 2020-12-09T03:58:06+01:00 Download 8ba0ac3
Download 6a82793 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 2.0 13 2020-12-08T06:34:10+01:00 Download 61849f1
Download 523bdce Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) correctness_witness CPAchecker 2.0 5 2020-12-06T18:26:25+01:00 Download ab700df
Download 51cb718 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0 13 2020-12-09T02:07:11+01:00 Download 1adba67
Download abcba66 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0 13 2020-12-07T16:35:02+01:00 Download bdcbd51
Download 27bc564 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0 13 2020-12-06T18:01:49+01:00 Download ec3b876
Download 345afb3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0 13 2020-12-05T18:44:38+01:00 Download ec3b876

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

Trying to find witnesses for program (f8b4bb9a8f404cd020a4d6119f922da096d098a1547934faf4c16f394bfab92c, sv-benchmarks/c/memsafety-ext3/scopes3_false-valid-deref.c).

Found 14 witnesses for program sv-benchmarks/c/memsafety-ext3/scopes3_false-valid-deref.c, f8b4bb9a8f404cd020a4d6119f922da096d098a1547934faf4c16f394bfab92c
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/f8b4bb9a8f404cd020a4d6119f922da096d098a1547934faf4c16f394bfab92c.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 5320055 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 1 2019-12-01 04:35:13
Download e14e2f4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 13 2019-12-11T21:09:00+01:00 Download 5320055
Download 83075e9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.9 13 2019-12-11T22:00:35+01:00 Download 8e7916f
Download 6f09c33 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.9 13 2019-12-11T20:54:50+01:00 Download a8372d1
Download aefb346 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.9 13 2019-12-03T08:56:54+01:00 Download c5c4359
Download 9ecd024 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.9 13 2019-12-03T08:09:14+01:00 Download ecfa71f
Download fa9751e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) correctness_witness CPAchecker 1.9 4 2019-12-06T02:40:29+01:00 Download cc63667
Download d24eb09 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) correctness_witness CPAchecker 1.9 4 2019-12-05T20:20:22+01:00 Download a624de9
Download c6c6475 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.9 13 2019-12-11T21:39:38+01:00 Download 95c8956
Download 3ec16f7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.9 13 2019-12-08T00:26:09+01:00 Download 7861339
Download 9f14b10 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.9 13 2019-12-08T00:07:36+01:00 Download 5abbc77
Download c6eb0e8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.9 13 2019-12-07T21:16:23+01:00 Download 55ca859
Download ecfa71f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.9 13 2019-11-30T14:45:56+01:00
Download 95c8956 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ 13 2019-12-01T17:04:46+01:00

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

Trying to find witnesses for program (f8b4bb9a8f404cd020a4d6119f922da096d098a1547934faf4c16f394bfab92c, sv-benchmarks/c/memsafety-ext3/scopes3_false-valid-deref.c).

Found 14 witnesses for program sv-benchmarks/c/memsafety-ext3/scopes3_false-valid-deref.c, f8b4bb9a8f404cd020a4d6119f922da096d098a1547934faf4c16f394bfab92c
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/f8b4bb9a8f404cd020a4d6119f922da096d098a1547934faf4c16f394bfab92c.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download b70e19a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 1 2018-12-08T07:12 CET (sv-comp)
Download 7d7b93a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 13 2018-12-10T10:48:53+01:00 Download e1231a1
Download aa806db Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 13 2018-12-09T20:35:25+01:00 Download 1219478
Download 063780c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 13 2018-12-08T07:52:04+01:00 Download fa8f7a5
Download 2177182 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 13 2018-12-06T01:39:31+01:00
Download e98cce8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-06T09:19:48+01:00 Download 512a451
Download 976e613 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-06T09:17:47+01:00 Download 8c123a0
Download f4d4a2e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.7-svn 29852 13 2018-12-07T09:29:14+01:00 Download 86cad4f
Download fa8f7a5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 13 2018-12-07T06:40:38+01:00
Download d1ec047 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 13 2018-12-09T20:53:22+01:00 Download 5f20dc1
Download 635bfb3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 13 2018-12-09T20:28:25+01:00 Download cbc642f
Download 9d724a5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 13 2018-12-08T23:44:04+01:00 Download b70e19a
Download bca82de Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 13 2018-12-08T03:54:49+01:00 Download e1231a1
Download 1a16290 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 13 2018-12-06T09:48:55+01:00 Download 2177182

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

Trying to find witnesses for program (f8b4bb9a8f404cd020a4d6119f922da096d098a1547934faf4c16f394bfab92c, sv-benchmarks/c/memsafety-ext3/scopes3_false-valid-deref.c).

Found 0 witnesses for program sv-benchmarks/c/memsafety-ext3/scopes3_false-valid-deref.c, f8b4bb9a8f404cd020a4d6119f922da096d098a1547934faf4c16f394bfab92c
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/f8b4bb9a8f404cd020a4d6119f922da096d098a1547934faf4c16f394bfab92c.json

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

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

Trying to find witnesses for program (f8b4bb9a8f404cd020a4d6119f922da096d098a1547934faf4c16f394bfab92c, sv-benchmarks/c/memsafety-ext3/scopes3_false-valid-deref.c).

Found 0 witnesses for program sv-benchmarks/c/memsafety-ext3/scopes3_false-valid-deref.c, f8b4bb9a8f404cd020a4d6119f922da096d098a1547934faf4c16f394bfab92c
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/f8b4bb9a8f404cd020a4d6119f922da096d098a1547934faf4c16f394bfab92c.json

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