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/sll-01_false-unreach-call_false-valid-deref.i
programSHA 04a668b517adc36b6ba64cb8bfea3a7d3c6080e86848215b01673710ab94b024
witnessName results-verified/cpa-bam-slicing.2017-11-30_1120.logfiles/sv-comp18.sll-01_false-unreach-call_false-valid-deref.i.files/witness.graphml
witnessSHA df6aaa949c9cde7cc3c0a622609073c4d46f90e97bedd6cc4bcba212a2262675

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2017-12-01T03:11:04+01:00
producer CPAchecker 1.6.1-svn 26758M
program-sha256 04a668b517adc36b6ba64cb8bfea3a7d3c6080e86848215b01673710ab94b024
programfile ../../sv-benchmarks/c/forester-heap/sll-01_false-unreach-call_false-valid-deref.i
programhash 31de2fb67e84e52bb7705ac8720e6b139fef2d91
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/df6aaa949c9cde7cc3c0a622609073c4d46f90e97bedd6cc4bcba212a2262675.graphml
witness-sha256 df6aaa949c9cde7cc3c0a622609073c4d46f90e97bedd6cc4bcba212a2262675
witness-size 20300
witness-type violation_witness

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

Trying to find witnesses for program (04a668b517adc36b6ba64cb8bfea3a7d3c6080e86848215b01673710ab94b024, sv-benchmarks/c/forester-heap/sll-01_false-unreach-call_false-valid-deref.i).

Found 0 witnesses for program sv-benchmarks/c/forester-heap/sll-01_false-unreach-call_false-valid-deref.i, 04a668b517adc36b6ba64cb8bfea3a7d3c6080e86848215b01673710ab94b024
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/04a668b517adc36b6ba64cb8bfea3a7d3c6080e86848215b01673710ab94b024.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 (04a668b517adc36b6ba64cb8bfea3a7d3c6080e86848215b01673710ab94b024, sv-benchmarks/c/forester-heap/sll-01_false-unreach-call_false-valid-deref.i).

Found 0 witnesses for program sv-benchmarks/c/forester-heap/sll-01_false-unreach-call_false-valid-deref.i, 04a668b517adc36b6ba64cb8bfea3a7d3c6080e86848215b01673710ab94b024
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/04a668b517adc36b6ba64cb8bfea3a7d3c6080e86848215b01673710ab94b024.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 (04a668b517adc36b6ba64cb8bfea3a7d3c6080e86848215b01673710ab94b024, sv-benchmarks/c/forester-heap/sll-01_false-unreach-call_false-valid-deref.i).

Found 0 witnesses for program sv-benchmarks/c/forester-heap/sll-01_false-unreach-call_false-valid-deref.i, 04a668b517adc36b6ba64cb8bfea3a7d3c6080e86848215b01673710ab94b024
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/04a668b517adc36b6ba64cb8bfea3a7d3c6080e86848215b01673710ab94b024.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 (04a668b517adc36b6ba64cb8bfea3a7d3c6080e86848215b01673710ab94b024, sv-benchmarks/c/forester-heap/sll-01_false-unreach-call_false-valid-deref.i).

Found 0 witnesses for program sv-benchmarks/c/forester-heap/sll-01_false-unreach-call_false-valid-deref.i, 04a668b517adc36b6ba64cb8bfea3a7d3c6080e86848215b01673710ab94b024
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/04a668b517adc36b6ba64cb8bfea3a7d3c6080e86848215b01673710ab94b024.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 (04a668b517adc36b6ba64cb8bfea3a7d3c6080e86848215b01673710ab94b024, sv-benchmarks/c/forester-heap/sll-01_false-unreach-call_false-valid-deref.i).

