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/loops/sum03_false-unreach-call_true-termination.i
programSHA 2a3547b16f75be3d225cb90d16687f3917cbb2360e0681ebeeb6cce258fb5cb0
witnessName results-verified/skink.2017-12-01_2203.logfiles/sv-comp18.sum03_false-unreach-call_true-termination.i.files/witness.graphml
witnessSHA 31a0462b74fe71db2915094d7e4bdefd71245d2b8272fe13b2f19058655f8f63

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2017-12-01T22:40 CET (sv-comp)
memorymodel simple
producer skink
program-sha256 2a3547b16f75be3d225cb90d16687f3917cbb2360e0681ebeeb6cce258fb5cb0
programfile ../../sv-benchmarks/c/loops/sum03_false-unreach-call_true-termination.i
programhash a5bec83c84f47b7653d49cdbe6bc7857a2bc0080
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/31a0462b74fe71db2915094d7e4bdefd71245d2b8272fe13b2f19058655f8f63.graphml
witness-sha256 31a0462b74fe71db2915094d7e4bdefd71245d2b8272fe13b2f19058655f8f63
witness-size 5695
witness-type violation_witness

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

Trying to find witnesses for program (2a3547b16f75be3d225cb90d16687f3917cbb2360e0681ebeeb6cce258fb5cb0, sv-benchmarks/c/loops/sum03_false-unreach-call_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/loops/sum03_false-unreach-call_true-termination.i, 2a3547b16f75be3d225cb90d16687f3917cbb2360e0681ebeeb6cce258fb5cb0
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/2a3547b16f75be3d225cb90d16687f3917cbb2360e0681ebeeb6cce258fb5cb0.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 (2a3547b16f75be3d225cb90d16687f3917cbb2360e0681ebeeb6cce258fb5cb0, sv-benchmarks/c/loops/sum03_false-unreach-call_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/loops/sum03_false-unreach-call_true-termination.i, 2a3547b16f75be3d225cb90d16687f3917cbb2360e0681ebeeb6cce258fb5cb0
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/2a3547b16f75be3d225cb90d16687f3917cbb2360e0681ebeeb6cce258fb5cb0.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 (2a3547b16f75be3d225cb90d16687f3917cbb2360e0681ebeeb6cce258fb5cb0, sv-benchmarks/c/loops/sum03_false-unreach-call_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/loops/sum03_false-unreach-call_true-termination.i, 2a3547b16f75be3d225cb90d16687f3917cbb2360e0681ebeeb6cce258fb5cb0
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/2a3547b16f75be3d225cb90d16687f3917cbb2360e0681ebeeb6cce258fb5cb0.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 (2a3547b16f75be3d225cb90d16687f3917cbb2360e0681ebeeb6cce258fb5cb0, sv-benchmarks/c/loops/sum03_false-unreach-call_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/loops/sum03_false-unreach-call_true-termination.i, 2a3547b16f75be3d225cb90d16687f3917cbb2360e0681ebeeb6cce258fb5cb0
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/2a3547b16f75be3d225cb90d16687f3917cbb2360e0681ebeeb6cce258fb5cb0.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 (2a3547b16f75be3d225cb90d16687f3917cbb2360e0681ebeeb6cce258fb5cb0, sv-benchmarks/c/loops/sum03_false-unreach-call_true-termination.i).

Found 20 witnesses for program sv-benchmarks/c/loops/sum03_false-unreach-call_true-termination.i, 2a3547b16f75be3d225cb90d16687f3917cbb2360e0681ebeeb6cce258fb5cb0
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/2a3547b16f75be3d225cb90d16687f3917cbb2360e0681ebeeb6cce258fb5cb0.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 68e9b8e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2019-12-01 13:26:07
Download 84f8fcd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 18 2019-12-04T00:19 CET (comp)
Download a175e4e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness GACAL 25 2019-12-07T23:20 CET (comp)
Download 19c449e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 39 2019-12-11T21:55:09+01:00 Download f7d70fa
Download 81ed9bd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 39 2019-12-11T21:09:20+01:00 Download 68e9b8e
Download e129ecb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 39 2019-12-11T20:55:22+01:00 Download 3385778
Download 208c7c6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 39 2019-12-11T20:44:29+01:00 Download 55afb67
Download 818d693 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 39 2019-12-08T01:51:58+01:00 Download 089fccc
Download 073dd36 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 39 2019-12-08T00:26:17+01:00 Download ec57e86
Download 16d6cbf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 39 2019-12-04T02:58:18+01:00 Download 84f8fcd
Download 39bff85 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 39 2019-12-03T08:56:47+01:00 Download 34af031
Download d57287e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 39 2019-12-03T08:09:45+01:00 Download 4801456
Download 4801456 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 38 2019-11-30T00:38:44+01:00
Download 089fccc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8 39 2019-12-07T13:26:54+01:00
Download f7d70fa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 38 2019-12-01T15:51:54+01:00
Download dd6ffa4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-08T00:14:01+01:00 Download a175e4e
Download df8a879 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-06T02:41:07+01:00 Download 7635cb4
Download 6be96cf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-05T20:20:58+01:00 Download 9f2fdda
Download 408d310 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-05T19:34:01+01:00 Download ffb2aa6
Download d2b28a4 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2019-12-03T22:42 CET (comp)

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

Trying to find witnesses for program (2a3547b16f75be3d225cb90d16687f3917cbb2360e0681ebeeb6cce258fb5cb0, sv-benchmarks/c/loops/sum03_false-unreach-call_true-termination.i).

Found 27 witnesses for program sv-benchmarks/c/loops/sum03_false-unreach-call_true-termination.i, 2a3547b16f75be3d225cb90d16687f3917cbb2360e0681ebeeb6cce258fb5cb0
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/2a3547b16f75be3d225cb90d16687f3917cbb2360e0681ebeeb6cce258fb5cb0.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download f351483 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 2 2018-12-08T07:38 CET (sv-comp)
Download 7431f19 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 9 2018-12-08T02:52:12
Download e6606c4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 21 2018-12-07T03:57 CET (sv-comp)
Download 97923ff Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7 37 2018-12-10T17:09:30+01:00
Download a3411fa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 38 2018-12-07T18:17:33+01:00
Download e98aff9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 39 2018-12-10T20:36:20+01:00 Download 97923ff
Download 4177b00 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 39 2018-12-10T10:48:40+01:00 Download 0300aa1
Download 9d1f667 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 39 2018-12-09T20:53:24+01:00 Download 5b27843
Download 397f254 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 39 2018-12-09T20:37:03+01:00 Download 03177d4
Download 1a5d2bd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 39 2018-12-09T20:26:50+01:00 Download 054e841
Download 33f4fef Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 39 2018-12-09T18:20:25+01:00 Download d90656a
Download eabc164 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 39 2018-12-08T23:43:47+01:00 Download f351483
Download 5aef862 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 39 2018-12-08T22:11:17+01:00 Download 7431f19
Download 4d03b08 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 39 2018-12-08T07:51:04+01:00 Download a3411fa
Download ba8ba2c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 39 2018-12-08T05:04:42+01:00 Download f9db73d
Download 5afcb8e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 39 2018-12-08T03:38:40+01:00 Download 0300aa1
Download 9f0066f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 39 2018-12-07T18:12:29+01:00 Download 39f2e79
Download c3fcdb1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 39 2018-12-07T17:45:27+01:00 Download e6606c4
Download b0aa6b1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 39 2018-12-06T10:18:45+01:00 Download bc6b27b
Download 15cdd3f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 39 2018-12-06T09:48:26+01:00 Download 71410e6
Download 44f6532 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 39 2018-12-06T09:15:43+01:00 Download f611c89
Download 71410e6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 38 2018-12-05T13:52:05+01:00
Download 731c857 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-07T01:08:58+01:00 Download 266b1a0
Download 738e2a9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-06T09:40:58+01:00 Download 084241e
Download b244324 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-06T09:18:23+01:00 Download cbae9d0
Download 018a082 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T07:00 CET (sv-comp)
Download 5dc5ac0 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-07T03:18 CET (sv-comp)

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

Trying to find witnesses for program (2a3547b16f75be3d225cb90d16687f3917cbb2360e0681ebeeb6cce258fb5cb0, sv-benchmarks/c/loops/sum03_false-unreach-call_true-termination.i).

Found 20 witnesses for program sv-benchmarks/c/loops/sum03_false-unreach-call_true-termination.i, 2a3547b16f75be3d225cb90d16687f3917cbb2360e0681ebeeb6cce258fb5cb0
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/2a3547b16f75be3d225cb90d16687f3917cbb2360e0681ebeeb6cce258fb5cb0.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 31a0462 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness skink 6 2017-12-01T22:40 CET (sv-comp)
Download 804399b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Taipan 33 2017-12-03T05:07Z
Download b65f8a6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2017-12-02T10:36 CET (sv-comp)
Download cd0bfe7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Map2Check 3 2017-12-01T20:15 CET (sv-comp)
Download a0ef6b3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Kojak 33 2017-12-02T09:56Z
Download 846853e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 4 2017-12-01T13:48:49.300259
Download eee6972 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 4 2017-12-01T18:15:36.750606
Download e886d26 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 11 2017-12-01T19:46 CET (sv-comp)
Download 9c1e0bc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 11 2017-11-30T16:06 CET (sv-comp)
Download a6c276c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 35 2017-12-02T18:41:16+01:00
Download f65ad9a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 36 2017-12-01T02:05:42+01:00
Download f14025e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 39 2017-11-30T14:36:03+01:00
Download d712fc6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 28 2017-12-01T01:28:30+01:00
Download ff0f576 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 27 2017-12-02T12:36:47+01:00
Download b6d93f2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 18 2017-11-30T16:05 CET (sv-comp)
Download e5c75b2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Automizer 33 2017-12-02T03:10Z
Download b788374 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness 2LS 21 2017-11-30T20:54 CET (sv-comp)
Download a495352 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T23:16:37.880094
Download f526582 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T14:52:37.254919
Download b737687 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 18 2017-12-01T18:14 CET (sv-comp)

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

Trying to find witnesses for program (2a3547b16f75be3d225cb90d16687f3917cbb2360e0681ebeeb6cce258fb5cb0, sv-benchmarks/c/loops/sum03_false-unreach-call_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/loops/sum03_false-unreach-call_true-termination.i, 2a3547b16f75be3d225cb90d16687f3917cbb2360e0681ebeeb6cce258fb5cb0
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/2a3547b16f75be3d225cb90d16687f3917cbb2360e0681ebeeb6cce258fb5cb0.json

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