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/forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i
programSHA 51ebf434d9764df50bd5afd11ada7c6c89fde2174c530c385c4e50a2aefb2cf4
witnessName results-verified/uautomizer.2017-12-02_0106.logfiles/sv-comp18.dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i.files/witness.graphml
witnessSHA 12cc63288014b6d33002dcd93cb194a05dbd824102f3ac8b653822060be22166

Information about the Witness from Competition Database

from https://sv-comp.sosy-lab.org/2018/results/witnessInfoByHash/12cc63288014b6d33002dcd93cb194a05dbd824102f3ac8b653822060be22166.json

Key Value
architecture 32bit
creationtime 2017-12-02T05:34Z
producer Automizer
program-sha256 51ebf434d9764df50bd5afd11ada7c6c89fde2174c530c385c4e50a2aefb2cf4
programfile /tmp/vcloud-vcloud-master/worker/working_dir_53566d4e-6e18-4018-ba33-d8f3e9c77331/sv-benchmarks/c/forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i
programhash 1f270b702de634d3ad2ee5a400388c6410a4cf10
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/12cc63288014b6d33002dcd93cb194a05dbd824102f3ac8b653822060be22166.graphml
witness-sha256 12cc63288014b6d33002dcd93cb194a05dbd824102f3ac8b653822060be22166
witness-size 7678
witness-type violation_witness

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

Trying to find witnesses for program (51ebf434d9764df50bd5afd11ada7c6c89fde2174c530c385c4e50a2aefb2cf4, sv-benchmarks/c/forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i).

Found 0 witnesses for program sv-benchmarks/c/forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i, 51ebf434d9764df50bd5afd11ada7c6c89fde2174c530c385c4e50a2aefb2cf4
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/51ebf434d9764df50bd5afd11ada7c6c89fde2174c530c385c4e50a2aefb2cf4.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 '23

Trying to find witnesses for program (51ebf434d9764df50bd5afd11ada7c6c89fde2174c530c385c4e50a2aefb2cf4, sv-benchmarks/c/forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i).

Found 0 witnesses for program sv-benchmarks/c/forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i, 51ebf434d9764df50bd5afd11ada7c6c89fde2174c530c385c4e50a2aefb2cf4
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/51ebf434d9764df50bd5afd11ada7c6c89fde2174c530c385c4e50a2aefb2cf4.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 '22

Trying to find witnesses for program (51ebf434d9764df50bd5afd11ada7c6c89fde2174c530c385c4e50a2aefb2cf4, sv-benchmarks/c/forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i).

Found 0 witnesses for program sv-benchmarks/c/forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i, 51ebf434d9764df50bd5afd11ada7c6c89fde2174c530c385c4e50a2aefb2cf4
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/51ebf434d9764df50bd5afd11ada7c6c89fde2174c530c385c4e50a2aefb2cf4.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 '21

Trying to find witnesses for program (51ebf434d9764df50bd5afd11ada7c6c89fde2174c530c385c4e50a2aefb2cf4, sv-benchmarks/c/forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i).

Found 0 witnesses for program sv-benchmarks/c/forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i, 51ebf434d9764df50bd5afd11ada7c6c89fde2174c530c385c4e50a2aefb2cf4
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/51ebf434d9764df50bd5afd11ada7c6c89fde2174c530c385c4e50a2aefb2cf4.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 '20

Trying to find witnesses for program (51ebf434d9764df50bd5afd11ada7c6c89fde2174c530c385c4e50a2aefb2cf4, sv-benchmarks/c/forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i).

