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/Problem02_label31_true-unreach-call_false-termination.c
programSHA 82d071ed562a4931dd331fdab42097ca8ff91243f94756a79921e70d05c70f0d
witnessName results-verified/depthk.2018-12-05_0936.logfiles/sv-comp19_prop-termination.Problem02_label31_true-unreach-call_false-termination.c.files/witness.graphml
witnessSHA c088a455420a7099619d7c06101dabb406342dc75acbc4ab7501b3eab7f2f2b7

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-05T22:08:22.385520
producer DepthK v3.0
programfile /tmp/vcloud-vcloud-master/worker/working_dir_6ac63f7a-84af-4468-bc55-8d4a9a051e76/sv-benchmarks/c/eca-rers2012/Problem02_label31_true-unreach-call_false-termination.c
programhash ec451dfa87bae03634c3df96f95bbd4db2c274c1
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/c088a455420a7099619d7c06101dabb406342dc75acbc4ab7501b3eab7f2f2b7.graphml
witness-sha256 c088a455420a7099619d7c06101dabb406342dc75acbc4ab7501b3eab7f2f2b7
witness-size 3493
witness-type correctness_witness

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

Trying to find witnesses for program (82d071ed562a4931dd331fdab42097ca8ff91243f94756a79921e70d05c70f0d, sv-benchmarks/c/eca-rers2012/Problem02_label31_true-unreach-call_false-termination.c).

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

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

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

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

Found 12 witnesses for program sv-benchmarks/c/eca-rers2012/Problem02_label31_true-unreach-call_false-termination.c, 82d071ed562a4931dd331fdab42097ca8ff91243f94756a79921e70d05c70f0d
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/82d071ed562a4931dd331fdab42097ca8ff91243f94756a79921e70d05c70f0d.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 300d720 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 280 2019-12-11T20:17:24+01:00 Download fedd5cc
Download 8ece05b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 280 2019-12-11T20:02:19+01:00 Download c8b333f
Download f1633a6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 280 2019-12-08T00:37:16+01:00 Download 5a729af
Download 6d5dc8b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 280 2019-12-07T23:34:28+01:00 Download e41dde8
Download a5b6699 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 280 2019-12-07T19:42:37+01:00 Download ee381db
Download e099c28 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 280 2019-12-05T19:02:55+01:00 Download 23c04be
Download c433aea Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 280 2019-11-30T16:11:41+01:00 Download 3c39c21
Download 3c39c21 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / svcomp20 280 2019-11-29T22:37:53+01:00
Download fedd5cc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 280 2019-11-30T21:14:55+01:00
Download e6970ea Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Symbiotic 2 2019-12-01 05:07:11
Download 2a27dd7 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.9 359 2019-11-29T16:33:56+01:00
Download ed78630 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ 359 2019-12-01T17:04:04+01:00

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

Trying to find witnesses for program (82d071ed562a4931dd331fdab42097ca8ff91243f94756a79921e70d05c70f0d, sv-benchmarks/c/eca-rers2012/Problem02_label31_true-unreach-call_false-termination.c).

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 9cfbfb8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-08T02:34:16
Download 4f236ed Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 280 2018-12-07T09:18:24+01:00
Download 6d9bd92 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 280 2018-12-10T20:08:59+01:00 Download 34052a3
Download e958932 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 280 2018-12-09T20:25:51+01:00 Download 33ca2d1
Download d6b1311 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 280 2018-12-09T20:08:32+01:00 Download bd8b212
Download 8028539 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 280 2018-12-08T21:41:51+01:00 Download 9cfbfb8
Download 9a7edd4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 280 2018-12-08T05:53:56+01:00 Download 4f236ed
Download 2914361 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 280 2018-12-08T02:19:57+01:00 Download a713fb2
Download 9da1aac Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 280 2018-12-06T09:28:43+01:00 Download d4b17ec
Download 61a128f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 280 2018-12-06T09:11:46+01:00 Download 5a34fd6
Download 14aafb0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 280 2018-12-06T07:44:47+01:00 Download 4fe1d4a
Download 5a34fd6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 280 2018-12-06T07:31:58+01:00
Download 3026be4 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 359 2018-12-07T17:02:01+01:00
Download d225a64 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn 29852 356 2018-12-08T08:30:25+01:00
Download 8a9cba5 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn 29852 356 2018-12-06T09:48:36+01:00
Download 2af1577 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn 29852 359 2018-12-05T18:29:35+01:00

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

Trying to find witnesses for program (82d071ed562a4931dd331fdab42097ca8ff91243f94756a79921e70d05c70f0d, sv-benchmarks/c/eca-rers2012/Problem02_label31_true-unreach-call_false-termination.c).

Found 21 witnesses for program sv-benchmarks/c/eca-rers2012/Problem02_label31_true-unreach-call_false-termination.c, 82d071ed562a4931dd331fdab42097ca8ff91243f94756a79921e70d05c70f0d
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/82d071ed562a4931dd331fdab42097ca8ff91243f94756a79921e70d05c70f0d.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 7e5e831 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Taipan 161 2017-12-03T04:56Z
Download d218359 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Kojak 178 2017-12-02T08:49Z
Download 89bb01e 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 3aba72d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 280 2017-12-03T06:56:58+01:00 586b8f5
Download bddb8d8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 280 2017-12-03T04:27:34+01:00 f7872af
Download 9c7984d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 280 2017-12-03T01:57:23+01:00 6e5d640
Download d6f620c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 285 2017-12-03T01:17:43+01:00 dd56307
Download df5956c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 280 2017-12-02T15:20:47+01:00 c3ef81c
Download df2e2e9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 280 2017-12-01T06:26:37+01:00 5f68172
Download 578dcf3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 280 2017-12-01T06:16:45+01:00 c409603
Download 3b26965 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 280 2017-12-01T05:02:56+01:00 95c7e35
Download 74e48fe Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 280 2017-12-01T04:43:35+01:00 84d5626
Download 28db1ee Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 280 2017-12-01T01:34:12+01:00
Download 2d754b8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26758M 319 2017-11-30T16:43:52+01:00
Download 86fdf7c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26725 280 2017-11-30T13:49:59+01:00
Download 290fb99 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker (unknown version) 430 2017-12-02T03:22:44+01:00
Download a7b01a8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Automizer 161 2017-12-02T17:35Z
Download f445997 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness 2LS 811 2017-12-01T03:26 CET (sv-comp)
Download eeefd12 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.6.1-svn 26773 334 2017-12-01T16:20:50+01:00
Download 998efba Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Automizer 15 2017-12-03T11:16Z
Download 0ba4d2d Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness 2LS 26 2017-12-01T14:30 CET (sv-comp)

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

Trying to find witnesses for program (82d071ed562a4931dd331fdab42097ca8ff91243f94756a79921e70d05c70f0d, sv-benchmarks/c/eca-rers2012/Problem02_label31_true-unreach-call_false-termination.c).

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

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