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-invgen/id_trans_false-unreach-call_true-termination.i
programSHA 94edc71c818c592c983fd441974a17f7c924d0961b696d3fb87eb28b263a6302
witnessName results-verified/ukojak.2018-12-08_1104.logfiles/sv-comp19_prop-reachsafety.id_trans_false-unreach-call_true-termination.i.files/witness.graphml
witnessSHA 5f2bcbe2b57fae6748725a05998b9956633e92e6086256a399d0724f3baef9af

Information about the Witness from Competition Database

from https://sv-comp.sosy-lab.org/2019/results/witnessInfoByHash/5f2bcbe2b57fae6748725a05998b9956633e92e6086256a399d0724f3baef9af.json

Key Value
architecture 32bit
creationtime 2018-12-09T16:13Z
producer Kojak
programfile /tmp/vcloud-vcloud-master/worker/working_dir_cc84c4fd-5088-4765-97be-f6fb14d453ea/sv-benchmarks/c/loop-invgen/id_trans_false-unreach-call_true-termination.i
programhash 6b853b7a72b17d5b4054a16a7ba98c728e55c23b
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/5f2bcbe2b57fae6748725a05998b9956633e92e6086256a399d0724f3baef9af.graphml
witness-sha256 5f2bcbe2b57fae6748725a05998b9956633e92e6086256a399d0724f3baef9af
witness-size 10215
witness-type violation_witness

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

Trying to find witnesses for program (94edc71c818c592c983fd441974a17f7c924d0961b696d3fb87eb28b263a6302, sv-benchmarks/c/loop-invgen/id_trans_false-unreach-call_true-termination.i).

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

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

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

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

Found 19 witnesses for program sv-benchmarks/c/loop-invgen/id_trans_false-unreach-call_true-termination.i, 94edc71c818c592c983fd441974a17f7c924d0961b696d3fb87eb28b263a6302
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/94edc71c818c592c983fd441974a17f7c924d0961b696d3fb87eb28b263a6302.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 7179fdf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2019-12-02 00:08:56
Download dc604ed Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 6 2019-12-04T01:12 CET (comp)
Download 042930a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 10 2019-12-11T21:45:05+01:00 Download 1c03b00
Download 19f6f96 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 10 2019-12-11T21:39:16+01:00 Download 0ce8f80
Download 5756c43 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 10 2019-12-11T21:09:27+01:00 Download 7179fdf
Download ea144a8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 10 2019-12-11T20:54:55+01:00 Download 7d49064
Download 52304a0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 10 2019-12-11T20:44:39+01:00 Download 20e777c
Download 97527ce Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 10 2019-12-08T01:51:17+01:00 Download 979b271
Download 5156765 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 10 2019-12-08T00:26:18+01:00 Download 81e8c41
Download a9f1cca Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 10 2019-12-07T21:13:03+01:00 Download b67fdc3
Download c722da7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 10 2019-12-04T02:58:03+01:00 Download dc604ed
Download b13255e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 10 2019-12-03T08:57:09+01:00 Download e30e383
Download 9018587 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 10 2019-12-03T08:10:27+01:00 Download cc6c455
Download cc6c455 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 10 2019-11-30T01:34:27+01:00
Download 979b271 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8 10 2019-12-07T22:10:06+01:00
Download 0ce8f80 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 10 2019-12-01T02:16:42+01:00
Download ea5282c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 8 2019-12-06T02:41:11+01:00 Download 395f585
Download d058f5e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 8 2019-12-05T20:21:25+01:00 Download d74a02e
Download d7635c2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 8 2019-12-05T19:34:02+01:00 Download b90bfa6

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

Trying to find witnesses for program (94edc71c818c592c983fd441974a17f7c924d0961b696d3fb87eb28b263a6302, sv-benchmarks/c/loop-invgen/id_trans_false-unreach-call_true-termination.i).

