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/eca-rers2012/Problem01_label17_true-unreach-call_false-termination.c
programSHA 465a7f8dda979fa7820b326ac722e7cb49f8fbd41255cbae2ee6124d7eefcc1d
witnessName results-verified/depthk.2018-12-05_0936.logfiles/sv-comp19_prop-termination.Problem01_label17_true-unreach-call_false-termination.c.files/witness.graphml
witnessSHA ae2d028ebd183c16de303b422a8c295dd78a26f6332715ef5e57f982e9a0664d

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-05T14:55:05.072679
producer DepthK v3.0
programfile /tmp/vcloud-vcloud-master/worker/working_dir_c50bac6b-2c72-4d20-92a6-d45710f450bb/sv-benchmarks/c/eca-rers2012/Problem01_label17_true-unreach-call_false-termination.c
programhash aac67f6dc6529e5dab098a5e1960c3e19b78df96
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/ae2d028ebd183c16de303b422a8c295dd78a26f6332715ef5e57f982e9a0664d.graphml
witness-sha256 ae2d028ebd183c16de303b422a8c295dd78a26f6332715ef5e57f982e9a0664d
witness-size 3493
witness-type correctness_witness

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

Trying to find witnesses for program (465a7f8dda979fa7820b326ac722e7cb49f8fbd41255cbae2ee6124d7eefcc1d, sv-benchmarks/c/eca-rers2012/Problem01_label17_true-unreach-call_false-termination.c).

Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem01_label17_true-unreach-call_false-termination.c, 465a7f8dda979fa7820b326ac722e7cb49f8fbd41255cbae2ee6124d7eefcc1d
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/465a7f8dda979fa7820b326ac722e7cb49f8fbd41255cbae2ee6124d7eefcc1d.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 (465a7f8dda979fa7820b326ac722e7cb49f8fbd41255cbae2ee6124d7eefcc1d, sv-benchmarks/c/eca-rers2012/Problem01_label17_true-unreach-call_false-termination.c).

Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem01_label17_true-unreach-call_false-termination.c, 465a7f8dda979fa7820b326ac722e7cb49f8fbd41255cbae2ee6124d7eefcc1d
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/465a7f8dda979fa7820b326ac722e7cb49f8fbd41255cbae2ee6124d7eefcc1d.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 (465a7f8dda979fa7820b326ac722e7cb49f8fbd41255cbae2ee6124d7eefcc1d, sv-benchmarks/c/eca-rers2012/Problem01_label17_true-unreach-call_false-termination.c).

Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem01_label17_true-unreach-call_false-termination.c, 465a7f8dda979fa7820b326ac722e7cb49f8fbd41255cbae2ee6124d7eefcc1d
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/465a7f8dda979fa7820b326ac722e7cb49f8fbd41255cbae2ee6124d7eefcc1d.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 (465a7f8dda979fa7820b326ac722e7cb49f8fbd41255cbae2ee6124d7eefcc1d, sv-benchmarks/c/eca-rers2012/Problem01_label17_true-unreach-call_false-termination.c).

Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem01_label17_true-unreach-call_false-termination.c, 465a7f8dda979fa7820b326ac722e7cb49f8fbd41255cbae2ee6124d7eefcc1d
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/465a7f8dda979fa7820b326ac722e7cb49f8fbd41255cbae2ee6124d7eefcc1d.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 (465a7f8dda979fa7820b326ac722e7cb49f8fbd41255cbae2ee6124d7eefcc1d, sv-benchmarks/c/eca-rers2012/Problem01_label17_true-unreach-call_false-termination.c).

Found 11 witnesses for program sv-benchmarks/c/eca-rers2012/Problem01_label17_true-unreach-call_false-termination.c, 465a7f8dda979fa7820b326ac722e7cb49f8fbd41255cbae2ee6124d7eefcc1d
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/465a7f8dda979fa7820b326ac722e7cb49f8fbd41255cbae2ee6124d7eefcc1d.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download e3fc1f5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 287 2019-12-11T20:14:24+01:00 Download 5c885af
Download 75ba024 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 287 2019-12-11T20:02:20+01:00 Download c3739f0
Download 4770063 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 287 2019-12-08T00:36:23+01:00 Download 54a8c92
Download d39104a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 287 2019-12-07T23:41:58+01:00 Download d8e25f6
Download f1db486 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 287 2019-12-07T19:45:34+01:00 Download 3735102
Download 8dacd96 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 287 2019-12-05T19:02:55+01:00 Download 9d2f0cc
Download 62bbd1f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 287 2019-11-30T17:24:31+01:00 Download 4f043b0
Download 4f043b0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / svcomp20 287 2019-11-29T20:06:53+01:00
Download 5c885af Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 287 2019-11-30T20:54:18+01:00
Download 468f5ca Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.9 339 2019-11-29T20:48:23+01:00
Download 807d910 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ 339 2019-12-01T00:35:01+01:00

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

