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_spec14_productSimulator_false-unreach-call_true-termination.cil.c
programSHA 7eee793f7a2714e33873bd4efff34a67e47494b24555ebf72081bf0380d68a7a
witnessName results-verified/cpa-seq.2018-12-05_0546.logfiles/sv-comp19_prop-reachsafety.elevator_spec14_productSimulator_false-unreach-call_true-termination.cil.c.files/witness.graphml
witnessSHA 960731bd8f87379314164af072aa3ab2720fd1c13813b748c59573e9be5588f6

Information about the Witness from Competition Database

from https://sv-comp.sosy-lab.org/2019/results/witnessInfoByHash/960731bd8f87379314164af072aa3ab2720fd1c13813b748c59573e9be5588f6.json

Key Value
architecture 32bit
creationtime 2018-12-05T16:12:55+01:00
producer CPAchecker 1.7-svn 29852
program-sha256 7eee793f7a2714e33873bd4efff34a67e47494b24555ebf72081bf0380d68a7a
programfile ../../sv-benchmarks/c/product-lines/elevator_spec14_productSimulator_false-unreach-call_true-termination.cil.c
programhash 7eee793f7a2714e33873bd4efff34a67e47494b24555ebf72081bf0380d68a7a
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/960731bd8f87379314164af072aa3ab2720fd1c13813b748c59573e9be5588f6.graphml
witness-sha256 960731bd8f87379314164af072aa3ab2720fd1c13813b748c59573e9be5588f6
witness-size 194498
witness-type violation_witness

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

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

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

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

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

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download ea3a405 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 2 2019-12-02 05:56:39
Download a2b45fa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 128 2019-12-04T00:14 CET (comp)
Download 2f77695 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 216 2019-12-11T21:54:57+01:00 Download 37bc391
Download 48e1411 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 216 2019-12-11T21:09:11+01:00 Download ea3a405
Download 0fddd22 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 229 2019-12-11T20:44:55+01:00 Download bbca9b6
Download 24444ad Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 216 2019-12-04T02:58:27+01:00 Download a2b45fa
Download 3d03d13 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 217 2019-12-03T08:57:39+01:00 Download aa8f63e
Download b192bb5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 216 2019-12-03T08:09:43+01:00 Download ac05d13
Download ac05d13 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 194 2019-11-29T14:22:34+01:00
Download 37bc391 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 194 2019-12-01T00:39:17+01:00
Download 72de075 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 334 2019-12-11T20:54:58+01:00 Download 388e771
Download f167f7a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 334 2019-12-05T20:21:36+01:00 Download 3e91892
Download df1f54b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 334 2019-12-05T19:34:20+01:00 Download 968b14c
Download 0e292a5 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2019-12-03T22:06 CET (comp)

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 01a3015 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2018-12-08T00:27 CET (sv-comp)
Download 24015bf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 31 2018-12-08T04:58:22
Download dcca10f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 155 2018-12-06T23:17 CET (sv-comp)
Download 58bd578 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 222 2018-12-08T03:38:31+01:00
Download 0bb5f7d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 229 2018-12-09T18:13:43+01:00 Download d344f79
Download c48175b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 217 2018-12-08T23:44:56+01:00 Download 01a3015
Download 1427a04 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 216 2018-12-08T22:09:22+01:00 Download 24015bf
Download f49ff9b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 216 2018-12-08T07:44:07+01:00 Download 58bd578
Download d63ae5f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 217 2018-12-08T04:34:16+01:00 Download 111e113
Download d2d0b71 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 229 2018-12-07T17:44:51+01:00 Download dcca10f
Download 149fa13 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 216 2018-12-06T09:48:41+01:00 Download 960731b
Download 960731b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 194 2018-12-05T16:12:55+01:00
Download 947e465 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 334 2018-12-08T05:02:00+01:00 Download 36c930c
Download 1bc13a8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 334 2018-12-06T10:13:24+01:00 Download 3640790
Download 8b432ea Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 334 2018-12-06T09:41:39+01:00 Download 210de3e
Download 1b34cd7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 334 2018-12-06T09:20:00+01:00 Download 9233dfc
Download 2dd23ea Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 334 2018-12-06T09:00:18+01:00 Download 3fc8b1e
Download b2d5889 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T10:01 CET (sv-comp)
Download 01416b5 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-07T10:29 CET (sv-comp)

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

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

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

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

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