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/Problem06_label29_false-unreach-call.c
programSHA 96869477f42cb3d84e0274ad4f009324e2ee0fbd0bbaee6f0d0c1d9f224d56a7
witnessName results-verified/symbiotic.2017-12-01_2241.logfiles/sv-comp18.Problem06_label29_false-unreach-call.c.files/witness.graphml
witnessSHA 70623016dab83703efc73bfe200468535c9d90b67703b425b633cc52f6096036

Information about the Witness from Competition Database

from https://sv-comp.sosy-lab.org/2018/results/witnessInfoByHash/70623016dab83703efc73bfe200468535c9d90b67703b425b633cc52f6096036.json

Key Value
architecture 32bit
creationtime 2017-12-02T14:20 CET (sv-comp)
producer Symbiotic
program-sha256 96869477f42cb3d84e0274ad4f009324e2ee0fbd0bbaee6f0d0c1d9f224d56a7
programfile /tmp/vcloud-vcloud-master/worker/working_dir_e6a8119a-9bcf-4735-a667-c3b7bfe24961/sv-benchmarks/c/eca-rers2012/Problem06_label29_false-unreach-call.c
programhash ae1e3c7dd201337ce815a1faae41aefc5fa59715
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/70623016dab83703efc73bfe200468535c9d90b67703b425b633cc52f6096036.graphml
witness-sha256 70623016dab83703efc73bfe200468535c9d90b67703b425b633cc52f6096036
witness-size 1237
witness-type violation_witness

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

Trying to find witnesses for program (96869477f42cb3d84e0274ad4f009324e2ee0fbd0bbaee6f0d0c1d9f224d56a7, sv-benchmarks/c/eca-rers2012/Problem06_label29_false-unreach-call.c).

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

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

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

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

Found 8 witnesses for program sv-benchmarks/c/eca-rers2012/Problem06_label29_false-unreach-call.c, 96869477f42cb3d84e0274ad4f009324e2ee0fbd0bbaee6f0d0c1d9f224d56a7
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/96869477f42cb3d84e0274ad4f009324e2ee0fbd0bbaee6f0d0c1d9f224d56a7.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download ab9ac5c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 455 2019-12-03T22:38 CET (comp)
Download 586fc93 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 1582 2019-12-11T21:45:43+01:00 Download bdfef0b
Download 5887eee Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 1581 2019-12-11T20:55:37+01:00 Download eb22980
Download 2022544 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 1582 2019-12-11T20:44:36+01:00 Download cb6f36c
Download e16eff7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 2113 2019-12-04T02:58:30+01:00 Download ab9ac5c
Download 1c9c475 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 1581 2019-12-03T08:10:09+01:00 Download 518f358
Download 518f358 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 1597 2019-11-30T07:57:49+01:00
Download bdfef0b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 1603 2019-12-01T00:27:03+01:00

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

Trying to find witnesses for program (96869477f42cb3d84e0274ad4f009324e2ee0fbd0bbaee6f0d0c1d9f224d56a7, sv-benchmarks/c/eca-rers2012/Problem06_label29_false-unreach-call.c).

Found 12 witnesses for program sv-benchmarks/c/eca-rers2012/Problem06_label29_false-unreach-call.c, 96869477f42cb3d84e0274ad4f009324e2ee0fbd0bbaee6f0d0c1d9f224d56a7
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/96869477f42cb3d84e0274ad4f009324e2ee0fbd0bbaee6f0d0c1d9f224d56a7.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 8444da8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2018-12-08T04:45 CET (sv-comp)
Download 299cc9f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 494 2018-12-07T10:03 CET (sv-comp)
Download 451f7e3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 1597 2018-12-07T22:17:14+01:00
Download 29dee2c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 1582 2018-12-09T18:20:59+01:00 Download 7629023
Download 577791b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 1602 2018-12-08T23:44:54+01:00 Download 8444da8
Download b5d49c3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 1581 2018-12-08T07:48:11+01:00 Download 451f7e3
Download 38d95b7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 1582 2018-12-08T05:00:32+01:00 Download 07e152e
Download 4b48461 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 2113 2018-12-07T17:44:43+01:00 Download 299cc9f
Download d1c2f49 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 1581 2018-12-06T10:13:36+01:00 Download 94994a2
Download a1850ed Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 1581 2018-12-06T09:49:08+01:00 Download 97dbffd
Download 3b67893 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 2115 2018-12-06T09:05:28+01:00 Download 1535c1e
Download 97dbffd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 1597 2018-12-05T18:52:55+01:00

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

Trying to find witnesses for program (96869477f42cb3d84e0274ad4f009324e2ee0fbd0bbaee6f0d0c1d9f224d56a7, sv-benchmarks/c/eca-rers2012/Problem06_label29_false-unreach-call.c).

Found 5 witnesses for program sv-benchmarks/c/eca-rers2012/Problem06_label29_false-unreach-call.c, 96869477f42cb3d84e0274ad4f009324e2ee0fbd0bbaee6f0d0c1d9f224d56a7
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/96869477f42cb3d84e0274ad4f009324e2ee0fbd0bbaee6f0d0c1d9f224d56a7.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 7062301 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2017-12-02T14:20 CET (sv-comp)
Download be8e5ca Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 5 2017-12-01T21:24:54.191937
Download fead9bd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 5 2017-12-01T11:44:35.222634
Download 0a754cf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 884 2017-11-30T13:45:30+01:00
Download 22f74cb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 563 2017-11-30T20:53 CET (sv-comp)

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

Trying to find witnesses for program (96869477f42cb3d84e0274ad4f009324e2ee0fbd0bbaee6f0d0c1d9f224d56a7, sv-benchmarks/c/eca-rers2012/Problem06_label29_false-unreach-call.c).

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

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