Found 25 witnesses for program sv-benchmarks/c/forester-heap/sll-01_false-unreach-call_false-valid-deref.i, 04a668b517adc36b6ba64cb8bfea3a7d3c6080e86848215b01673710ab94b024
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/04a668b517adc36b6ba64cb8bfea3a7d3c6080e86848215b01673710ab94b024.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 01e887b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 1 2019-12-02 00:43:28
Download eeccdf9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 17 2019-12-11T20:54:21+01:00 Download 4aa5fad
Download 97c9667 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 17 2019-12-08T00:26:25+01:00 Download a4dbb93
Download 4257a5d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 17 2019-12-07T21:17:20+01:00 Download 6de4aad
Download f52ca21 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 12 2019-12-06T02:39:40+01:00 Download 4e3ed52
Download bc242cc Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 17 2019-12-05T19:34:37+01:00 Download 8c93c68
Download e15c3cb Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.9 21 2019-12-03T08:09:58+01:00 Download 722952a
Download 722952a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.9 20 2019-11-29T21:56:36+01:00
Download da16034 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.9 17 2019-12-11T21:40:11+01:00 Download d88ad1c
Download bd82b18 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.9 13 2019-12-11T21:09:07+01:00 Download 01e887b
Download 23d6b72 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) correctness_witness CPAchecker 1.9 21 2019-12-11T21:45:37+01:00 Download f2681fc
Download 77e4f63 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) correctness_witness CPAchecker 1.9 21 2019-12-05T20:21:18+01:00 Download 9366d8e
Download f2681fc Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ 20 2019-12-01T18:09:05+01:00
Download 5393add Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.9 17 2019-12-08T00:07:32+01:00 Download 690457f
Download 0926da2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 15 2019-12-11T21:56:54+01:00 Download c7e724c
Download 4c5f020 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 15 2019-12-11T21:56:16+01:00 Download ac7ec78
Download da3c62f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 19 2019-12-11T20:54:51+01:00 Download 2d0dd39
Download 7a1cc7d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 15 2019-12-08T00:26:12+01:00 Download f10b86a
Download f25cd18 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 15 2019-12-07T21:17:26+01:00 Download c82d0bd
Download ef0cd15 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 15 2019-12-03T08:09:00+01:00 Download 770c811
Download 770c811 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 15 2019-11-30T12:19:24+01:00
Download 1485a0f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8 4 2019-12-07T11:07:27+01:00
Download c7e724c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 15 2019-12-01T13:46:47+01:00
Download 17b7c56 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 20 2019-12-08T01:51:36+01:00 Download 1485a0f
Download 52866dc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 21 2019-12-05T20:20:15+01:00 Download fea95ec

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

Trying to find witnesses for program (04a668b517adc36b6ba64cb8bfea3a7d3c6080e86848215b01673710ab94b024, sv-benchmarks/c/forester-heap/sll-01_false-unreach-call_false-valid-deref.i).

Found 30 witnesses for program sv-benchmarks/c/forester-heap/sll-01_false-unreach-call_false-valid-deref.i, 04a668b517adc36b6ba64cb8bfea3a7d3c6080e86848215b01673710ab94b024
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/04a668b517adc36b6ba64cb8bfea3a7d3c6080e86848215b01673710ab94b024.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 862527a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 1 2018-12-08T00:29 CET (sv-comp)
Download 53c0ade Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 12 2018-12-10T10:48:40+01:00 Download a74a19a
Download 2b0f8a5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 17 2018-12-09T20:53:15+01:00 Download c21c9dd
Download 7ce2e12 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 17 2018-12-09T20:39:55+01:00 Download 591edc9
Download d6415c2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 17 2018-12-09T20:26:08+01:00 Download d0242be
Download 10e1a9e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 17 2018-12-06T09:42:07+01:00 Download 2383255
Download 9f26790 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.7-svn 29852 17 2018-12-07T09:14:01+01:00 Download c2f66cc
Download 69888e9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.7-svn 29852 12 2018-12-06T10:17:50+01:00 Download 995c8fd
Download 3c8d090 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-08T02:11:03
Download 5c44294 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 12 2018-12-08T23:44:45+01:00 Download 862527a
Download 168eaaa Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 12 2018-12-08T22:09:22+01:00 Download 3c8d090
Download 030cdfb Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 12 2018-12-08T05:03:45+01:00 Download 04602b4
Download 3ea2a9a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 12 2018-12-08T03:39:35+01:00 Download a74a19a
Download 997c18b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 12 2018-12-07T01:17:24+01:00 Download 9954fd2
Download be3a436 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2018-12-08T07:40 CET (sv-comp)
Download 85c81d3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 3 2018-12-08T02:27:36
Download 69870af Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7 4 2018-12-10T17:43:40+01:00
Download e54152e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 15 2018-12-07T10:59:32+01:00
Download 472f1d1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 15 2018-12-09T20:53:21+01:00 Download 46bf54f
Download 50c1f47 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 15 2018-12-09T20:37:11+01:00 Download bef2d15
Download 4799750 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 15 2018-12-09T20:33:28+01:00 Download 1523490
Download 8cbc583 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 15 2018-12-08T08:55:02+01:00 Download e54152e
Download d413381 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 24 2018-12-08T05:05:44+01:00 Download 2c7b9e8
Download 5e7e0e7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 21 2018-12-06T10:12:10+01:00 Download 9450a38
Download 4dd4aaa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 15 2018-12-06T09:48:38+01:00 Download 2d9d68c
Download 7f1bebd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 21 2018-12-06T09:18:44+01:00 Download 6a6bbe0
Download 2d9d68c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 15 2018-12-06T00:29:47+01:00
Download ab8562e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 20 2018-12-10T20:35:16+01:00 Download 69870af
Download 8c848be Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 20 2018-12-08T23:43:30+01:00 Download be3a436
Download 9a6150d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 20 2018-12-08T22:10:59+01:00 Download 85c81d3

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