Trying to find witnesses for program (465a7f8dda979fa7820b326ac722e7cb49f8fbd41255cbae2ee6124d7eefcc1d, sv-benchmarks/c/eca-rers2012/Problem01_label17_true-unreach-call_false-termination.c).

Found 16 witnesses for program sv-benchmarks/c/eca-rers2012/Problem01_label17_true-unreach-call_false-termination.c, 465a7f8dda979fa7820b326ac722e7cb49f8fbd41255cbae2ee6124d7eefcc1d
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/465a7f8dda979fa7820b326ac722e7cb49f8fbd41255cbae2ee6124d7eefcc1d.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 55d526e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-08T00:20:57
Download 709c122 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 287 2018-12-07T10:19:44+01:00
Download 0a2c834 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 287 2018-12-10T20:01:06+01:00 Download 7b4330c
Download d15c9a5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 287 2018-12-09T20:17:43+01:00 Download e83c512
Download 0bca918 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 287 2018-12-09T20:12:10+01:00 Download 23c1330
Download 9b28a2a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 287 2018-12-08T21:35:52+01:00 Download 55d526e
Download 75dd8e4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 287 2018-12-08T07:16:28+01:00 Download 709c122
Download b08ca5c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 287 2018-12-08T02:22:13+01:00 Download 1bda4d0
Download 18b314b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 287 2018-12-06T09:28:52+01:00 Download 0f3503d
Download 490cac2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 287 2018-12-06T09:01:54+01:00 Download c8c1ab0
Download 423b561 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 287 2018-12-06T07:20:19+01:00 Download 5137063
Download c8c1ab0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 287 2018-12-06T03:19:51+01:00
Download a5ab9d5 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 339 2018-12-07T01:46:37+01:00
Download ed600a8 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn 29852 336 2018-12-08T09:04:19+01:00
Download 09075ca Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn 29852 324 2018-12-06T09:49:02+01:00
Download 5b5fe3d Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn 29852 327 2018-12-05T11:51:57+01:00

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

Trying to find witnesses for program (465a7f8dda979fa7820b326ac722e7cb49f8fbd41255cbae2ee6124d7eefcc1d, sv-benchmarks/c/eca-rers2012/Problem01_label17_true-unreach-call_false-termination.c).

Found 17 witnesses for program sv-benchmarks/c/eca-rers2012/Problem01_label17_true-unreach-call_false-termination.c, 465a7f8dda979fa7820b326ac722e7cb49f8fbd41255cbae2ee6124d7eefcc1d
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/465a7f8dda979fa7820b326ac722e7cb49f8fbd41255cbae2ee6124d7eefcc1d.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 201416b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Kojak 181 2017-12-02T17:32Z
Download cc9a739 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.12-svcomp17 4 2017-11-02T13:16:17+05:30
Download 6abf0b9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 287 2017-12-03T04:18:28+01:00 782a06e
Download 1f1e662 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 293 2017-12-03T01:59:25+01:00 87500e0
Download 17bcadc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 287 2017-12-03T01:12:48+01:00 3feb195
Download b50251a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 287 2017-12-02T15:01:45+01:00 06a638c
Download 372ec53 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 287 2017-12-01T06:01:55+01:00 194d8d0
Download 99ec8d0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 287 2017-12-01T05:33:33+01:00 8d3976b
Download 0ee5bb6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 287 2017-12-01T05:18:49+01:00 62ec6e3
Download a27c8c3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 287 2017-12-01T05:07:59+01:00 cd78e51
Download c5cab8c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 287 2017-12-01T00:21:44+01:00
Download 1c901c1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26758M 489 2017-11-30T20:27:43+01:00
Download 7cf9d87 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26725 287 2017-12-01T00:55:05+01:00
Download 75a6325 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker (unknown version) 504 2017-12-01T22:42:32+01:00
Download 5df3c56 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Automizer 160 2017-12-02T14:40Z
Download d67cfb6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness 2LS 778 2017-11-30T15:58 CET (sv-comp)
Download 586fffa Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness 2LS 31 2017-12-01T12:43 CET (sv-comp)

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

Trying to find witnesses for program (465a7f8dda979fa7820b326ac722e7cb49f8fbd41255cbae2ee6124d7eefcc1d, sv-benchmarks/c/eca-rers2012/Problem01_label17_true-unreach-call_false-termination.c).

Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem01_label17_true-unreach-call_false-termination.c, 465a7f8dda979fa7820b326ac722e7cb49f8fbd41255cbae2ee6124d7eefcc1d
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/465a7f8dda979fa7820b326ac722e7cb49f8fbd41255cbae2ee6124d7eefcc1d.json

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