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/product-lines/elevator_spec2_product30_false-unreach-call_true-termination.cil.c
programSHA 4f9c0d446c683bf57f8ba0a9ca884e97f65b7c47fe9d55b3bb71f96f33c68009
witnessName results-verified/cbmc-path.2018-12-04_2245.logfiles/sv-comp19_prop-reachsafety.elevator_spec2_product30_false-unreach-call_true-termination.cil.c.files/witness.graphml
witnessSHA 01070d7377533ff5774422199f7c3443a1b7c73590d72520d77feda444a368ba

Information about the Witness from Competition Database

from https://sv-comp.sosy-lab.org/2019/results/witnessInfoByHash/01070d7377533ff5774422199f7c3443a1b7c73590d72520d77feda444a368ba.json

Key Value
architecture 32bit
creationtime 2018-12-06T01:15 CET (sv-comp)
producer CBMC
programfile ../../sv-benchmarks/c/product-lines/elevator_spec2_product30_false-unreach-call_true-termination.cil.c
programhash 16eb34bf8ac588b2057113d948643073bd800c2b
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/01070d7377533ff5774422199f7c3443a1b7c73590d72520d77feda444a368ba.graphml
witness-sha256 01070d7377533ff5774422199f7c3443a1b7c73590d72520d77feda444a368ba
witness-size 106503
witness-type violation_witness

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

Trying to find witnesses for program (4f9c0d446c683bf57f8ba0a9ca884e97f65b7c47fe9d55b3bb71f96f33c68009, sv-benchmarks/c/product-lines/elevator_spec2_product30_false-unreach-call_true-termination.cil.c).

Found 0 witnesses for program sv-benchmarks/c/product-lines/elevator_spec2_product30_false-unreach-call_true-termination.cil.c, 4f9c0d446c683bf57f8ba0a9ca884e97f65b7c47fe9d55b3bb71f96f33c68009
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/4f9c0d446c683bf57f8ba0a9ca884e97f65b7c47fe9d55b3bb71f96f33c68009.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 (4f9c0d446c683bf57f8ba0a9ca884e97f65b7c47fe9d55b3bb71f96f33c68009, sv-benchmarks/c/product-lines/elevator_spec2_product30_false-unreach-call_true-termination.cil.c).

Found 0 witnesses for program sv-benchmarks/c/product-lines/elevator_spec2_product30_false-unreach-call_true-termination.cil.c, 4f9c0d446c683bf57f8ba0a9ca884e97f65b7c47fe9d55b3bb71f96f33c68009
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/4f9c0d446c683bf57f8ba0a9ca884e97f65b7c47fe9d55b3bb71f96f33c68009.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 (4f9c0d446c683bf57f8ba0a9ca884e97f65b7c47fe9d55b3bb71f96f33c68009, sv-benchmarks/c/product-lines/elevator_spec2_product30_false-unreach-call_true-termination.cil.c).

Found 0 witnesses for program sv-benchmarks/c/product-lines/elevator_spec2_product30_false-unreach-call_true-termination.cil.c, 4f9c0d446c683bf57f8ba0a9ca884e97f65b7c47fe9d55b3bb71f96f33c68009
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/4f9c0d446c683bf57f8ba0a9ca884e97f65b7c47fe9d55b3bb71f96f33c68009.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 (4f9c0d446c683bf57f8ba0a9ca884e97f65b7c47fe9d55b3bb71f96f33c68009, sv-benchmarks/c/product-lines/elevator_spec2_product30_false-unreach-call_true-termination.cil.c).

Found 0 witnesses for program sv-benchmarks/c/product-lines/elevator_spec2_product30_false-unreach-call_true-termination.cil.c, 4f9c0d446c683bf57f8ba0a9ca884e97f65b7c47fe9d55b3bb71f96f33c68009
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/4f9c0d446c683bf57f8ba0a9ca884e97f65b7c47fe9d55b3bb71f96f33c68009.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 (4f9c0d446c683bf57f8ba0a9ca884e97f65b7c47fe9d55b3bb71f96f33c68009, sv-benchmarks/c/product-lines/elevator_spec2_product30_false-unreach-call_true-termination.cil.c).

