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/sum04_true-unreach-call_true-termination.i
programSHA be967b8ab35436c417d75c2d9436cdcab289aa61d3353672ce70a99e3da19b06
witnessName results-validated/cpa-seq-validate-correctness-witnesses-esbmc-kind.2018-12-08_0216.logfiles/sv-comp19_prop-reachsafety.sum04_true-unreach-call_true-termination.i.files/witness.graphml
witnessSHA 601d192403ce7cd9fa9ad7d22259de352f5bcc54a3631494804fc788baa90775

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-08T02:47:47+01:00
inputwitnesshash f997798edd4a77a87a12f88d09008c428790e712d3c6e68947c6f49b07c54efe
producer CPAchecker 1.7-svn 29852
program-sha256 be967b8ab35436c417d75c2d9436cdcab289aa61d3353672ce70a99e3da19b06
programfile ../../sv-benchmarks/c/loops/sum04_true-unreach-call_true-termination.i
programhash be967b8ab35436c417d75c2d9436cdcab289aa61d3353672ce70a99e3da19b06
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/601d192403ce7cd9fa9ad7d22259de352f5bcc54a3631494804fc788baa90775.graphml
witness-sha256 601d192403ce7cd9fa9ad7d22259de352f5bcc54a3631494804fc788baa90775
witness-size 5981
witness-type correctness_witness

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

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

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

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

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

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 228c706 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2019-12-04T01:00 CET (comp)
Download 37098f5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness GACAL 5 2019-12-07T23:16 CET (comp)
Download 8c836c9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-11T20:28:12+01:00 Download 976161f
Download 71b4ff6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-11T20:27:30+01:00 Download 49ee80b
Download f8d0487 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-11T20:08:37+01:00 Download a83b446
Download 3c2c311 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-11T20:02:16+01:00 Download a465e97
Download d1ad615 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-08T00:37:16+01:00 Download 42d5976
Download 442ee70 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-07T23:47:04+01:00 Download 37098f5
Download df3323b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-07T23:41:32+01:00 Download c1e1dd3
Download 81a5648 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-07T19:47:04+01:00 Download 6c97a9e
Download e1ac479 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-06T01:54:14+01:00 Download 57a6aa0
Download 9b8c9b8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-05T19:12:58+01:00 Download 1a2ff97
Download 4035dc5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-05T19:02:50+01:00 Download b238ba6
Download 5e86ee8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-04T02:07:28+01:00 Download 228c706
Download 85ffc2d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-11-30T19:11:58+01:00 Download b9499ad
Download aa647c8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-11-30T16:32:11+01:00 Download cb7f825
Download cb7f825 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / svcomp20 6 2019-11-29T21:52:39+01:00
Download 42d5976 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8 7 2019-12-07T15:06:24+01:00
Download a83b446 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 6 2019-12-01T07:18:13+01:00
Download e2bad38 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2019-12-04T00:32 CET (comp)

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

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

Found 25 witnesses for program sv-benchmarks/c/loops/sum04_true-unreach-call_true-termination.i, be967b8ab35436c417d75c2d9436cdcab289aa61d3353672ce70a99e3da19b06
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/be967b8ab35436c417d75c2d9436cdcab289aa61d3353672ce70a99e3da19b06.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 7a666e3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2018-12-08T08:44 CET (sv-comp)
Download 350d506 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-08T06:31:15
Download 2ee22bc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2018-12-07T01:09 CET (sv-comp)
Download 21a5615 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 6 2018-12-08T03:36:18+01:00
Download 405ea8e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-10T19:56:52+01:00 Download e2ecdc0
Download 6996ea0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-10T10:31:34+01:00 Download 7e1d5c0
Download cd0d42b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-09T21:06:40+01:00 Download 8c14c47
Download 1003385 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-09T20:26:31+01:00 Download 0587cd1
Download 3cf6d21 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-09T20:05:34+01:00 Download 868e6ed
Download 621a27c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-09T19:47:10+01:00 Download a22fdab
Download d717893 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-08T23:08:38+01:00 Download 7a666e3
Download b055496 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-08T21:47:34+01:00 Download 350d506
Download 8116776 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-08T05:24:51+01:00 Download 21a5615
Download 601d192 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-08T02:47:47+01:00 Download f997798
Download 9bd5172 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-08T01:52:23+01:00 Download 7e1d5c0
Download fb8a5bc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-07T17:44:19+01:00 Download 7d6c728
Download e21af29 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-07T16:37:34+01:00 Download 2ee22bc
Download 0f0382a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-06T09:28:30+01:00 Download c0ddd47
Download c0983a9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-06T08:45:24+01:00 Download 0b5df88
Download f8ab1e4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-06T08:28:33+01:00 Download 5e42b04
Download b9f245a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-06T08:23:21+01:00 Download a31be94
Download 9e75427 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-06T07:11:00+01:00 Download e589d18
Download 0b5df88 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-06T05:47:25+01:00
Download 972b680 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T17:23 CET (sv-comp)
Download 8485e51 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-06T23:46 CET (sv-comp)

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

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

