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/loop-lit/gj2007_true-unreach-call_true-termination.c.i
programSHA dbbe0b55d632b437834bb306bd4f2e46c51f53e534d349936210ad96dace403f
witnessName results-verified/uautomizer.2017-12-02_0106.logfiles/sv-comp18.gj2007_true-unreach-call_true-termination.c.i.files/witness.graphml
witnessSHA 0167d77536c80d715417e92ee25c296e407f977c67732042689471c6159f2d97

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2017-12-02T19:39Z
producer Automizer
program-sha256 dbbe0b55d632b437834bb306bd4f2e46c51f53e534d349936210ad96dace403f
programfile /tmp/vcloud-vcloud-master/worker/working_dir_8f490bf7-0182-423f-aac1-07584a623c27/sv-benchmarks/c/loop-lit/gj2007_true-unreach-call_true-termination.c.i
programhash 1a9963030a13e3c679db84f21688cc66372a5ac3
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/0167d77536c80d715417e92ee25c296e407f977c67732042689471c6159f2d97.graphml
witness-sha256 0167d77536c80d715417e92ee25c296e407f977c67732042689471c6159f2d97
witness-size 10157
witness-type correctness_witness

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

Trying to find witnesses for program (dbbe0b55d632b437834bb306bd4f2e46c51f53e534d349936210ad96dace403f, sv-benchmarks/c/loop-lit/gj2007_true-unreach-call_true-termination.c.i).

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

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

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

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

Found 20 witnesses for program sv-benchmarks/c/loop-lit/gj2007_true-unreach-call_true-termination.c.i, dbbe0b55d632b437834bb306bd4f2e46c51f53e534d349936210ad96dace403f
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/dbbe0b55d632b437834bb306bd4f2e46c51f53e534d349936210ad96dace403f.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 771e241 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2019-12-03T21:44 CET (comp)
Download 1cff02f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness GACAL 6 2019-12-07T23:03 CET (comp)
Download 0690963 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-11T20:28:11+01:00 Download c306425
Download 9510c61 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-11T20:18:13+01:00 Download 95d1b91
Download fb14f20 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-11T20:12:48+01:00 Download 045de23
Download 8dc7f62 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-11T20:02:32+01:00 Download 837a58e
Download 793d02a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-08T00:36:37+01:00 Download d92c823
Download 95f5691 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-07T23:43:44+01:00 Download 1cff02f
Download 5398e70 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-07T23:40:10+01:00 Download 5300814
Download 28789ec Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-07T19:39:38+01:00 Download 393d4da
Download bece94a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-06T02:12:33+01:00 Download c7f9103
Download 94500df Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-05T19:13:31+01:00 Download 4ef3631
Download 82982d5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-05T19:02:52+01:00 Download 3483956
Download 73009fd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-04T02:07:36+01:00 Download 771e241
Download 3b993b7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-11-30T19:38:28+01:00 Download 63bd2ad
Download 8998d89 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-11-30T16:34:17+01:00 Download 01b7554
Download 01b7554 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / svcomp20 7 2019-11-30T01:36:02+01:00
Download d92c823 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8 7 2019-12-07T13:37:51+01:00
Download 045de23 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 7 2019-12-01T06:25:30+01:00
Download 8b86f2e Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2019-12-03T23:46 CET (comp)

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

Trying to find witnesses for program (dbbe0b55d632b437834bb306bd4f2e46c51f53e534d349936210ad96dace403f, sv-benchmarks/c/loop-lit/gj2007_true-unreach-call_true-termination.c.i).

Found 24 witnesses for program sv-benchmarks/c/loop-lit/gj2007_true-unreach-call_true-termination.c.i, dbbe0b55d632b437834bb306bd4f2e46c51f53e534d349936210ad96dace403f
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/dbbe0b55d632b437834bb306bd4f2e46c51f53e534d349936210ad96dace403f.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download bdd72c3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2018-12-08T09:30 CET (sv-comp)
Download a3eb5ad Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2018-12-07T07:18 CET (sv-comp)
Download 5fffa8a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7 7 2018-12-10T17:50:31+01:00
Download c5cddca Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 8 2018-12-08T00:36:13+01:00
Download c7c4190 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-10T20:25:01+01:00 Download 5fffa8a
Download 8de7f18 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-10T10:32:15+01:00 Download e0355c2
Download e7b2934 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-09T21:07:29+01:00 Download e6c0772
Download 037ea42 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 11 2018-12-09T20:35:11+01:00 Download 1ddef75
Download 22ef04f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 11 2018-12-09T20:03:27+01:00 Download 70400a9
Download 13b2c95 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 15 2018-12-09T19:53:19+01:00 Download 8b7c379
Download cd87da9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-08T23:10:06+01:00 Download bdd72c3
Download cc54a48 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 8 2018-12-08T06:10:03+01:00 Download c5cddca
Download 46dcd7c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-08T03:54:28+01:00 Download 064bbee
Download 7618739 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-08T01:48:14+01:00 Download e0355c2
Download 0f08d28 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-07T17:43:54+01:00 Download d56f1ee
Download c1dc6e3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-07T16:39:52+01:00 Download a3eb5ad
Download dcd7202 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-06T09:29:39+01:00 Download 8cce0bc
Download c434c78 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 8 2018-12-06T08:56:07+01:00 Download 869542c
Download ed99074 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-06T08:17:02+01:00 Download 32d0409
Download 3330031 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-06T07:58:57+01:00 Download c6be20d
Download 6b656c9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-06T07:45:22+01:00 Download 492d674
Download 869542c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 8 2018-12-05T17:37:23+01:00
Download 9f35186 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T08:12 CET (sv-comp)
Download e22826f Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-07T05:16 CET (sv-comp)

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

