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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download b0e4d78 Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2023-12-18T10:56:19+01:00
Download beda36f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 3 2023-11-30T00:22:20Z
Download e29f552 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-19T05:26:18+01:00 Download 8605d6f
Download 4e4ac74 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-18T12:05:58+01:00 Download b0e4d78
Download ba5973a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-18T03:09:07+01:00 Download a7f464e
Download bcd8ddf Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-05T14:38:17+01:00 Download c51ab42
Download 9c79674 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-04T16:41:10+01:00 Download b906097
Download 6826d74 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-04T12:13:44+01:00 Download 2dadd2a
Download 29276bf Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-04T02:27:13+01:00 Download 3146696
Download 86fe91c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-03T06:19:11+01:00 Download 1c088d4
Download ab061fb Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-01T18:28:16+01:00 Download 3d87b49
Download 556e64c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-11-30T13:44:31+01:00 Download 14f0237
Download 6a64eac Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-11-30T09:44:09+01:00 Download a241479
Download 14f0237 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-11-30T07:44:56+01:00
Download ca0d789 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-11-30T03:05:44+01:00 Download beda36f
Download f590be0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-11-29T08:34:55+01:00 Download 961e37d
Download 422d8be Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-11-28T23:49:52+01:00 Download b68f8cb
Download 3146696 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2.1-svn-e677b7cd46+ 3 2023-12-03T22:45:01+01:00
Download a7f464e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-38892M 4 2023-12-18T02:14:36+01:00
Download 4cc2034 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.3 3 2023-12-17T22:08:09+01:00 Download db3a7a9
Download 17471f7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Bubaak 3 2023-12-01T19:38:28Z
Download 3d87b49 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:33:30Z
Download 8605d6f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 2.0.1-svn-a45b42da2f+ 3 2023-12-18T18:07:06+01:00
Download 2dadd2a 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 4 2023-12-02T11:43:44Z
Download 1c088d4 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 4 2023-12-02T21:00:29Z
Download db3a7a9 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 2023-12-17T16:24:34+01:00
Download 961e37d 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 4 2023-11-29T04:40:22Z
Download b68f8cb Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness sv-sanitizers 0.1.1 3 2023-11-28T21:05:46Z
Download a241479 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness PredatorHP 4 2023-11-30T08:24:17Z
Download c51ab42 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness Bubaak 3 2023-12-05T07:54:10Z
Download b906097 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness Bubaak 3 2023-12-04T14:08:11Z
Download 6f6f086 Inspect Inspect
Validate
- content: - segment: - waypoint: action: follow location: column: 5 file_name: vcloud_worker_vcloud-master_on_vcloud-master/run_dir_f09a7503-e8f3-45a1-9791-8ca110dfc6e2/sv-benchmarks/c/memsafety-ext3/scopes5.c line: 7 type: target entry_type: violation_sequence metadata: creation_time: '2023-11-30T00:22:20Z' format_version: '0.1' producer: name: symbiotic task: data_model: ILP32 input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_f09a7503-e8f3-45a1-9791-8ca110dfc6e2/sv-benchmarks/c/memsafety-ext3/scopes5.c : e5aa7fc476b23cf3c590ec0e83134b87eb137366becc080b05d62a7d4a14bb8b input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_f09a7503-e8f3-45a1-9791-8ca110dfc6e2/sv-benchmarks/c/memsafety-ext3/scopes5.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 4 2023-11-30T02:57:45+01:00

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 135674d Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2022-12-09T06:51:19+01:00
Download 8798c30 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 3 2022-12-12T17:41:36Z
Download 0b6d512 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-29T10:44:27+01:00 Download ca70ecd
Download effb5f0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-29T06:53:09+01:00 Download 31514e3
Download 19509e0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-29T06:38:54+01:00 Download 18821e7
Download 71b30c5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-29T05:57:11+01:00 Download 8798c30
Download 29c8b59 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-29T04:19:20+01:00 Download 9fd8859
Download 478cabb Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-29T01:31:00+01:00 Download 363176d
Download 1135f99 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-28T21:06:13+01:00 Download a98ba70
Download 90734ae Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-28T15:45:24+01:00 Download 23c30e2
Download 28d381b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-28T14:10:16+01:00 Download 135674d
Download 0313e27 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-28T08:56:39+01:00 Download 99c88d8
Download 02912a5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-28T06:01:12+01:00 Download 1a41373
Download cb2e720 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-28T02:22:54+01:00 Download 245d97b
Download 58fc1a1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-28T00:29:09+01:00 Download b43dd42
Download 99c88d8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2022-12-10T19:25:46+01:00
Download 363176d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2.1-svn-1715bd67dc+ 3 2022-12-12T02:44:00+01:00
Download 1a41373 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-38892M 4 2022-12-09T02:50:43+01:00
Download 1301ebb Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2 3 2023-01-28T04:22:02+01:00 Download f48b497
Download 23c30e2 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:42:01Z
Download 245d97b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 6.8.0 incr 4 2022-12-25T10:16:43Z
Download ca70ecd 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 4 2022-12-14T09:03:51Z
Download 18821e7 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 4 2022-12-15T00:40:03Z
Download f48b497 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 2022-12-08T02:27:57+01:00
Download 31514e3 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 4 2022-12-13T12:46:31Z
Download a98ba70 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0.1-svn-a45b42da2f+ 3 2022-12-10T00:00:31+01:00
Download b43dd42 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness Bubaak 3 2022-12-08T19:14:52Z

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 92e78d7 Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2021-12-07T09:15:24+01:00
Download 0311eb4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 2 2021-12-10T19:11:02
Download 53125f6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 3 2021-12-07T16:59:34Z
Download 18511bd Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-10T21:26:19+01:00 Download f8648c4
Download 4d28f77 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-10T17:26:55+01:00 Download 8f2d708
Download a58cd1e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-10T08:34:23+01:00 Download b95dd6d
Download ce300d0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-09T16:01:56+01:00 Download 118599a
Download b698c41 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-09T06:21:59+01:00 Download 9fd8859
Download 01d21fe Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-08T21:10:29+01:00 Download 301da08
Download 9f59618 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-08T13:47:53+01:00 Download ee20a3c
Download e1045f4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-07T19:12:41+01:00 Download 53125f6
Download aea25c0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-07T11:25:46+01:00 Download 92e78d7
Download b27cc75 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-07T04:56:17+01:00 Download 7c2b5f4
Download 53709bd Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-07T02:36:10+01:00 Download df69674
Download acf92e2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-05T20:41:24+01:00 Download 54b77dd
Download 54b77dd Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-05T16:59:03+01:00
Download 301da08 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-fe6f522dd3+ 3 2021-12-08T19:57:43+01:00
Download 118599a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-eda176372c+ 3 2021-12-09T12:50:55+01:00
Download 7c2b5f4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-38892M 4 2021-12-07T02:31:00+01:00
Download c6cce56 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.1 3 2021-12-06T11:47:35+01:00 Download 14b8c44
Download ee20a3c 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:38:16Z
Download b95dd6d 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 4 2021-12-10T05:47:14Z
Download 8f2d708 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 4 2021-12-10T08:51:48Z
Download 14b8c44 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CBMC 4 2021-12-06T07:33:32+01:00
Download df69674 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 4 2021-12-06T17:11:36Z
Download 9f83f16 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness SESL 2 2021-12-06T11:55:00+01:00

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 20a5390 Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2020-12-06T17:47:25+01:00
Download 8521436 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 2 2020-12-11T20:04:11
Download 70725a3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 2 2020-12-09T00:43:15
Download e782479 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 3 2020-12-12T01:37:24+01:00 Download 8521436
Download 5879c87 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 3 2020-12-09T21:48:11+01:00 Download ee63d2a
Download 1cc69b8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 3 2020-12-09T21:42:31+01:00 Download 362e686
Download caff12a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 3 2020-12-09T02:30:34+01:00 Download 1cfe3f3
Download a41fe1f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 3 2020-12-06T18:02:34+01:00 Download 4607fd5
Download a9a28aa Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0 3 2020-12-06T18:28:34+01:00 Download a8c965e
Download f9321b5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0 3 2020-12-06T07:40:24+01:00 Download a8c965e
Download 54ec89c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 2.0 3 2020-12-08T06:31:55+01:00 Download fb30898
Download 54e4291 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 2.0 3 2020-12-07T16:32:34+01:00 Download 11eb03a
Download 76a7840 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0 3 2020-12-09T03:59:51+01:00 Download 70725a3
Download ed6ca04 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0 3 2020-12-06T19:31:00+01:00 Download 20a5390
Download 27eda45 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0 3 2020-12-05T18:31:15+01:00 Download 4607fd5
Download 4607fd5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0 3 2020-12-05T14:11:37+01:00
Download fb30898 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0.1-svn-eda176372c+ 3 2020-12-08T00:39:36+01:00

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download c4f9664 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 1 2019-12-02 00:22:27
Download ea8a4d1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 3 2019-12-11T21:53:52+01:00 Download 3c3fa1c
Download 9a87174 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 3 2019-12-08T00:26:17+01:00 Download 7150f00
Download 201e0a4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 3 2019-12-07T21:17:31+01:00 Download 126ecbc
Download 16cd38e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 3 2019-12-03T08:09:15+01:00 Download 566cec2
Download 566cec2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 3 2019-11-30T10:26:44+01:00
Download 60e6717 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.9 3 2019-12-11T21:57:23+01:00 Download 72f5753
Download 6962b9f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.9 3 2019-12-11T21:09:38+01:00 Download c4f9664
Download 7c4db52 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.9 3 2019-12-11T20:54:19+01:00 Download e43ccc7
Download 019eb6e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.9 3 2019-12-08T00:06:01+01:00 Download 9fd8859
Download b6247b5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.9 3 2019-12-03T08:57:16+01:00 Download e44d2fd
Download 3c3fa1c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ 3 2019-12-01T06:11:06+01:00
Download 090de5e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 1.9 3 2019-12-06T02:38:11+01:00 Download f22f833
Download e0d274a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 1.9 3 2019-12-05T20:20:25+01:00 Download 30ef7f4

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download de2357d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 1 2018-12-08T01:47 CET (sv-comp)
Download a45de77 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-10T10:48:49+01:00 Download f16d268
Download 3c34dfd Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-09T20:53:16+01:00 Download 8e51931
Download 4579bd9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-09T20:34:08+01:00 Download b4c035a
Download 3224817 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-06T09:48:30+01:00 Download 52f3476
Download 70b463f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-09T20:39:23+01:00 Download db51497
Download ae49f95 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-08T08:08:26+01:00 Download 5decd88
Download 15ec88d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-07T09:26:25+01:00 Download bbd5d11
Download ecf0386 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) correctness_witness CPAchecker 1.7-svn 29852 3 2018-12-06T09:16:41+01:00 Download 7ea8b23
Download 67c544e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) correctness_witness CPAchecker 1.7-svn 29852 3 2018-12-06T09:10:02+01:00 Download 63f6a21
Download 5decd88 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 3 2018-12-07T09:01:56+01:00
Download 751da60 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-08T23:42:25+01:00 Download de2357d
Download fa5e2cf Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-08T04:34:14+01:00 Download f16d268
Download 52f3476 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-06T05:31:49+01:00

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

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

Found 0 witnesses for program sv-benchmarks/c/memsafety-ext3/scopes5_false-valid-deref.c, e5aa7fc476b23cf3c590ec0e83134b87eb137366becc080b05d62a7d4a14bb8b
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/e5aa7fc476b23cf3c590ec0e83134b87eb137366becc080b05d62a7d4a14bb8b.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 (e5aa7fc476b23cf3c590ec0e83134b87eb137366becc080b05d62a7d4a14bb8b, sv-benchmarks/c/memsafety-ext3/scopes5_false-valid-deref.c).

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

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