Found 23 witnesses for program sv-benchmarks/c/loop-invgen/id_trans_false-unreach-call_true-termination.i, 94edc71c818c592c983fd441974a17f7c924d0961b696d3fb87eb28b263a6302
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/94edc71c818c592c983fd441974a17f7c924d0961b696d3fb87eb28b263a6302.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download d674fe2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 2 2018-12-08T18:08 CET (sv-comp)
Download a62bf2b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 4 2018-12-08T10:37:08
Download ff058ce Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 7 2018-12-06T23:49 CET (sv-comp)
Download 346327c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7 10 2018-12-10T18:49:10+01:00
Download 91af1bf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 10 2018-12-07T10:21:53+01:00
Download af5d79f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 10 2018-12-10T20:36:04+01:00 Download 346327c
Download d53297a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 10 2018-12-09T20:53:21+01:00 Download 04ee6e0
Download ca91c81 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 10 2018-12-09T20:36:40+01:00 Download 5c0a7bc
Download fc2342d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 10 2018-12-09T20:33:34+01:00 Download 5f2bcbe
Download 4864d1d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 10 2018-12-09T18:21:54+01:00 Download 65988f6
Download c62d6fb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 10 2018-12-08T23:44:01+01:00 Download d674fe2
Download 07ba9eb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 10 2018-12-08T22:10:18+01:00 Download a62bf2b
Download 4243c45 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 10 2018-12-08T07:59:02+01:00 Download 91af1bf
Download 3f069c4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 10 2018-12-08T04:59:43+01:00 Download 467ca9b
Download f1cc53f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 10 2018-12-08T04:12:08+01:00 Download c6f91b9
Download b259d06 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 10 2018-12-07T18:47:11+01:00 Download 81fd304
Download dfcb6ea Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 10 2018-12-07T17:34:48+01:00 Download ff058ce
Download 8d576ba Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 10 2018-12-06T10:18:22+01:00 Download 258467b
Download 311ea8d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 10 2018-12-06T09:48:07+01:00 Download ff12e39
Download 9bf3b95 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 10 2018-12-06T09:42:09+01:00 Download c5dbae7
Download 602897e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 10 2018-12-06T09:19:07+01:00 Download 18a7054
Download ff12e39 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 10 2018-12-05T18:59:33+01:00
Download d90f49c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 8 2018-12-06T09:04:15+01:00 Download 40040f4

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

Trying to find witnesses for program (94edc71c818c592c983fd441974a17f7c924d0961b696d3fb87eb28b263a6302, sv-benchmarks/c/loop-invgen/id_trans_false-unreach-call_true-termination.i).

Found 18 witnesses for program sv-benchmarks/c/loop-invgen/id_trans_false-unreach-call_true-termination.i, 94edc71c818c592c983fd441974a17f7c924d0961b696d3fb87eb28b263a6302
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/94edc71c818c592c983fd441974a17f7c924d0961b696d3fb87eb28b263a6302.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 3cbf0de Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness skink 4 2017-12-01T23:19 CET (sv-comp)
Download ada5037 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Taipan 10 2017-12-03T02:08Z
Download 7cadc07 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2017-12-02T01:17 CET (sv-comp)
Download f5e6e74 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Map2Check 3 2017-12-01T20:54 CET (sv-comp)
Download 1405e88 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Kojak 10 2017-12-02T13:43Z
Download 6ac4138 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 4 2017-12-01T20:28:55.880117
Download 357b8c9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 4 2017-12-01T16:23:49.791302
Download aa2a77a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 5 2017-12-01T17:40 CET (sv-comp)
Download a2176a4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 5 2017-11-30T22:33 CET (sv-comp)
Download f9d1c57 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 11 2017-12-03T00:41:04+01:00
Download 319fc79 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 10 2017-11-30T21:50:46+01:00
Download 8204115 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 14 2017-12-01T02:58:43+01:00
Download 2eb7512 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 8 2017-11-30T16:19:12+01:00
Download b77d35a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 10 2017-12-01T21:58:09+01:00
Download 66e2586 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 7 2017-11-30T14:56 CET (sv-comp)
Download ee992ad Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Automizer 10 2017-12-02T07:15Z
Download cb3d65e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness 2LS 7 2017-11-30T15:02 CET (sv-comp)
Download 41c6c05 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 17 2017-12-01T13:15 CET (sv-comp)

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

Trying to find witnesses for program (94edc71c818c592c983fd441974a17f7c924d0961b696d3fb87eb28b263a6302, sv-benchmarks/c/loop-invgen/id_trans_false-unreach-call_true-termination.i).

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

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