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_productSimulator_false-unreach-call_true-termination.cil.c
programSHA f1dff60ce85d3d1cdd786e076ad600021b7bb096cbcce38ce49757ae4e6aa23c
witnessName results-validated/cpa-seq-validate-violation-witnesses-divine-smt.2018-12-08_0324.logfiles/sv-comp19_prop-reachsafety.elevator_spec1_productSimulator_false-unreach-call_true-termination.cil.c.files/witness.graphml
witnessSHA 6a0ac325cff54e64e240231bd207a5cf1116f6aece066839a4219c8cce14031a

Information about the Witness from Competition Database

from https://sv-comp.sosy-lab.org/2019/results/witnessInfoByHash/6a0ac325cff54e64e240231bd207a5cf1116f6aece066839a4219c8cce14031a.json

Key Value
architecture 32bit
creationtime 2018-12-08T04:11:33+01:00
inputwitnesshash 29bfdc98f01eca0b6bba9b1b7d54097f2fdc1ac78dad19bad38bdd3283d77d05
producer CPAchecker 1.7-svn 29852
program-sha256 f1dff60ce85d3d1cdd786e076ad600021b7bb096cbcce38ce49757ae4e6aa23c
programfile ../../sv-benchmarks/c/product-lines/elevator_spec1_productSimulator_false-unreach-call_true-termination.cil.c
programhash f1dff60ce85d3d1cdd786e076ad600021b7bb096cbcce38ce49757ae4e6aa23c
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/6a0ac325cff54e64e240231bd207a5cf1116f6aece066839a4219c8cce14031a.graphml
witness-sha256 6a0ac325cff54e64e240231bd207a5cf1116f6aece066839a4219c8cce14031a
witness-size 230525
witness-type violation_witness

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

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

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

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

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

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download cf60e20 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 2 2019-12-01 08:04:37
Download c35415e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 137 2019-12-03T23:37 CET (comp)
Download 785a0ec Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 229 2019-12-11T22:00:57+01:00 Download 41b598b
Download 661362b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 229 2019-12-11T21:09:42+01:00 Download cf60e20
Download d20ddf6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 262 2019-12-05T20:21:48+01:00 Download 27a9415
Download 7bb6703 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 230 2019-12-04T02:58:08+01:00 Download c35415e
Download e0b4789 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 230 2019-12-03T08:57:11+01:00 Download 7a48622
Download 16133b6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 229 2019-12-03T08:09:35+01:00 Download caccd81
Download caccd81 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 207 2019-11-30T09:17:14+01:00
Download 41b598b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 207 2019-12-01T13:29:24+01:00
Download 875d643 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 351 2019-12-11T20:55:30+01:00 Download b824492
Download 8b2844a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 351 2019-12-08T01:52:43+01:00 Download e855371
Download 4500f64 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 350 2019-12-05T19:34:17+01:00 Download 8b415b0
Download c10edc3 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2019-12-03T22:27 CET (comp)

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download f0255f8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2018-12-08T14:44 CET (sv-comp)
Download c4f9491 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 38 2018-12-07T21:34:42
Download 27a52ff Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 180 2018-12-07T09:15 CET (sv-comp)
Download 0c2fe0e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 264 2018-12-07T10:24:47+01:00
Download 9827811 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 263 2018-12-09T18:21:16+01:00 Download aab68ba
Download 4260b32 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 231 2018-12-08T23:45:16+01:00 Download f0255f8
Download 01736e4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 242 2018-12-08T22:07:42+01:00 Download c4f9491
Download bd3b0cb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 262 2018-12-08T08:01:59+01:00 Download 0c2fe0e
Download 6a0ac32 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 231 2018-12-08T04:11:33+01:00 Download 29bfdc9
Download 3fe191b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 262 2018-12-07T17:45:48+01:00 Download 27a52ff
Download c13f47a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 229 2018-12-06T09:49:20+01:00 Download 57792c8
Download 57792c8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 207 2018-12-05T08:02:31+01:00
Download 814a73f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 351 2018-12-10T20:37:41+01:00 Download 2069968
Download f9922f5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 350 2018-12-08T05:01:39+01:00 Download 3b52bc6
Download 3593fb3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 350 2018-12-06T10:11:46+01:00 Download c465e84
Download e15f4e5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 350 2018-12-06T09:42:50+01:00 Download e66c58c
Download d78891c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 351 2018-12-06T09:16:39+01:00 Download 58b35c1
Download c4132a5 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T01:05 CET (sv-comp)
Download 2ac3c8f Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-07T15:33 CET (sv-comp)

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

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

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

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

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