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_label38_true-unreach-call_false-termination.c
programSHA 2d9abcf9faff65782976ff66ac41ce5573829ea9e54b54bbb8915def7a894f41
witnessName results-verified/cpa-seq.2017-12-01_1227.logfiles/sv-comp18.Problem02_label38_true-unreach-call_false-termination.c.files/witness.graphml
witnessSHA 3604ddb93274aee2ec496dcc5da6197b1728361a1904589f85ae237717b8889d

Information about the Witness from Competition Database

from https://sv-comp.sosy-lab.org/2018/results/witnessInfoByHash/3604ddb93274aee2ec496dcc5da6197b1728361a1904589f85ae237717b8889d.json

Key Value
architecture 32bit
creationtime 2017-12-01T16:04:05+01:00
producer CPAchecker 1.6.1-svn 26773
program-sha256 2d9abcf9faff65782976ff66ac41ce5573829ea9e54b54bbb8915def7a894f41
programfile ../../sv-benchmarks/c/eca-rers2012/Problem02_label38_true-unreach-call_false-termination.c
programhash 04fd81e9543232110dc189b4b001c0bb7a784bec
sourcecodelang C
specification CHECK( init(main()), LTL(F end) )
witness-file witnessFileByHash/3604ddb93274aee2ec496dcc5da6197b1728361a1904589f85ae237717b8889d.graphml
witness-sha256 3604ddb93274aee2ec496dcc5da6197b1728361a1904589f85ae237717b8889d
witness-size 334383
witness-type violation_witness

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

Trying to find witnesses for program (2d9abcf9faff65782976ff66ac41ce5573829ea9e54b54bbb8915def7a894f41, sv-benchmarks/c/eca-rers2012/Problem02_label38_true-unreach-call_false-termination.c).

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

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

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

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

Found 13 witnesses for program sv-benchmarks/c/eca-rers2012/Problem02_label38_true-unreach-call_false-termination.c, 2d9abcf9faff65782976ff66ac41ce5573829ea9e54b54bbb8915def7a894f41
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/2d9abcf9faff65782976ff66ac41ce5573829ea9e54b54bbb8915def7a894f41.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 4f40756 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 280 2019-12-11T20:21:08+01:00 Download 26213bd
Download 1d2d837 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 280 2019-12-11T20:18:05+01:00 Download 5e37a8a
Download f55fa20 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 280 2019-12-11T20:02:39+01:00 Download 6356189
Download 7cdd7d2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 280 2019-12-08T01:00:50+01:00 Download 773bd1a
Download 6959c0a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 280 2019-12-07T23:20:19+01:00 Download 841b038
Download 190ed5c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 280 2019-12-07T19:46:47+01:00 Download 69d709a
Download 44083ef Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 280 2019-12-05T19:03:08+01:00 Download 9fc1de2
Download de6af05 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 280 2019-11-30T17:06:41+01:00 Download d1fa3ae
Download d1fa3ae Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / svcomp20 280 2019-11-30T01:44:37+01:00
Download 5e37a8a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 280 2019-12-01T19:07:03+01:00
Download fadddc5 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Symbiotic 2 2019-12-02 02:03:43
Download 0d62dd2 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.9 359 2019-11-30T12:04:39+01:00
Download e04716b Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ 359 2019-12-01T04:08:55+01:00

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

Trying to find witnesses for program (2d9abcf9faff65782976ff66ac41ce5573829ea9e54b54bbb8915def7a894f41, sv-benchmarks/c/eca-rers2012/Problem02_label38_true-unreach-call_false-termination.c).

Found 17 witnesses for program sv-benchmarks/c/eca-rers2012/Problem02_label38_true-unreach-call_false-termination.c, 2d9abcf9faff65782976ff66ac41ce5573829ea9e54b54bbb8915def7a894f41
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/2d9abcf9faff65782976ff66ac41ce5573829ea9e54b54bbb8915def7a894f41.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download de8f2cb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-08T05:06:26
Download 606fce4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 280 2018-12-06T22:53:54+01:00
Download 93606db Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 280 2018-12-10T20:14:28+01:00 Download eb4dcbd
Download 05e6d46 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 280 2018-12-09T20:17:45+01:00 Download 94bdead
Download 61bb826 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 280 2018-12-09T19:59:37+01:00 Download 96dbb5a
Download d50c15f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 280 2018-12-09T17:29:57+01:00 Download 169bd24
Download dfeec88 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 280 2018-12-08T21:28:55+01:00 Download de8f2cb
Download 7694853 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 280 2018-12-08T06:59:14+01:00 Download 606fce4
Download a2df936 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 280 2018-12-08T04:29:22+01:00 Download 93301ec
Download 3adb1b5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 280 2018-12-06T09:28:27+01:00 Download 1cffe31
Download fff5fbc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 280 2018-12-06T09:06:31+01:00 Download 7ef6153
Download 69a413f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 280 2018-12-06T08:17:12+01:00 Download 6467768
Download 7ef6153 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 280 2018-12-06T02:07:40+01:00
Download 32660d9 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 359 2018-12-06T13:13:18+01:00
Download 28a2d53 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn 29852 356 2018-12-08T08:59:00+01:00
Download 49ea7b2 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn 29852 356 2018-12-06T09:49:08+01:00
Download aabcbd2 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn 29852 359 2018-12-05T18:43:38+01:00

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

Trying to find witnesses for program (2d9abcf9faff65782976ff66ac41ce5573829ea9e54b54bbb8915def7a894f41, sv-benchmarks/c/eca-rers2012/Problem02_label38_true-unreach-call_false-termination.c).

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 90a82d6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Taipan 161 2017-12-02T16:35Z
Download a214b40 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Kojak 182 2017-12-02T14:12Z
Download 2582e9b 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 25f6542 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 280 2017-12-03T06:50:39+01:00 5cc42dd
Download 637836d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 280 2017-12-03T04:09:11+01:00 0656214
Download 3bea860 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 280 2017-12-03T02:01:55+01:00 efcea3c
Download 785f2ed Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 280 2017-12-03T00:27:59+01:00 8c0008c
Download 7c2bf36 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 280 2017-12-02T15:14:53+01:00 407e9ad
Download af02602 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 280 2017-12-01T06:46:24+01:00 e1ef12f
Download 604a3a7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 280 2017-12-01T05:57:48+01:00 0a4afce
Download 3c3fbee Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 280 2017-12-01T05:56:34+01:00 8c2ab46
Download c257fe1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 280 2017-12-01T04:38:15+01:00 e956a37
Download 6325534 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 280 2017-11-30T18:12:37+01:00
Download 7df4ce5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26758M 319 2017-11-30T11:27:55+01:00
Download 20c5d07 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26725 280 2017-12-01T02:59:37+01:00
Download 33c98bc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker (unknown version) 462 2017-12-01T22:34:28+01:00
Download 036d819 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Automizer 161 2017-12-02T01:02Z
Download bba6ffe Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness 2LS 811 2017-11-30T12:35 CET (sv-comp)
Download 3604ddb Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.6.1-svn 26773 334 2017-12-01T16:04:05+01:00
Download 18aaddd Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Automizer 15 2017-12-03T11:18Z
Download 78f62de Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness 2LS 26 2017-12-01T17:18 CET (sv-comp)

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

Trying to find witnesses for program (2d9abcf9faff65782976ff66ac41ce5573829ea9e54b54bbb8915def7a894f41, sv-benchmarks/c/eca-rers2012/Problem02_label38_true-unreach-call_false-termination.c).

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

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