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).

View and Validate the Witness

Input Given to this Service about the Witness (URL Query)

Key Value
programName sv-benchmarks/c/memsafety-ext3/naturalNumbers1_false-valid-deref.c
programSHA 68fe5d136456ecb82ea00426715bf936d3e38ca581ddd26cec97e5010ad5777c
witnessName results-validated/cpa-seq-validate-violation-witnesses-cbmc-path.2018-12-06_0853.logfiles/sv-comp19_prop-memsafety.naturalNumbers1_false-valid-deref.c.files/witness.graphml
witnessSHA d9ba8b69d31121a1a164d81985b9c8788b8c369b953dbeb233622527809fa187

Information about the Witness from Competition Database

from https://sv-comp.sosy-lab.org/2019/results/witnessInfoByHash/d9ba8b69d31121a1a164d81985b9c8788b8c369b953dbeb233622527809fa187.json

Key Value
architecture 32bit
creationtime 2018-12-06T09:15:00+01:00
inputwitnesshash ffd4a26cb189fa66e19a0ee994b46f662e4d2ad4ff94d0db0095e7f7b61afd3b
producer CPAchecker 1.7-svn 29852
program-sha256 68fe5d136456ecb82ea00426715bf936d3e38ca581ddd26cec97e5010ad5777c
programfile ../../sv-benchmarks/c/memsafety-ext3/naturalNumbers1_false-valid-deref.c
programhash 68fe5d136456ecb82ea00426715bf936d3e38ca581ddd26cec97e5010ad5777c
sourcecodelang C
specification CHECK( init(main()), LTL(G valid-memtrack) )
witness-file witnessFileByHash/d9ba8b69d31121a1a164d81985b9c8788b8c369b953dbeb233622527809fa187.graphml
witness-sha256 d9ba8b69d31121a1a164d81985b9c8788b8c369b953dbeb233622527809fa187
witness-size 5891
witness-type correctness_witness

This witness was created for this program (cf. table above, 68fe5d136456ecb82ea00426715bf936d3e38ca581ddd26cec97e5010ad5777c).

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

Trying to find witnesses for program (68fe5d136456ecb82ea00426715bf936d3e38ca581ddd26cec97e5010ad5777c, sv-benchmarks/c/memsafety-ext3/naturalNumbers1_false-valid-deref.c).

Found 30 witnesses for program sv-benchmarks/c/memsafety-ext3/naturalNumbers1_false-valid-deref.c, 68fe5d136456ecb82ea00426715bf936d3e38ca581ddd26cec97e5010ad5777c
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/68fe5d136456ecb82ea00426715bf936d3e38ca581ddd26cec97e5010ad5777c.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 3afc797 Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2023-12-18T09:46:52+01:00
Download a4b4323 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 8 2023-12-18T12:07:54+01:00 Download 3afc797
Download c7c7b74 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 8 2023-12-17T22:09:53+01:00 Download 6631d26
Download 6439cc2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 8 2023-12-05T14:39:59+01:00 Download f066dac
Download 74fe65e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 8 2023-12-04T16:44:22+01:00 Download 46f8f69
Download 73f3748 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 8 2023-12-04T12:11:59+01:00 Download 534163c
Download 290a94d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 8 2023-12-01T22:53:32+01:00 Download 4d0359a
Download 34ab5bf Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 8 2023-12-01T18:27:42+01:00 Download 361561e
Download a24cb9d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 8 2023-11-30T13:45:14+01:00 Download e3b694a
Download f94b918 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 8 2023-11-30T09:44:12+01:00 Download a3cb887
Download e3b694a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 7 2023-11-30T08:30:11+01:00
Download 14ebcd8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 8 2023-11-29T08:33:48+01:00 Download 043b9a6
Download f49d8a9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 8 2023-11-28T23:49:42+01:00 Download c3ab716
Download 90c674b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2.1-svn-e677b7cd46+ 8 2023-12-04T00:20:49+01:00
Download c7006b5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-38892M 9 2023-12-18T01:37:49+01:00
Download c8587bd Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Symbiotic 3 2023-11-29T20:09:27Z
Download a23cd57 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.3 6 2023-12-19T05:26:04+01:00 Download 2ede77e
Download 65c3b92 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.3 6 2023-12-18T03:09:11+01:00 Download c7006b5
Download 4e2e67d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.3 6 2023-12-04T02:26:18+01:00 Download 90c674b
Download 361561e 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:13:46Z
Download 534163c 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 7 2023-12-02T13:13:41Z
Download 6631d26 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-17T20:54:16+01:00
Download 043b9a6 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 7 2023-11-29T01:11:50Z
Download 8680b48 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Kojak 10 2023-12-02T23:00:30Z
Download c3ab716 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness sv-sanitizers 0.1.1 3 2023-11-28T21:00:01Z
Download a3cb887 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness PredatorHP 4 2023-11-30T08:23:53Z
Download 2ede77e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0.1-svn-a45b42da2f+ 8 2023-12-18T20:09:29+01:00
Download f066dac Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness Bubaak 3 2023-12-05T08:43:11Z
Download 46f8f69 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness Bubaak 3 2023-12-04T12:28:00Z
Download 4d0359a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness Bubaak 3 2023-12-01T20:24:15Z

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