Found 37 witnesses for program sv-benchmarks/c/loops/sum04_true-unreach-call_true-termination.i, be967b8ab35436c417d75c2d9436cdcab289aa61d3353672ce70a99e3da19b06
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/be967b8ab35436c417d75c2d9436cdcab289aa61d3353672ce70a99e3da19b06.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 7d6c728 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness skink 3 2017-12-01T22:53 CET (sv-comp)
Download 1067c5b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Taipan 6 2017-12-02T18:30Z
Download 81722f7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2017-12-02T01:57 CET (sv-comp)
Download 36f4974 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Map2Check 3 2017-12-01T19:48 CET (sv-comp)
Download 64422ab Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Kojak 6 2017-12-02T02:47Z
Download 9b73e3f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T19:41:13.961881
Download 0ee99f6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T15:13:57.232267
Download 467ce9c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 kind 3 2017-12-01T20:47:16.053341
Download 949f363 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 incr 3 2017-12-01T07:49:53.661379
Download dc78195 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 5 2017-12-01T19:10 CET (sv-comp)
Download 9216370 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 7 2017-12-03T03:27:07+01:00
Download 8b43d55 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 4 2017-12-01T06:00:39+01:00
Download 36d65c9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 7 2017-12-03T06:51:44+01:00 66ae9fb
Download b1b0c3b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-03T04:10:31+01:00 d02f5c6
Download aa9cf37 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 8 2017-12-03T01:26:27+01:00 29dd9d8
Download 07d8730 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 7 2017-12-02T23:23:28+01:00 82bf113
Download 3e18195 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-02T20:23:26+01:00 183728c
Download 9284329 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-02T15:01:24+01:00 0e83a14
Download 1ff2470 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-02T07:08:24+01:00 d111bab
Download 3b02a13 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-02T00:08:45+01:00 f68591a
Download c284c5f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-01T22:34:24+01:00 f0fd1ec
Download 395ccbc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-01T22:19:40+01:00 67e7724
Download 7ce6caf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-01T08:13:29+01:00 0caafe1
Download 8240f8c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-01T06:56:17+01:00 15837ac
Download 1012632 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-01T06:46:11+01:00 3058ea1
Download 641c117 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-01T06:16:49+01:00 d22b863
Download 1c20df2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-01T05:04:12+01:00 5632569
Download 070a111 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-01T05:00:39+01:00 d9a79ce
Download 98a3341 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-11-30T17:30:45+01:00
Download b9e1f4d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26758M 10 2017-11-30T14:19:51+01:00
Download e47519f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26725 6 2017-11-30T20:42:56+01:00
Download a32e8a2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker (unknown version) 5 2017-12-02T08:52:54+01:00
Download af53cfd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CBMC 9 2017-11-30T15:43 CET (sv-comp)
Download cb9d7b0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Automizer 6 2017-12-02T08:56Z
Download 17729a0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness 2LS 17 2017-11-30T13:51 CET (sv-comp)
Download 14d7e43 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 9 2017-12-01T14:54 CET (sv-comp)
Download 320af88 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 8 2017-12-01T12:43 CET (sv-comp)

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

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

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

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