Found 28 witnesses for program sv-benchmarks/c/forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i, 51ebf434d9764df50bd5afd11ada7c6c89fde2174c530c385c4e50a2aefb2cf4
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/51ebf434d9764df50bd5afd11ada7c6c89fde2174c530c385c4e50a2aefb2cf4.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 932bd6a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 2 2019-12-01 06:14:49
Download d1db846 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 10 2019-12-11T21:42:24+01:00 Download d20ce0b
Download 9156bdb Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 15 2019-12-11T20:54:58+01:00 Download cb937d3
Download a7f185e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.9 10 2019-12-11T21:44:48+01:00 Download b6247b2
Download b6f1cbb Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.9 10 2019-12-03T08:11:21+01:00 Download 48adb12
Download b6247b2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ 10 2019-12-01T17:47:07+01:00
Download 54307d7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.9 12 2019-12-11T21:09:21+01:00 Download 932bd6a
Download 1069b08 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.9 13 2019-12-08T00:06:03+01:00 Download eb969e1
Download e4ded77 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.9 10 2019-12-07T21:16:43+01:00 Download 3c83c0a
Download 48adb12 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) correctness_witness CPAchecker 1.9 10 2019-11-29T21:33:11+01:00
Download 152da80 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.9 10 2019-12-08T00:26:48+01:00 Download 9301813
Download 94c7a14 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 1.9 10 2019-12-05T20:21:35+01:00 Download 3065870
Download da94993 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2019-12-01 09:12:45
Download fb7385b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 9 2019-12-11T21:40:09+01:00 Download c9054a5
Download abcd729 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 9 2019-12-11T21:30:30+01:00 Download 5d70ce3
Download 7a00406 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 9 2019-12-11T21:09:43+01:00 Download da94993
Download e725318 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 9 2019-12-11T20:54:26+01:00 Download 05b90a1
Download d0007fb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 9 2019-12-08T00:07:36+01:00 Download 2d2ad9a
Download 9761c71 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 9 2019-12-07T21:17:50+01:00 Download d5bd45f
Download d4e52c2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 9 2019-12-05T20:20:12+01:00 Download f477032
Download 58177a3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 9 2019-12-05T19:34:31+01:00 Download cf60166
Download dd068d0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 9 2019-12-03T08:09:39+01:00 Download 4b8d2ef
Download 4b8d2ef Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 9 2019-11-30T03:08:07+01:00
Download a3145e7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8 6 2019-12-07T10:38:55+01:00
Download c9054a5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 9 2019-12-01T01:56:19+01:00
Download 9999eb7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 10 2019-12-11T20:45:55+01:00 Download 75f1d52
Download 3ec2488 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 10 2019-12-08T01:52:34+01:00 Download a3145e7
Download 0645b48 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 10 2019-12-06T02:39:22+01:00 Download 9e366fb

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

Trying to find witnesses for program (51ebf434d9764df50bd5afd11ada7c6c89fde2174c530c385c4e50a2aefb2cf4, sv-benchmarks/c/forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i).

Found 36 witnesses for program sv-benchmarks/c/forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i, 51ebf434d9764df50bd5afd11ada7c6c89fde2174c530c385c4e50a2aefb2cf4
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/51ebf434d9764df50bd5afd11ada7c6c89fde2174c530c385c4e50a2aefb2cf4.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download f66b15d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 1 2018-12-08T01:18 CET (sv-comp)
Download 03ccc85 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 11 2018-12-09T20:23:04+01:00 Download 89ba2fd
Download 07a9899 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 11 2018-12-08T23:43:59+01:00 Download f66b15d
Download 2264f65 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 11 2018-12-06T10:14:13+01:00 Download 9e96ce6
Download 3a70e92 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 11 2018-12-06T09:42:16+01:00 Download fb79335
Download ccbb438 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 10 2018-12-08T01:56:47+01:00
Download 3f43623 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.7-svn 29852 10 2018-12-05T22:24:04+01:00
Download ffab74c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.7-svn 29852 14 2018-12-07T09:29:01+01:00 Download 4ab8bd5
Download 84de915 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) correctness_witness CPAchecker 1.7-svn 29852 10 2018-12-06T09:20:42+01:00 Download 6fc8ced
Download 52800c2 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:44:42
Download 997d09f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 11 2018-12-09T20:39:33+01:00 Download bb252fb
Download 7bfd57a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 11 2018-12-08T05:02:32+01:00 Download e691d30
Download 40cbe1c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 1.7-svn 29852 10 2018-12-08T22:11:53+01:00 Download 52800c2
Download a0fb4e6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2018-12-08T01:42 CET (sv-comp)
Download c1a24be Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 3 2018-12-08T13:59:18
Download d8fc1a4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7 6 2018-12-10T19:14:07+01:00
Download 093084f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 8 2018-12-08T03:33:46+01:00
Download 891ba07 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-10T10:48:41+01:00 Download 6a6a4c3
Download c39b6cb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-09T20:53:05+01:00 Download e3b051f
Download 137f3a4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-09T20:36:21+01:00 Download e78d969
Download 61839b7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-09T20:34:22+01:00 Download 8f8eca2
Download a04c8a7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-08T22:09:42+01:00 Download c1a24be
Download c53c1be Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-08T08:51:24+01:00 Download 093084f
Download c1e932a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-08T05:05:19+01:00 Download 7abd129
Download 56d86f7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-08T04:35:58+01:00 Download 6a6a4c3
Download 8bfa3f3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-07T09:27:59+01:00 Download 169f8b8
Download 6a08aca Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-06T10:18:27+01:00 Download 2d164e6
Download fd91e55 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-06T09:48:11+01:00 Download 25bdda0
Download 5eb04e9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-06T09:42:32+01:00 Download 626821f
Download 0c034bc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-06T09:17:49+01:00 Download a8a15f4
Download a072367 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-06T09:13:25+01:00 Download d81cdb8
Download 25bdda0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-05T12:20:05+01:00
Download d5a0ed1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 10 2018-12-10T20:35:08+01:00 Download d8fc1a4
Download 458942c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 10 2018-12-09T18:21:48+01:00 Download 2263659
Download b78c285 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 10 2018-12-08T23:44:42+01:00 Download a0fb4e6
Download 3d160ff Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 10 2018-12-07T01:08:16+01:00 Download c19aab3

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

