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_spec9_product26_false-unreach-call_true-termination.cil.c
programSHA 18e36e8a88c791c6f4510123f568cb314c5ea32debde244d04812c609ac53e42
witnessName results-validated/cpa-seq-validate-violation-witnesses-divine-explicit.2018-12-10_1048.logfiles/sv-comp19_prop-reachsafety.elevator_spec9_product26_false-unreach-call_true-termination.cil.c.files/witness.graphml
witnessSHA 3ae201dfdd87b27768ff0cebf3388f1de97630cb58e89bcf7f59bc75f826b3f3

Information about the Witness from Competition Database

from https://sv-comp.sosy-lab.org/2019/results/witnessInfoByHash/3ae201dfdd87b27768ff0cebf3388f1de97630cb58e89bcf7f59bc75f826b3f3.json

Key Value
architecture 32bit
creationtime 2018-12-10T10:48:42+01:00
inputwitnesshash eda0f6cb5952b0907a937ae1689251623212c5c450b18092b4b9652e8604f806
producer CPAchecker 1.7-svn 29852
program-sha256 18e36e8a88c791c6f4510123f568cb314c5ea32debde244d04812c609ac53e42
programfile ../../sv-benchmarks/c/product-lines/elevator_spec9_product26_false-unreach-call_true-termination.cil.c
programhash 18e36e8a88c791c6f4510123f568cb314c5ea32debde244d04812c609ac53e42
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/3ae201dfdd87b27768ff0cebf3388f1de97630cb58e89bcf7f59bc75f826b3f3.graphml
witness-sha256 3ae201dfdd87b27768ff0cebf3388f1de97630cb58e89bcf7f59bc75f826b3f3
witness-size 209182
witness-type violation_witness

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

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

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

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

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

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 1a14ca7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2019-12-01 03:21:13
Download c073d24 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 118 2019-12-04T00:51 CET (comp)
Download 9af4f84 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 209 2019-12-11T21:41:49+01:00 Download 7f8830c
Download 70c63c0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 210 2019-12-11T21:09:43+01:00 Download 1a14ca7
Download 826314d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 209 2019-12-11T20:54:24+01:00 Download 30d406c
Download 6aa5115 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 210 2019-12-11T20:44:38+01:00 Download b08aeb3
Download 2b63feb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 209 2019-12-04T02:58:06+01:00 Download c073d24
Download 76979d2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 209 2019-12-03T08:57:41+01:00 Download ec17d06
Download 534da3e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 209 2019-12-03T08:10:37+01:00 Download b9bb936
Download b9bb936 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 192 2019-11-29T20:07:40+01:00
Download 7f8830c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 209 2019-12-01T07:35:14+01:00
Download 8a50607 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 302 2019-12-08T01:51:49+01:00 Download 8f2c16f
Download 7fd8b21 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 302 2019-12-05T20:20:30+01:00 Download f1c9c6e
Download b3914f1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 302 2019-12-05T19:34:43+01:00 Download 2728d82
Download 9441f65 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2019-12-03T23:55 CET (comp)

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 5987728 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2018-12-08T05:25 CET (sv-comp)
Download 73d4c08 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 30 2018-12-08T10:57:38
Download f50996f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 134 2018-12-07T09:47 CET (sv-comp)
Download 053b1d9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 216 2018-12-08T03:07:35+01:00
Download 3ae201d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 209 2018-12-10T10:48:42+01:00 Download eda0f6c
Download 8bbd991 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 210 2018-12-09T18:20:45+01:00 Download 43a1a95
Download 77fbbc9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 209 2018-12-08T23:44:08+01:00 Download 5987728
Download 2610060 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 145 2018-12-08T22:11:23+01:00 Download 73d4c08
Download 7dff0ca Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 209 2018-12-08T08:04:17+01:00 Download 053b1d9
Download 1fe9926 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 209 2018-12-08T05:06:02+01:00 Download ab26634
Download c6329cf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 209 2018-12-08T03:42:36+01:00 Download eda0f6c
Download 800fc79 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 209 2018-12-07T17:45:31+01:00 Download f50996f
Download ae47d0f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 209 2018-12-06T10:18:22+01:00 Download e5d507a
Download 2061736 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 209 2018-12-06T09:49:13+01:00 Download 7e09914
Download 7e09914 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 192 2018-12-05T13:31:48+01:00
Download 4eb1fc0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 302 2018-12-10T20:37:22+01:00 Download b8022e4
Download a4d45fc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 302 2018-12-06T09:40:36+01:00 Download f0d8935
Download 8763a15 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 302 2018-12-06T09:20:32+01:00 Download a05a9fb
Download 2de3950 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 302 2018-12-06T09:18:04+01:00 Download 0fc8327
Download 96c8a88 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T05:21 CET (sv-comp)
Download 8db51a4 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-07T02:57 CET (sv-comp)

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

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

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

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

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