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/Problem03_label09_false-unreach-call.c
programSHA f9b640580574f7329fb3f8918ccfecc42683beb2d05a2453b1ab4ae97dfba802
witnessName results-verified/2ls.2017-11-30_1120.logfiles/sv-comp18.Problem03_label09_false-unreach-call.c.files/witness.graphml
witnessSHA 2db2ac89822a631151b6575348ffef8b838a80b4405d1c0262be3c41fc034851

Information about the Witness from Competition Database

from https://sv-comp.sosy-lab.org/2018/results/witnessInfoByHash/2db2ac89822a631151b6575348ffef8b838a80b4405d1c0262be3c41fc034851.json

Key Value
architecture 32bit
creationtime 2017-11-30T18:28 CET (sv-comp)
producer 2LS
program-sha256 f9b640580574f7329fb3f8918ccfecc42683beb2d05a2453b1ab4ae97dfba802
programfile ../../sv-benchmarks/c/eca-rers2012/Problem03_label09_false-unreach-call.c
programhash c7e2f80610aedd2a38d03dcaf2820fb6da6158ed
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/2db2ac89822a631151b6575348ffef8b838a80b4405d1c0262be3c41fc034851.graphml
witness-sha256 2db2ac89822a631151b6575348ffef8b838a80b4405d1c0262be3c41fc034851
witness-size 183565
witness-type violation_witness

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

Trying to find witnesses for program (f9b640580574f7329fb3f8918ccfecc42683beb2d05a2453b1ab4ae97dfba802, sv-benchmarks/c/eca-rers2012/Problem03_label09_false-unreach-call.c).

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

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

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

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

Found 11 witnesses for program sv-benchmarks/c/eca-rers2012/Problem03_label09_false-unreach-call.c, f9b640580574f7329fb3f8918ccfecc42683beb2d05a2453b1ab4ae97dfba802
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/f9b640580574f7329fb3f8918ccfecc42683beb2d05a2453b1ab4ae97dfba802.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 5625f7c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 2 2019-12-02 02:03:41
Download be80a72 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 149 2019-12-04T00:10 CET (comp)
Download e67daf8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 502 2019-12-11T21:43:50+01:00 Download 4db65b6
Download 0b9c96e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 502 2019-12-11T21:09:13+01:00 Download 5625f7c
Download 7feb726 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 502 2019-12-11T20:54:40+01:00 Download b9490a1
Download 4f4c0b5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 502 2019-12-11T20:44:51+01:00 Download 2565bea
Download eb6fdfb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 504 2019-12-08T01:51:37+01:00 Download 627f73e
Download 56e9562 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 669 2019-12-04T02:58:06+01:00 Download be80a72
Download 5114bda Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 502 2019-12-03T08:10:27+01:00 Download 2992f5e
Download 2992f5e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 502 2019-11-30T04:37:23+01:00
Download 4db65b6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 502 2019-11-30T21:34:23+01:00

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

Trying to find witnesses for program (f9b640580574f7329fb3f8918ccfecc42683beb2d05a2453b1ab4ae97dfba802, sv-benchmarks/c/eca-rers2012/Problem03_label09_false-unreach-call.c).

Found 15 witnesses for program sv-benchmarks/c/eca-rers2012/Problem03_label09_false-unreach-call.c, f9b640580574f7329fb3f8918ccfecc42683beb2d05a2453b1ab4ae97dfba802
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/f9b640580574f7329fb3f8918ccfecc42683beb2d05a2453b1ab4ae97dfba802.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download d5af69b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2018-12-08T04:51 CET (sv-comp)
Download 1b4af7e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 13 2018-12-08T03:57:09
Download a92f75e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 161 2018-12-07T06:32 CET (sv-comp)
Download c611d9b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 507 2018-12-07T04:36:14+01:00
Download a458fbb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 504 2018-12-10T20:35:40+01:00 Download 22ead09
Download 8739a82 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 502 2018-12-09T18:21:19+01:00 Download 0eb0b96
Download 85bb2be Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 506 2018-12-08T23:45:00+01:00 Download d5af69b
Download b474715 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 502 2018-12-08T22:11:32+01:00 Download 1b4af7e
Download cec54e6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 502 2018-12-08T09:02:35+01:00 Download c611d9b
Download 12c4094 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 502 2018-12-08T04:51:33+01:00 Download fd05335
Download 61c54c1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 669 2018-12-07T17:45:42+01:00 Download a92f75e
Download 083d823 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 502 2018-12-06T10:18:37+01:00 Download dfc30b9
Download b06f1cb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 502 2018-12-06T09:49:11+01:00 Download 75b0a26
Download 86c54cc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 670 2018-12-06T09:17:41+01:00 Download e338d54
Download 75b0a26 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 502 2018-12-06T04:25:46+01:00

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

Trying to find witnesses for program (f9b640580574f7329fb3f8918ccfecc42683beb2d05a2453b1ab4ae97dfba802, sv-benchmarks/c/eca-rers2012/Problem03_label09_false-unreach-call.c).

Found 9 witnesses for program sv-benchmarks/c/eca-rers2012/Problem03_label09_false-unreach-call.c, f9b640580574f7329fb3f8918ccfecc42683beb2d05a2453b1ab4ae97dfba802
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/f9b640580574f7329fb3f8918ccfecc42683beb2d05a2453b1ab4ae97dfba802.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 85a9c1c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Veriabs 3 2017-12-03T01:08 CET (sv-comp)
Download 3948e95 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2017-12-02T00:18 CET (sv-comp)
Download ad6743d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 5 2017-12-01T13:21:00.287813
Download 7780c89 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 5 2017-12-01T12:25:52.568416
Download b1726ec Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 21 2017-12-01T03:45 CET (sv-comp)
Download 74680f7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 286 2017-11-30T21:16:51+01:00
Download 349758c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 1101 2017-11-30T21:56:27+01:00
Download 0984e7a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 183 2017-11-30T21:16 CET (sv-comp)
Download 2db2ac8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness 2LS 184 2017-11-30T18:28 CET (sv-comp)

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

Trying to find witnesses for program (f9b640580574f7329fb3f8918ccfecc42683beb2d05a2453b1ab4ae97dfba802, sv-benchmarks/c/eca-rers2012/Problem03_label09_false-unreach-call.c).

Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem03_label09_false-unreach-call.c, f9b640580574f7329fb3f8918ccfecc42683beb2d05a2453b1ab4ae97dfba802
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/f9b640580574f7329fb3f8918ccfecc42683beb2d05a2453b1ab4ae97dfba802.json

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