Trying to find witnesses for program (68fe5d136456ecb82ea00426715bf936d3e38ca581ddd26cec97e5010ad5777c, sv-benchmarks/c/memsafety-ext3/naturalNumbers1_false-valid-deref.c).

Found 26 witnesses for program sv-benchmarks/c/memsafety-ext3/naturalNumbers1_false-valid-deref.c, 68fe5d136456ecb82ea00426715bf936d3e38ca581ddd26cec97e5010ad5777c
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/68fe5d136456ecb82ea00426715bf936d3e38ca581ddd26cec97e5010ad5777c.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 33d5ddf Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2022-12-09T06:55:04+01:00
Download 4e45001 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 3 2022-12-12T14:27:05Z
Download 1e07686 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 8 2023-01-29T10:45:37+01:00 Download 3879a35
Download 9905f35 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 8 2023-01-29T06:53:06+01:00 Download 64e5d76
Download 942cdbc Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 8 2023-01-29T05:55:56+01:00 Download 4e45001
Download 11e9d12 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 8 2023-01-29T04:19:21+01:00 Download 226b4ac
Download acc06b1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 8 2023-01-28T15:42:35+01:00 Download 0f9b75d
Download cb69db9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 8 2023-01-28T14:21:12+01:00 Download 33d5ddf
Download b1d573e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 8 2023-01-28T04:23:48+01:00 Download f2a85d1
Download be5ba1f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 8 2023-01-28T02:24:12+01:00 Download f8f1f41
Download 45c72e6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 8 2023-01-28T00:30:32+01:00 Download 4723301
Download fbae707 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 8 2022-12-10T19:05:24+01:00
Download 415af61 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2.1-svn-1715bd67dc+ 8 2022-12-12T00:40:53+01:00
Download c7cc523 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-a45b42da2f+ 8 2022-12-10T04:40:27+01:00
Download 3a03fec Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-38892M 9 2022-12-09T02:59:40+01:00
Download a82f66e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2 6 2023-01-29T01:30:44+01:00 Download 415af61
Download 911fcb9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2 6 2023-01-28T21:06:17+01:00 Download c7cc523
Download c570333 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2 6 2023-01-28T08:54:39+01:00 Download fbae707
Download a284e68 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2 6 2023-01-28T06:01:27+01:00 Download 3a03fec
Download 0f9b75d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 7.0.0 incr 4 2022-12-19T02:33:06Z
Download f8f1f41 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 6.8.0 incr 4 2022-12-25T12:15:39Z
Download 3879a35 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 7 2022-12-14T07:25:45Z
Download f2a85d1 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-08T09:29:07+01:00
Download 64e5d76 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 7 2022-12-13T14:57:17Z
Download a486faf Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Kojak 9 2022-12-14T21:17:06Z
Download 4723301 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness Bubaak 3 2022-12-08T14:25:55Z

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

