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/ldv-linux-3.0/module_get_put-drivers-block-drbd-drbd.ko_false-unreach-call.cil.out.i
programSHA 0240a58a1d211714124d2332b7d89f99342c5992fcca90758b3f3499b856a5fe
witnessName results-validated/cpa-seq-validate-violation-witnesses-cpa-bam-bnb.2018-12-05_1542.logfiles/sv-comp19_prop-reachsafety.module_get_put-drivers-block-drbd-drbd.ko_false-unreach-call.cil.out.i.files/witness.graphml
witnessSHA 7bf05ac39a5a0d5c834a32545610f8eadcecd47c2550747162f92f4c3d0dcbbd

Information about the Witness from Competition Database

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

Key Value
architecture 64bit
creationtime 2018-12-05T16:12:33+01:00
inputwitnesshash ad7f7eecdba1825715867783253b3c9a0849f06d53e38c010f68349f6af04074
producer CPAchecker 1.7-svn 29852
program-sha256 0240a58a1d211714124d2332b7d89f99342c5992fcca90758b3f3499b856a5fe
programfile ../../sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-block-drbd-drbd.ko_false-unreach-call.cil.out.i
programhash 0240a58a1d211714124d2332b7d89f99342c5992fcca90758b3f3499b856a5fe
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/7bf05ac39a5a0d5c834a32545610f8eadcecd47c2550747162f92f4c3d0dcbbd.graphml
witness-sha256 7bf05ac39a5a0d5c834a32545610f8eadcecd47c2550747162f92f4c3d0dcbbd
witness-size 16518
witness-type violation_witness

This witness was created for this program (cf. table above, 0240a58a1d211714124d2332b7d89f99342c5992fcca90758b3f3499b856a5fe).

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

Trying to find witnesses for program (0240a58a1d211714124d2332b7d89f99342c5992fcca90758b3f3499b856a5fe, sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-block-drbd-drbd.ko_false-unreach-call.cil.out.i).

Found 0 witnesses for program sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-block-drbd-drbd.ko_false-unreach-call.cil.out.i, 0240a58a1d211714124d2332b7d89f99342c5992fcca90758b3f3499b856a5fe
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/0240a58a1d211714124d2332b7d89f99342c5992fcca90758b3f3499b856a5fe.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 (0240a58a1d211714124d2332b7d89f99342c5992fcca90758b3f3499b856a5fe, sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-block-drbd-drbd.ko_false-unreach-call.cil.out.i).

Found 0 witnesses for program sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-block-drbd-drbd.ko_false-unreach-call.cil.out.i, 0240a58a1d211714124d2332b7d89f99342c5992fcca90758b3f3499b856a5fe
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/0240a58a1d211714124d2332b7d89f99342c5992fcca90758b3f3499b856a5fe.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 (0240a58a1d211714124d2332b7d89f99342c5992fcca90758b3f3499b856a5fe, sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-block-drbd-drbd.ko_false-unreach-call.cil.out.i).

Found 0 witnesses for program sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-block-drbd-drbd.ko_false-unreach-call.cil.out.i, 0240a58a1d211714124d2332b7d89f99342c5992fcca90758b3f3499b856a5fe
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/0240a58a1d211714124d2332b7d89f99342c5992fcca90758b3f3499b856a5fe.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 (0240a58a1d211714124d2332b7d89f99342c5992fcca90758b3f3499b856a5fe, sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-block-drbd-drbd.ko_false-unreach-call.cil.out.i).

Found 0 witnesses for program sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-block-drbd-drbd.ko_false-unreach-call.cil.out.i, 0240a58a1d211714124d2332b7d89f99342c5992fcca90758b3f3499b856a5fe
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/0240a58a1d211714124d2332b7d89f99342c5992fcca90758b3f3499b856a5fe.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 (0240a58a1d211714124d2332b7d89f99342c5992fcca90758b3f3499b856a5fe, sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-block-drbd-drbd.ko_false-unreach-call.cil.out.i).

Found 0 witnesses for program sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-block-drbd-drbd.ko_false-unreach-call.cil.out.i, 0240a58a1d211714124d2332b7d89f99342c5992fcca90758b3f3499b856a5fe
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/0240a58a1d211714124d2332b7d89f99342c5992fcca90758b3f3499b856a5fe.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 '19

Trying to find witnesses for program (0240a58a1d211714124d2332b7d89f99342c5992fcca90758b3f3499b856a5fe, sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-block-drbd-drbd.ko_false-unreach-call.cil.out.i).

Found 12 witnesses for program sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-block-drbd-drbd.ko_false-unreach-call.cil.out.i, 0240a58a1d211714124d2332b7d89f99342c5992fcca90758b3f3499b856a5fe
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/0240a58a1d211714124d2332b7d89f99342c5992fcca90758b3f3499b856a5fe.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 22f20e6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 6 2018-12-08T04:35:04
Download bb5dd5f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7 23 2018-12-10T17:46:59+01:00
Download 8206d24 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 19 2018-12-07T09:25:26+01:00
Download 95d3334 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 17 2018-12-10T20:36:51+01:00 Download bb5dd5f
Download c28b903 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 17 2018-12-08T22:11:02+01:00 Download 22f20e6
Download 865f139 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 17 2018-12-08T08:42:48+01:00 Download 8206d24
Download 1907540 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 19 2018-12-08T05:01:34+01:00 Download 0dfea1f
Download 84f4267 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 17 2018-12-06T09:48:22+01:00 Download c690046
Download be802ad Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 37 2018-12-06T09:19:19+01:00 Download e544cb5
Download c690046 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 19 2018-12-05T18:05:09+01:00
Download 7bf05ac Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 17 2018-12-05T16:12:33+01:00 Download ad7f7ee
Download ad7f7ee Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29794 18 2018-12-05T05:49:52+01:00

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

Trying to find witnesses for program (0240a58a1d211714124d2332b7d89f99342c5992fcca90758b3f3499b856a5fe, sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-block-drbd-drbd.ko_false-unreach-call.cil.out.i).

Found 0 witnesses for program sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-block-drbd-drbd.ko_false-unreach-call.cil.out.i, 0240a58a1d211714124d2332b7d89f99342c5992fcca90758b3f3499b856a5fe
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/0240a58a1d211714124d2332b7d89f99342c5992fcca90758b3f3499b856a5fe.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 '17

Trying to find witnesses for program (0240a58a1d211714124d2332b7d89f99342c5992fcca90758b3f3499b856a5fe, sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-block-drbd-drbd.ko_false-unreach-call.cil.out.i).

Found 0 witnesses for program sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-block-drbd-drbd.ko_false-unreach-call.cil.out.i, 0240a58a1d211714124d2332b7d89f99342c5992fcca90758b3f3499b856a5fe
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/0240a58a1d211714124d2332b7d89f99342c5992fcca90758b3f3499b856a5fe.json

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