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_spec1_product09_true-unreach-call_true-termination.cil.c
programSHA cc1d245c1b6dd522eef24e10ecb61060ac8e03b16a9aa0c5e65697d063e52d25
witnessName results-validated/cpa-seq-validate-correctness-witnesses-depthk.2018-12-06_0926.logfiles/sv-comp19_prop-reachsafety.elevator_spec1_product09_true-unreach-call_true-termination.cil.c.files/witness.graphml
witnessSHA 47ac82771b62a0af76c6bc009210fe6ed211ed57677e89dee88c3ab007654e48

Information about the Witness from Competition Database

from https://sv-comp.sosy-lab.org/2019/results/witnessInfoByHash/47ac82771b62a0af76c6bc009210fe6ed211ed57677e89dee88c3ab007654e48.json

Key Value
architecture 32bit
creationtime 2018-12-06T09:30:03+01:00
inputwitnesshash 468d111807fd2d94f2e6f2868252d03a9699ac6a3f474cfde1724993955803b9
producer CPAchecker 1.7-svn 29852
program-sha256 cc1d245c1b6dd522eef24e10ecb61060ac8e03b16a9aa0c5e65697d063e52d25
programfile ../../sv-benchmarks/c/product-lines/elevator_spec1_product09_true-unreach-call_true-termination.cil.c
programhash cc1d245c1b6dd522eef24e10ecb61060ac8e03b16a9aa0c5e65697d063e52d25
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/47ac82771b62a0af76c6bc009210fe6ed211ed57677e89dee88c3ab007654e48.graphml
witness-sha256 47ac82771b62a0af76c6bc009210fe6ed211ed57677e89dee88c3ab007654e48
witness-size 292915
witness-type correctness_witness

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

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

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

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

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

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 93d2634 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2019-12-03T22:49 CET (comp)
Download 074baa6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 293 2019-12-11T20:17:29+01:00 Download 7305f20
Download 8204007 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 293 2019-12-11T20:07:57+01:00 Download 904ae88
Download 0cf4e12 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 293 2019-12-11T20:02:21+01:00 Download aee6f66
Download 4d5af9e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 293 2019-12-08T00:37:43+01:00 Download a9399f9
Download 1bfe701 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 293 2019-12-05T19:20:43+01:00 Download 8ec83fc
Download 6a78657 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 293 2019-12-05T19:03:00+01:00 Download 15686d6
Download 0955f4a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 293 2019-12-04T02:08:03+01:00 Download 93d2634
Download 9ca7859 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 293 2019-11-30T19:54:14+01:00 Download 586fa3d
Download 6e92fc1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 293 2019-11-30T17:26:53+01:00 Download 1244588
Download 1244588 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / svcomp20 293 2019-11-30T13:45:54+01:00
Download a9399f9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8 293 2019-12-07T16:37:42+01:00
Download 904ae88 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 293 2019-12-01T15:56:43+01:00
Download 4444eac Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2019-12-04T00:47 CET (comp)

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download ae0112c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2018-12-08T16:50 CET (sv-comp)
Download 3301113 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-08T08:56:39
Download 0a9b076 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2018-12-07T05:34 CET (sv-comp)
Download 86fb2ff Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 293 2018-12-07T19:10:06+01:00
Download ece2892 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 293 2018-12-10T20:06:45+01:00 Download 2d5cdf4
Download 966f106 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 293 2018-12-10T10:31:33+01:00 Download e50c1f4
Download 710504a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 293 2018-12-08T23:15:50+01:00 Download ae0112c
Download 9143472 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 293 2018-12-08T21:42:48+01:00 Download 3301113
Download bf475ff Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 293 2018-12-08T05:40:21+01:00 Download 86fb2ff
Download fb12d29 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 293 2018-12-08T04:12:41+01:00 Download f09e2f1
Download af45255 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 293 2018-12-08T02:57:32+01:00 Download e50c1f4
Download 9589a57 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 293 2018-12-07T16:39:51+01:00 Download 0a9b076
Download 47ac827 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 293 2018-12-06T09:30:03+01:00 Download 468d111
Download 15cb940 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 293 2018-12-06T08:49:47+01:00 Download e2addcc
Download 474176d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 293 2018-12-06T08:01:53+01:00 Download 72ac36b
Download e2addcc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 293 2018-12-06T07:31:17+01:00
Download 1f867fc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 293 2018-12-06T07:14:39+01:00 Download 7922326
Download 01f7dfa Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T00:56 CET (sv-comp)
Download 6840329 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-07T14:21 CET (sv-comp)

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

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

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

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

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