Trying to find witnesses for program (68fe5d136456ecb82ea00426715bf936d3e38ca581ddd26cec97e5010ad5777c, sv-benchmarks/c/memsafety-ext3/naturalNumbers1_false-valid-deref.c).

Found 24 witnesses for program sv-benchmarks/c/memsafety-ext3/naturalNumbers1_false-valid-deref.c, 68fe5d136456ecb82ea00426715bf936d3e38ca581ddd26cec97e5010ad5777c
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/68fe5d136456ecb82ea00426715bf936d3e38ca581ddd26cec97e5010ad5777c.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download b2035d4 Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2021-12-07T08:06:11+01:00
Download 9ac92b1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 2 2021-12-10T17:46:42
Download fb3c779 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 3 2021-12-07T16:29:53Z
Download 96325bf Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 8 2021-12-10T21:26:18+01:00 Download 40e58f1
Download fcf9a9d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 8 2021-12-10T08:33:32+01:00 Download b6773cc
Download 03c7e67 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 8 2021-12-09T06:21:46+01:00 Download 226b4ac
Download 074203d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 8 2021-12-08T13:47:24+01:00 Download baaa8b1
Download c3aa2ec Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 8 2021-12-07T19:11:30+01:00 Download fb3c779
Download 8fbfe30 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 8 2021-12-07T11:25:32+01:00 Download b2035d4
Download 1fb4d62 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 8 2021-12-07T02:36:21+01:00 Download 20a8249
Download a521c9c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 8 2021-12-06T11:46:25+01:00 Download 96f385f
Download 19b1af4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 8 2021-12-05T19:31:12+01:00
Download ceff023 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-fe6f522dd3+ 8 2021-12-08T18:14:07+01:00
Download ae34261 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-eda176372c+ 8 2021-12-09T14:34:26+01:00
Download a6a0b33 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-38892M 9 2021-12-07T02:10:29+01:00
Download a204d75 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.1 6 2021-12-09T15:59:46+01:00 Download ae34261
Download b69f737 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.1 6 2021-12-08T21:08:11+01:00 Download ceff023
Download 5f4a6a6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.1 6 2021-12-07T04:55:09+01:00 Download a6a0b33
Download f90d440 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.1 6 2021-12-05T20:39:48+01:00 Download 19b1af4
Download baaa8b1 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:07:21Z
Download b6773cc 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 7 2021-12-09T22:49:23Z
Download 96f385f 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 2021-12-06T08:15:32+01:00
Download 20a8249 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 7 2021-12-06T16:31:20Z
Download b13d8b2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Kojak 9 2021-12-10T10:27:16Z

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

Trying to find witnesses for program (68fe5d136456ecb82ea00426715bf936d3e38ca581ddd26cec97e5010ad5777c, sv-benchmarks/c/memsafety-ext3/naturalNumbers1_false-valid-deref.c).

Found 16 witnesses for program sv-benchmarks/c/memsafety-ext3/naturalNumbers1_false-valid-deref.c, 68fe5d136456ecb82ea00426715bf936d3e38ca581ddd26cec97e5010ad5777c
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/68fe5d136456ecb82ea00426715bf936d3e38ca581ddd26cec97e5010ad5777c.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 6c42776 Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2020-12-06T17:49:26+01:00
Download 7440ef7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 2 2020-12-11T17:15:47
Download 29d774e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 2 2020-12-08T23:59:42
Download 5da06ef Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 8 2020-12-12T01:33:42+01:00 Download 7440ef7
Download 9de7545 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 8 2020-12-09T21:47:51+01:00 Download fa36b5a
Download 9881248 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 8 2020-12-09T02:09:09+01:00 Download 08ec2e8
Download 8e12034 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 8 2020-12-07T16:24:59+01:00 Download 796440e
Download 549ca72 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 8 2020-12-06T18:27:07+01:00 Download 644f6ed
Download 6a7107b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 8 2020-12-06T07:33:37+01:00 Download 644f6ed
Download c44cb2c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 8 2020-12-05T15:21:50+01:00
Download 93c3d30 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-eda176372c+ 8 2020-12-08T04:15:10+01:00
Download 83d10b1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0 6 2020-12-06T18:02:38+01:00 Download c44cb2c
Download dbfd002 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0 8 2020-12-09T04:12:08+01:00 Download 29d774e
Download d889525 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0 8 2020-12-06T19:06:20+01:00 Download 6c42776
Download 547bb39 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 2.0 6 2020-12-08T07:43:49+01:00 Download 93c3d30
Download c973145 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 2.0 6 2020-12-05T18:04:03+01:00 Download c44cb2c

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