Trying to find witnesses for program (dbbe0b55d632b437834bb306bd4f2e46c51f53e534d349936210ad96dace403f, sv-benchmarks/c/loop-lit/gj2007_true-unreach-call_true-termination.c.i).

Found 36 witnesses for program sv-benchmarks/c/loop-lit/gj2007_true-unreach-call_true-termination.c.i, dbbe0b55d632b437834bb306bd4f2e46c51f53e534d349936210ad96dace403f
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/dbbe0b55d632b437834bb306bd4f2e46c51f53e534d349936210ad96dace403f.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download d56f1ee Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness skink 3 2017-12-01T23:07 CET (sv-comp)
Download ac77d58 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Taipan 10 2017-12-02T17:40Z
Download b25c036 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2017-12-02T00:10 CET (sv-comp)
Download 2440655 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Map2Check 4 2017-12-01T19:49 CET (sv-comp)
Download 8afaca4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Kojak 15 2017-12-02T23:10Z
Download f8e8649 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T21:29:39.772236
Download 56993bf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T15:44:42.584832
Download 63615e6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 kind 3 2017-12-01T13:52:17.248028
Download c6baf0c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 incr 3 2017-12-01T09:25:44.002510
Download ae0b89d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 20 2017-12-01T20:05 CET (sv-comp)
Download 50fa915 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 20 2017-11-30T20:42 CET (sv-comp)
Download faa4c88 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 14 2017-12-02T23:41:34+01:00
Download c531452 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 11 2017-12-03T06:50:44+01:00 bf5fb73
Download 9e749f5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 14 2017-12-03T04:20:44+01:00 e23b8a5
Download 1b13175 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 33 2017-12-03T02:52:23+01:00 ee053f8
Download 534efb1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 11 2017-12-03T00:04:42+01:00 f9dd24c
Download 449ee5d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-02T20:47:49+01:00 b08f95b
Download 5ef32df Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-02T15:33:44+01:00 552f6a7
Download 23b9df4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-02T07:04:00+01:00 41c78bb
Download 3b69b9a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-02T00:16:41+01:00 0e0c679
Download 40cb7ba Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-01T22:34:25+01:00 6347838
Download c16b343 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-01T22:17:50+01:00 72029f9
Download 7919eb3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-01T08:14:01+01:00 9f9dfc9
Download 4834195 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-01T06:18:47+01:00 9a2dd8d
Download 1a9d3aa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-01T05:45:52+01:00 3bdc479
Download 01da68a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 7 2017-12-01T04:54:52+01:00 fa145ab
Download b213e6b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-01T04:26:17+01:00 3234831
Download 7cfcbe2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 7 2017-11-30T15:09:00+01:00
Download ff6fefb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26758M 10 2017-11-30T12:06:46+01:00
Download 0718359 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26725 6 2017-11-30T17:31:32+01:00
Download f5e53ff Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker (unknown version) 5 2017-12-02T06:09:17+01:00
Download c783894 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CBMC 50 2017-11-30T21:27 CET (sv-comp)
Download 0167d77 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Automizer 10 2017-12-02T19:39Z
Download 86be14b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness 2LS 208 2017-12-01T01:44 CET (sv-comp)
Download 82e650c Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 50 2017-12-01T13:32 CET (sv-comp)
Download a793aa0 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 9 2017-12-01T16:44 CET (sv-comp)

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

Trying to find witnesses for program (dbbe0b55d632b437834bb306bd4f2e46c51f53e534d349936210ad96dace403f, sv-benchmarks/c/loop-lit/gj2007_true-unreach-call_true-termination.c.i).

Found 0 witnesses for program sv-benchmarks/c/loop-lit/gj2007_true-unreach-call_true-termination.c.i, dbbe0b55d632b437834bb306bd4f2e46c51f53e534d349936210ad96dace403f
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/dbbe0b55d632b437834bb306bd4f2e46c51f53e534d349936210ad96dace403f.json

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