Trying to find witnesses for program (51ebf434d9764df50bd5afd11ada7c6c89fde2174c530c385c4e50a2aefb2cf4, sv-benchmarks/c/forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i).

Found 25 witnesses for program sv-benchmarks/c/forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i, 51ebf434d9764df50bd5afd11ada7c6c89fde2174c530c385c4e50a2aefb2cf4
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/51ebf434d9764df50bd5afd11ada7c6c89fde2174c530c385c4e50a2aefb2cf4.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download de92ac4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 1 2017-12-03T00:16 CET (sv-comp)
Download 1dd94d7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 4.6.0 kind 7 2017-12-02T10:31:24.245220
Download 9088b4f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 4.6.0 incr 7 2017-12-01T23:51:34.311585
Download 3df1927 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 3.1 4 2017-12-01T09:35 CET (sv-comp)
Download 20399bf 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 Forester 6 2017-12-01T19:29 CET (sv-comp)
Download 0522c75 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 38 2017-12-01T08:28 CET (sv-comp)
Download aad5bd5 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 15 2017-12-03T04:04Z
Download 4ab8bd5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness PredatorHP 5 2017-12-01T21:50 CET (sv-comp)
Download c69565e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness Map2Check 3 2017-12-01T23:33 CET (sv-comp)
Download 439d2d3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Taipan 8 2017-12-02T18:32Z
Download 46b4522 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2017-12-02T11:48 CET (sv-comp)
Download 169f8b8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness PredatorHP 4 2017-12-01T20:54 CET (sv-comp)
Download 61005cb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Map2Check 2 2017-12-01T20:37 CET (sv-comp)
Download b85aee9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Kojak 8 2017-12-02T21:31Z
Download 9f20323 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Forester 6 2017-12-01T18:04 CET (sv-comp)
Download 348bd5c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 5 2017-12-02T01:25:06.285188
Download aafe648 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 4 2017-12-01T13:59:30.739383
Download 0a68fe4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 4 2017-12-01T06:44 CET (sv-comp)
Download d1298cb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 7 2017-11-30T13:59:09+01:00
Download 441cc2e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 11 2017-11-30T11:38:28+01:00
Download 06b4ac4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 5 2017-11-30T22:02:31+01:00
Download c7aa5e0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 7 2017-12-02T08:25:39+01:00
Download 6fd1cf1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 12 2017-12-01T00:56 CET (sv-comp)
Download 12cc632 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Automizer 8 2017-12-02T05:34Z
Download 84321d0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness 2LS 5 2017-11-30T16:50 CET (sv-comp)

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

Trying to find witnesses for program (51ebf434d9764df50bd5afd11ada7c6c89fde2174c530c385c4e50a2aefb2cf4, sv-benchmarks/c/forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i).

Found 0 witnesses for program sv-benchmarks/c/forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i, 51ebf434d9764df50bd5afd11ada7c6c89fde2174c530c385c4e50a2aefb2cf4
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/51ebf434d9764df50bd5afd11ada7c6c89fde2174c530c385c4e50a2aefb2cf4.json

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