Trying to find witnesses for program (68fe5d136456ecb82ea00426715bf936d3e38ca581ddd26cec97e5010ad5777c, sv-benchmarks/c/memsafety-ext3/naturalNumbers1_false-valid-deref.c).

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 65a3369 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 1 2019-12-01 13:38:22
Download 346ee93 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 8 2019-12-08T00:27:21+01:00 Download c55ad6b
Download df28ae6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 8 2019-12-07T21:18:00+01:00 Download 012d6ec
Download 5bfab65 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 8 2019-12-06T02:40:45+01:00 Download bdd4762
Download b2ceb79 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 8 2019-12-03T08:57:32+01:00 Download 437df93
Download 570e479 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.9 6 2019-12-11T21:42:34+01:00 Download a6811da
Download 50123c0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.9 6 2019-12-05T20:21:35+01:00 Download a02b108
Download a586429 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.9 8 2019-12-11T21:09:17+01:00 Download 65a3369
Download 067cc5d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) correctness_witness CPAchecker 1.9 6 2019-12-11T21:38:59+01:00 Download ac86e35
Download e4a1ac4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.9 8 2019-12-11T20:54:20+01:00 Download 5f6a595
Download d9a74fb Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.9 8 2019-12-08T00:06:03+01:00 Download 226b4ac
Download 824f489 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.9 8 2019-11-30T01:34:39+01:00
Download a6811da Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ 8 2019-11-30T21:10:12+01:00
Download 5160ee6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 1.9 6 2019-12-03T08:10:11+01:00 Download 824f489

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

Trying to find witnesses for program (68fe5d136456ecb82ea00426715bf936d3e38ca581ddd26cec97e5010ad5777c, sv-benchmarks/c/memsafety-ext3/naturalNumbers1_false-valid-deref.c).

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 84bcfae Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 1 2018-12-08T17:52 CET (sv-comp)
Download 7a9ae40 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 9 2018-12-08T00:56:17+01:00
Download 372ec86 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-10T10:48:43+01:00 Download a38bb78
Download a0cbfa3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-08T23:44:03+01:00 Download 84bcfae
Download 726cf7e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-08T04:34:09+01:00 Download a38bb78
Download aff8945 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-06T09:49:18+01:00 Download 9a19bfa
Download 32c1249 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-06T09:18:50+01:00 Download e412f44
Download d9ba8b6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-06T09:15:00+01:00 Download ffd4a26
Download b8d69cd Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-08T05:00:47+01:00 Download 6b11b7f
Download 030361c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-07T09:26:51+01:00 Download 8301ab3
Download bcce031 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-06T10:17:35+01:00 Download b41992b
Download 2bf0c09 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-08T08:47:41+01:00 Download 7a9ae40
Download da08f49 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-07T01:15:40+01:00 Download 1ef3ee2
Download 9a19bfa Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-06T07:05:46+01:00

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

Trying to find witnesses for program (68fe5d136456ecb82ea00426715bf936d3e38ca581ddd26cec97e5010ad5777c, sv-benchmarks/c/memsafety-ext3/naturalNumbers1_false-valid-deref.c).

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

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

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