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_spec3_product23_false-unreach-call_true-termination.cil.c
programSHA 37d3161b649dc9605dccbe05787269f3ca66485677be45c5cffbf600c89e0897
witnessName results-validated/cpa-seq-validate-violation-witnesses-2ls.2018-12-06_0936.logfiles/sv-comp19_prop-reachsafety.elevator_spec3_product23_false-unreach-call_true-termination.cil.c.files/witness.graphml
witnessSHA 74d720945ca9a4712e38499674933ae9409620aafd191dfad45eb3ba92b5d9cd

Information about the Witness from Competition Database

from https://sv-comp.sosy-lab.org/2019/results/witnessInfoByHash/74d720945ca9a4712e38499674933ae9409620aafd191dfad45eb3ba92b5d9cd.json

Key Value
architecture 32bit
creationtime 2018-12-06T09:40:46+01:00
inputwitnesshash 1a8ae54bcb27906a24ed9a4fea5ce35cfd22bb3a2a705616f3450b746fa49adb
producer CPAchecker 1.7-svn 29852
program-sha256 37d3161b649dc9605dccbe05787269f3ca66485677be45c5cffbf600c89e0897
programfile ../../sv-benchmarks/c/product-lines/elevator_spec3_product23_false-unreach-call_true-termination.cil.c
programhash 37d3161b649dc9605dccbe05787269f3ca66485677be45c5cffbf600c89e0897
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/74d720945ca9a4712e38499674933ae9409620aafd191dfad45eb3ba92b5d9cd.graphml
witness-sha256 74d720945ca9a4712e38499674933ae9409620aafd191dfad45eb3ba92b5d9cd
witness-size 315877
witness-type correctness_witness

This witness was created for this program (cf. table above, 37d3161b649dc9605dccbe05787269f3ca66485677be45c5cffbf600c89e0897).

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

Trying to find witnesses for program (37d3161b649dc9605dccbe05787269f3ca66485677be45c5cffbf600c89e0897, sv-benchmarks/c/product-lines/elevator_spec3_product23_false-unreach-call_true-termination.cil.c).

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

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

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

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

Found 16 witnesses for program sv-benchmarks/c/product-lines/elevator_spec3_product23_false-unreach-call_true-termination.cil.c, 37d3161b649dc9605dccbe05787269f3ca66485677be45c5cffbf600c89e0897
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/37d3161b649dc9605dccbe05787269f3ca66485677be45c5cffbf600c89e0897.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 1c45571 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2019-12-01 16:59:25
Download e56cc50 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 194 2019-12-03T23:59 CET (comp)
Download 17da6e6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 335 2019-12-11T21:44:16+01:00 Download 10e4519
Download b0f613f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 336 2019-12-11T21:09:48+01:00 Download 1c45571
Download 4562bda Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 335 2019-12-11T20:55:07+01:00 Download 8f2e42d
Download a5212a6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 336 2019-12-11T20:44:56+01:00 Download 57f7fec
Download 2eccd67 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 335 2019-12-08T01:51:46+01:00 Download b7d64ab
Download aac4042 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 335 2019-12-04T02:58:28+01:00 Download e56cc50
Download 1f98763 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 335 2019-12-03T08:56:52+01:00 Download f40dd36
Download da1e45e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 335 2019-12-03T08:09:34+01:00 Download 5118000
Download 5118000 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 296 2019-11-30T02:45:11+01:00
Download b7d64ab Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8 337 2019-12-07T16:05:56+01:00
Download 10e4519 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 335 2019-12-01T00:37:41+01:00
Download 5a61a8e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 316 2019-12-05T20:20:46+01:00 Download 4ab82f3
Download d5f8cfa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 316 2019-12-05T19:34:10+01:00 Download a02d01c
Download 12a7b72 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2019-12-04T00:14 CET (comp)

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

Trying to find witnesses for program (37d3161b649dc9605dccbe05787269f3ca66485677be45c5cffbf600c89e0897, sv-benchmarks/c/product-lines/elevator_spec3_product23_false-unreach-call_true-termination.cil.c).

Found 22 witnesses for program sv-benchmarks/c/product-lines/elevator_spec3_product23_false-unreach-call_true-termination.cil.c, 37d3161b649dc9605dccbe05787269f3ca66485677be45c5cffbf600c89e0897
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/37d3161b649dc9605dccbe05787269f3ca66485677be45c5cffbf600c89e0897.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download d0f6003 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2018-12-08T16:15 CET (sv-comp)
Download e02fed4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 59 2018-12-08T07:13:29
Download 5253092 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 220 2018-12-07T13:57 CET (sv-comp)
Download e028756 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7 308 2018-12-10T18:41:10+01:00
Download 8c44db6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 337 2018-12-08T02:36:28+01:00
Download 3117e5b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 335 2018-12-10T20:35:23+01:00 Download e028756
Download d01b9d2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 335 2018-12-10T10:48:54+01:00 Download 91a437e
Download 3440ca9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 336 2018-12-09T18:20:02+01:00 Download c702d54
Download 1472bbc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 335 2018-12-08T23:44:10+01:00 Download d0f6003
Download bbc2813 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 208 2018-12-08T22:08:15+01:00 Download e02fed4
Download fb9620a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 335 2018-12-08T08:04:13+01:00 Download 8c44db6
Download d6e8c32 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 335 2018-12-08T04:59:43+01:00 Download 05b72fd
Download c88dc54 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 335 2018-12-08T04:33:57+01:00 Download 91a437e
Download 7e93629 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 335 2018-12-07T17:42:53+01:00 Download 5253092
Download 7358b4e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 335 2018-12-06T10:19:27+01:00 Download 8f7fa3d
Download 43c6667 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 335 2018-12-06T09:48:18+01:00 Download 720a30a
Download 720a30a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 296 2018-12-05T16:56:24+01:00
Download 74d7209 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 316 2018-12-06T09:40:46+01:00 Download 1a8ae54
Download 3a67f18 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 316 2018-12-06T09:12:05+01:00 Download 40d869c
Download b4f3fed Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 316 2018-12-06T09:11:35+01:00 Download 3955f53
Download 8b85c60 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T21:12 CET (sv-comp)
Download 2f00ee9 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-07T14:30 CET (sv-comp)

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

Trying to find witnesses for program (37d3161b649dc9605dccbe05787269f3ca66485677be45c5cffbf600c89e0897, sv-benchmarks/c/product-lines/elevator_spec3_product23_false-unreach-call_true-termination.cil.c).

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

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

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