Found 15 witnesses for program sv-benchmarks/c/product-lines/elevator_spec2_product30_false-unreach-call_true-termination.cil.c, 4f9c0d446c683bf57f8ba0a9ca884e97f65b7c47fe9d55b3bb71f96f33c68009
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/4f9c0d446c683bf57f8ba0a9ca884e97f65b7c47fe9d55b3bb71f96f33c68009.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download e57a25b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2019-12-01 20:33:25
Download 75e64bf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 115 2019-12-04T00:25 CET (comp)
Download 8ec5e80 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 203 2019-12-11T21:40:10+01:00 Download 4313af1
Download 8115d28 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 203 2019-12-11T21:09:03+01:00 Download e57a25b
Download 543e5f5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 203 2019-12-11T20:54:22+01:00 Download d4d3091
Download 733d38c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 203 2019-12-11T20:44:45+01:00 Download b567657
Download d9481b1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 203 2019-12-04T02:58:20+01:00 Download 75e64bf
Download aef1764 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 203 2019-12-03T08:57:03+01:00 Download 1512a47
Download 2641b7a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 203 2019-12-03T08:08:32+01:00 Download 6690764
Download 6690764 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 187 2019-11-30T12:09:28+01:00
Download 4313af1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 187 2019-12-01T03:09:34+01:00
Download a12c249 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 314 2019-12-08T01:51:41+01:00 Download 1e6edc0
Download af2a080 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 314 2019-12-05T20:20:18+01:00 Download a3a7d01
Download 81677c7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 314 2019-12-05T19:34:10+01:00 Download 0800c46
Download 7c52c38 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2019-12-04T00:19 CET (comp)

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

Trying to find witnesses for program (4f9c0d446c683bf57f8ba0a9ca884e97f65b7c47fe9d55b3bb71f96f33c68009, sv-benchmarks/c/product-lines/elevator_spec2_product30_false-unreach-call_true-termination.cil.c).

Found 21 witnesses for program sv-benchmarks/c/product-lines/elevator_spec2_product30_false-unreach-call_true-termination.cil.c, 4f9c0d446c683bf57f8ba0a9ca884e97f65b7c47fe9d55b3bb71f96f33c68009
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/4f9c0d446c683bf57f8ba0a9ca884e97f65b7c47fe9d55b3bb71f96f33c68009.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 97d1217 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2018-12-08T00:08 CET (sv-comp)
Download 0942ae4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 30 2018-12-08T03:40:50
Download d401c67 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 130 2018-12-07T04:07 CET (sv-comp)
Download 750f355 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 209 2018-12-07T11:02:49+01:00
Download dfe3c99 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 203 2018-12-10T10:49:00+01:00 Download a05304b
Download 533da0a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 204 2018-12-09T18:20:21+01:00 Download b33f93c
Download c123046 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 203 2018-12-08T23:42:57+01:00 Download 97d1217
Download 053b6f2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 140 2018-12-08T22:11:25+01:00 Download 0942ae4
Download 2303f5c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 203 2018-12-08T08:08:32+01:00 Download 750f355
Download f6638a8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 203 2018-12-08T05:01:45+01:00 Download 10f4946
Download 8c8a6ae Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 203 2018-12-08T04:28:23+01:00 Download a05304b
Download 4f8fd2c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 203 2018-12-07T17:44:26+01:00 Download d401c67
Download 8174b65 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 203 2018-12-06T10:17:44+01:00 Download a3c2de4
Download a99e920 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 203 2018-12-06T09:47:57+01:00 Download 61ba61c
Download 61ba61c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 187 2018-12-05T10:09:51+01:00
Download 336dd0f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 314 2018-12-10T20:38:07+01:00 Download 6438b11
Download 8b7f882 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 314 2018-12-06T09:42:27+01:00 Download 8ec064a
Download dfb2c98 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 314 2018-12-06T09:18:21+01:00 Download df70a0c
Download b270890 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 314 2018-12-06T09:02:01+01:00 Download 01070d7
Download 8fbb8c9 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T05:07 CET (sv-comp)
Download c603820 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-07T06:39 CET (sv-comp)

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

Trying to find witnesses for program (4f9c0d446c683bf57f8ba0a9ca884e97f65b7c47fe9d55b3bb71f96f33c68009, sv-benchmarks/c/product-lines/elevator_spec2_product30_false-unreach-call_true-termination.cil.c).

Found 0 witnesses for program sv-benchmarks/c/product-lines/elevator_spec2_product30_false-unreach-call_true-termination.cil.c, 4f9c0d446c683bf57f8ba0a9ca884e97f65b7c47fe9d55b3bb71f96f33c68009
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/4f9c0d446c683bf57f8ba0a9ca884e97f65b7c47fe9d55b3bb71f96f33c68009.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 (4f9c0d446c683bf57f8ba0a9ca884e97f65b7c47fe9d55b3bb71f96f33c68009, sv-benchmarks/c/product-lines/elevator_spec2_product30_false-unreach-call_true-termination.cil.c).

Found 0 witnesses for program sv-benchmarks/c/product-lines/elevator_spec2_product30_false-unreach-call_true-termination.cil.c, 4f9c0d446c683bf57f8ba0a9ca884e97f65b7c47fe9d55b3bb71f96f33c68009
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/4f9c0d446c683bf57f8ba0a9ca884e97f65b7c47fe9d55b3bb71f96f33c68009.json

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