Trying to find witnesses for program (04a668b517adc36b6ba64cb8bfea3a7d3c6080e86848215b01673710ab94b024, sv-benchmarks/c/forester-heap/sll-01_false-unreach-call_false-valid-deref.i).

Found 23 witnesses for program sv-benchmarks/c/forester-heap/sll-01_false-unreach-call_false-valid-deref.i, 04a668b517adc36b6ba64cb8bfea3a7d3c6080e86848215b01673710ab94b024
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/04a668b517adc36b6ba64cb8bfea3a7d3c6080e86848215b01673710ab94b024.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 03185e9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 1 2017-12-03T00:16 CET (sv-comp)
Download 0cba977 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 4.6.0 kind 6 2017-12-02T10:45:07.430399
Download f89e2f5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 4.6.0 incr 5 2017-12-01T23:38:13.368357
Download d80f432 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 3.1 4 2017-12-01T09:24 CET (sv-comp)
Download 183fb99 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 11 2017-12-03T06:55Z
Download 907471f 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 11 2017-12-03T04:32Z
Download 12e341b 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 10 2017-12-01T19:12 CET (sv-comp)
Download 628bca3 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 2017-12-01T08:31 CET (sv-comp)
Download 8a608ba 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 10 2017-12-03T03:47Z
Download c102a09 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 2LS 7 2017-12-01T08:19 CET (sv-comp)
Download c2f66cc Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness PredatorHP 5 2017-12-01T21:51 CET (sv-comp)
Download 785d5a0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness Map2Check 3 2017-12-01T23:24 CET (sv-comp)
Download c994b44 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Taipan 13 2017-12-03T02:54Z
Download e0a0d50 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Kojak 12 2017-12-02T21:19Z
Download 7689902 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Forester 10 2017-12-01T17:47 CET (sv-comp)
Download bc89453 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 6 2017-12-02T00:20:47.693713
Download 45df104 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 6 2017-12-01T10:02:16.525423
Download fa8dc13 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 5 2017-12-01T03:31 CET (sv-comp)
Download 30ed9c9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 18 2017-11-30T11:49:45+01:00
Download df6aaa9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 20 2017-12-01T03:11:04+01:00
Download f59d188 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 4 2017-11-30T15:17:06+01:00
Download f4d7e7a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 14 2017-11-30T18:01 CET (sv-comp)
Download 8418218 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Automizer 12 2017-12-02T15:25Z

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

Trying to find witnesses for program (04a668b517adc36b6ba64cb8bfea3a7d3c6080e86848215b01673710ab94b024, sv-benchmarks/c/forester-heap/sll-01_false-unreach-call_false-valid-deref.i).

Found 0 witnesses for program sv-benchmarks/c/forester-heap/sll-01_false-unreach-call_false-valid-deref.i, 04a668b517adc36b6ba64cb8bfea3a7d3c6080e86848215b01673710ab94b024
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/04a668b517adc36b6ba64cb8bfea3a7d3c6080e86848215b01673710ab94b024.json

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