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_spec2_product22_false-unreach-call_true-termination.cil.c
programSHA 8995889333d118f6e8c410def59548c89655c232ac0f500d438237cd4f69ec1c
witnessName results-validated/cpa-seq-validate-violation-witnesses-veriabs.2018-12-10_2034.logfiles/sv-comp19_prop-reachsafety.elevator_spec2_product22_false-unreach-call_true-termination.cil.c.files/witness.graphml
witnessSHA ac7a998605f333b5e15e4bc552d6db92828057d956a37ef0ad2d13674c7cda45

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-10T20:37:46+01:00
inputwitnesshash 674bba293589f0b30d475f309180bbf19c1751414d3d33b8e2ce9a93cf95c147
producer CPAchecker 1.7-svn 29852
program-sha256 8995889333d118f6e8c410def59548c89655c232ac0f500d438237cd4f69ec1c
programfile ../../sv-benchmarks/c/product-lines/elevator_spec2_product22_false-unreach-call_true-termination.cil.c
programhash 8995889333d118f6e8c410def59548c89655c232ac0f500d438237cd4f69ec1c
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/ac7a998605f333b5e15e4bc552d6db92828057d956a37ef0ad2d13674c7cda45.graphml
witness-sha256 ac7a998605f333b5e15e4bc552d6db92828057d956a37ef0ad2d13674c7cda45
witness-size 202555
witness-type violation_witness

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

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

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

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

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

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 2988cb5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2019-12-01 20:56:35
Download 94a3af9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 115 2019-12-03T21:44 CET (comp)
Download c11175b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 203 2019-12-11T21:50:06+01:00 Download 820d956
Download f547869 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 203 2019-12-11T21:09:05+01:00 Download 2988cb5
Download f7822e4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 203 2019-12-11T20:55:08+01:00 Download 2c1dcd7
Download 9ff88fa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 203 2019-12-11T20:44:40+01:00 Download f465497
Download 3e26378 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 203 2019-12-04T02:58:26+01:00 Download 94a3af9
Download e61341d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 203 2019-12-03T08:57:00+01:00 Download 4fd50cc
Download 0f33d43 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 203 2019-12-03T08:08:12+01:00 Download ff2aca7
Download ff2aca7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 187 2019-11-29T21:56:36+01:00
Download 820d956 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 202 2019-12-01T08:39:33+01:00
Download 9a72150 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 308 2019-12-08T01:52:28+01:00 Download 338a7d2
Download f1e6edf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 308 2019-12-05T20:21:03+01:00 Download 8fa92f9
Download 36f2e0f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 308 2019-12-05T19:34:08+01:00 Download b8ac565
Download 1d66009 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2019-12-04T00:04 CET (comp)

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 8d8ebea Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2018-12-08T07:49 CET (sv-comp)
Download 30e156d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 30 2018-12-08T07:45:17
Download 9fb6334 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 130 2018-12-07T03:04 CET (sv-comp)
Download 674bba2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7 186 2018-12-10T17:49:07+01:00
Download a331375 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 204 2018-12-06T20:07:28+01:00
Download ac7a998 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 203 2018-12-10T20:37:46+01:00 Download 674bba2
Download 0c0b0f2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 203 2018-12-10T10:48:44+01:00 Download 3c8ed4e
Download 9a2d3e5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 204 2018-12-09T18:21:34+01:00 Download dcdd1c5
Download 7aeaeb1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 203 2018-12-08T23:43:13+01:00 Download 8d8ebea
Download 9ec1c3b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 140 2018-12-08T22:07:37+01:00 Download 30e156d
Download 96a5295 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 203 2018-12-08T09:02:15+01:00 Download a331375
Download a2232c4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 203 2018-12-08T05:02:19+01:00 Download a3719f8
Download 4aab71b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 203 2018-12-08T04:35:58+01:00 Download 3c8ed4e
Download 3a272b8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 203 2018-12-07T17:44:12+01:00 Download 9fb6334
Download d8cc82d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 203 2018-12-06T10:20:13+01:00 Download fc3a6f4
Download cf39b45 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 203 2018-12-06T09:49:05+01:00 Download c7f81c9
Download c7f81c9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 187 2018-12-05T12:56:17+01:00
Download cd075d9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 308 2018-12-06T09:41:32+01:00 Download a079e2d
Download 7fccb2c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 308 2018-12-06T09:12:14+01:00 Download 2a25cfa
Download 177d4f2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 308 2018-12-06T09:00:31+01:00 Download 7c2ced5
Download 1fcd2ff Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T08:53 CET (sv-comp)
Download 00a687f Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-07T07:46 CET (sv-comp)

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

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

Found 12 witnesses for program sv-benchmarks/c/product-lines/elevator_spec2_product22_false-unreach-call_true-termination.cil.c, 8995889333d118f6e8c410def59548c89655c232ac0f500d438237cd4f69ec1c
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/8995889333d118f6e8c410def59548c89655c232ac0f500d438237cd4f69ec1c.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 5463193 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2017-12-02T19:05 CET (sv-comp)
Download f5398d5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 4 2017-12-01T16:00:49.542424
Download 95fbda6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 4 2017-12-01T11:27:01.655607
Download b1b8b65 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 60 2017-12-01T19:53 CET (sv-comp)
Download 463213d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 60 2017-12-01T07:21 CET (sv-comp)
Download bfd95e4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 166 2017-11-30T14:17:31+01:00
Download 4fc2c5f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 106 2017-11-30T16:47 CET (sv-comp)
Download e7f510b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness 2LS 122 2017-11-30T12:31 CET (sv-comp)
Download 464653f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-03T00:26:11.886802
Download a08c24e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T15:55:57.350880
Download 71c35bf Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 98 2017-12-01T18:07 CET (sv-comp)
Download e1f22f2 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 11363 2017-12-01T12:40 CET (sv-comp)

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

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

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

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