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_label48_true-unreach-call_false-termination.c
programSHA 5a6adba7e125841467d527d0cea9fd378a2a63cbb7649b0acf6647fb8a1a6f74
witnessName results-verified/cpa-seq.2017-12-01_1227.logfiles/sv-comp18.Problem02_label48_true-unreach-call_false-termination.c.files/witness.graphml
witnessSHA 9ed108b9c7cb7854783ea119c12b1729220cbc07ba7bbb4e055ae84b5934d9c2

Information about the Witness from Competition Database

from https://sv-comp.sosy-lab.org/2018/results/witnessInfoByHash/9ed108b9c7cb7854783ea119c12b1729220cbc07ba7bbb4e055ae84b5934d9c2.json

Key Value
architecture 32bit
creationtime 2017-12-01T14:40:36+01:00
producer CPAchecker 1.6.1-svn 26773
program-sha256 5a6adba7e125841467d527d0cea9fd378a2a63cbb7649b0acf6647fb8a1a6f74
programfile ../../sv-benchmarks/c/eca-rers2012/Problem02_label48_true-unreach-call_false-termination.c
programhash d21c5ccf8cec8e25a14d9a868b5f3d1150798ab4
sourcecodelang C
specification CHECK( init(main()), LTL(F end) )
witness-file witnessFileByHash/9ed108b9c7cb7854783ea119c12b1729220cbc07ba7bbb4e055ae84b5934d9c2.graphml
witness-sha256 9ed108b9c7cb7854783ea119c12b1729220cbc07ba7bbb4e055ae84b5934d9c2
witness-size 334383
witness-type violation_witness

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

Trying to find witnesses for program (5a6adba7e125841467d527d0cea9fd378a2a63cbb7649b0acf6647fb8a1a6f74, sv-benchmarks/c/eca-rers2012/Problem02_label48_true-unreach-call_false-termination.c).

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

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

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 2c75d9d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 280 2019-12-11T20:27:12+01:00 Download f6d072b
Download 25f435c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 280 2019-12-11T20:07:46+01:00 Download 59d44bb
Download 22d8393 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 280 2019-12-11T20:02:23+01:00 Download 2cd831c
Download a30edb4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 280 2019-12-08T00:52:07+01:00 Download 7ce5957
Download 6bd8bb1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 280 2019-12-07T23:27:28+01:00 Download 3f9b1cd
Download 1350771 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 280 2019-12-07T19:47:50+01:00 Download 85aeb7e
Download c6ce932 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 280 2019-12-05T19:02:54+01:00 Download 4846e08
Download 6051c74 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 280 2019-11-30T17:26:06+01:00 Download cbb2f9d
Download cbb2f9d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / svcomp20 280 2019-11-30T09:34:11+01:00
Download 59d44bb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 280 2019-12-01T07:32:39+01:00
Download 73c47f5 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Symbiotic 2 2019-12-02 05:54:38
Download 696b149 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.9 359 2019-11-30T07:04:55+01:00
Download b4fab8c Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ 359 2019-12-01T13:35:38+01:00

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

Trying to find witnesses for program (5a6adba7e125841467d527d0cea9fd378a2a63cbb7649b0acf6647fb8a1a6f74, sv-benchmarks/c/eca-rers2012/Problem02_label48_true-unreach-call_false-termination.c).

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download ec2d55f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-08T09:56:01
Download ee9ce2a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 280 2018-12-07T16:50:54+01:00
Download 3ac633a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 280 2018-12-10T19:57:40+01:00 Download 9323974
Download dc29920 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 280 2018-12-09T20:13:59+01:00 Download bd8b25f
Download 1028bc9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 280 2018-12-09T20:01:44+01:00 Download b3deb2b
Download 5b96500 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 280 2018-12-09T19:57:01+01:00 Download ac508bf
Download 0a35156 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 280 2018-12-08T21:26:55+01:00 Download ec2d55f
Download 55b440e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 280 2018-12-08T05:24:43+01:00 Download ee9ce2a
Download 2d9af78 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 280 2018-12-08T03:58:44+01:00 Download afb9987
Download 7a27549 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 280 2018-12-06T09:28:53+01:00 Download 7fdd0d3
Download dfef4b1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 280 2018-12-06T09:14:08+01:00 Download 5bd8130
Download e0a71b9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 280 2018-12-06T07:24:56+01:00 Download 80169a7
Download 5bd8130 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 280 2018-12-05T13:52:10+01:00
Download 473e25e Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 359 2018-12-07T07:46:36+01:00
Download d0a68a9 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn 29852 356 2018-12-08T08:36:56+01:00
Download 0a4cca5 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn 29852 356 2018-12-06T09:49:19+01:00
Download 55d444f Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn 29852 359 2018-12-05T18:30:00+01:00

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

Trying to find witnesses for program (5a6adba7e125841467d527d0cea9fd378a2a63cbb7649b0acf6647fb8a1a6f74, sv-benchmarks/c/eca-rers2012/Problem02_label48_true-unreach-call_false-termination.c).

Found 19 witnesses for program sv-benchmarks/c/eca-rers2012/Problem02_label48_true-unreach-call_false-termination.c, 5a6adba7e125841467d527d0cea9fd378a2a63cbb7649b0acf6647fb8a1a6f74
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/5a6adba7e125841467d527d0cea9fd378a2a63cbb7649b0acf6647fb8a1a6f74.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 4a73623 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Kojak 191 2017-12-02T03:13Z
Download be8219e 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 fc59039 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 280 2017-12-03T04:25:03+01:00 07a2070
Download 547e702 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 291 2017-12-03T01:13:40+01:00 c959b5e
Download e13f15c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 280 2017-12-02T23:19:35+01:00 9c30319
Download 2561734 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 280 2017-12-02T15:00:57+01:00 ae37d54
Download 9bc728a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 280 2017-12-01T06:50:04+01:00 fcc20fc
Download 80c975a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 280 2017-12-01T06:07:36+01:00 f2566d6
Download c175b30 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 280 2017-12-01T05:59:25+01:00 4d204d7
Download bd4dc74 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 280 2017-12-01T05:59:01+01:00 0659eb7
Download 3d2aca2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 280 2017-11-30T20:44:42+01:00
Download 144f45a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26758M 337 2017-11-30T13:20:59+01:00
Download c6c8c62 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26725 280 2017-12-01T03:14:23+01:00
Download 494dfec Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker (unknown version) 462 2017-12-02T02:24:53+01:00
Download dff31a5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Automizer 161 2017-12-02T07:57Z
Download 90dc8ee Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness 2LS 811 2017-11-30T11:23 CET (sv-comp)
Download 9ed108b Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.6.1-svn 26773 334 2017-12-01T14:40:36+01:00
Download af6b027 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Automizer 15 2017-12-03T11:12Z
Download 3639916 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness 2LS 26 2017-12-01T16:53 CET (sv-comp)

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

Trying to find witnesses for program (5a6adba7e125841467d527d0cea9fd378a2a63cbb7649b0acf6647fb8a1a6f74, sv-benchmarks/c/eca-rers2012/Problem02_label48_true-unreach-call_false-termination.c).

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

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