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_product24_false-unreach-call_true-termination.cil.c
programSHA 7784c714ef470aa5e5bb76f1077834ca7868c83d5de9c96f784d85127086dbc8
witnessName results-validated/cpa-seq-validate-violation-witnesses-cbmc.2018-12-06_0859.logfiles/sv-comp19_prop-reachsafety.elevator_spec14_product24_false-unreach-call_true-termination.cil.c.files/witness.graphml
witnessSHA 16b00972aa24dfaa8bb9e2cf5036d7f810cdabd6034b5066727e4ddcd78b06e7

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-06T09:17:48+01:00
inputwitnesshash 9ed067bc931905e704f185135a488382f6983fd9551d93cb485c7660ae932faa
producer CPAchecker 1.7-svn 29852
program-sha256 7784c714ef470aa5e5bb76f1077834ca7868c83d5de9c96f784d85127086dbc8
programfile ../../sv-benchmarks/c/product-lines/elevator_spec14_product24_false-unreach-call_true-termination.cil.c
programhash 7784c714ef470aa5e5bb76f1077834ca7868c83d5de9c96f784d85127086dbc8
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/16b00972aa24dfaa8bb9e2cf5036d7f810cdabd6034b5066727e4ddcd78b06e7.graphml
witness-sha256 16b00972aa24dfaa8bb9e2cf5036d7f810cdabd6034b5066727e4ddcd78b06e7
witness-size 300001
witness-type correctness_witness

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

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

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

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

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

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download f6b06e1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2019-12-02 03:51:41
Download 98d97d8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 115 2019-12-04T00:28 CET (comp)
Download 21e4456 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 203 2019-12-11T21:58:28+01:00 Download e918d9f
Download 879d86f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 204 2019-12-11T21:09:06+01:00 Download f6b06e1
Download e7ee081 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 203 2019-12-11T20:55:00+01:00 Download 1704086
Download eecc514 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 204 2019-12-11T20:44:50+01:00 Download 266906b
Download d476e05 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 203 2019-12-08T01:51:49+01:00 Download d806a5c
Download 7012445 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 203 2019-12-04T02:58:31+01:00 Download 98d97d8
Download 3dccaba Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 203 2019-12-03T08:57:03+01:00 Download e48a440
Download e4e36e7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 203 2019-12-03T08:10:14+01:00 Download f4a2ac5
Download f4a2ac5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 186 2019-11-30T12:17:13+01:00
Download d806a5c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8 206 2019-12-07T13:22:00+01:00
Download e918d9f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 186 2019-12-01T00:52:53+01:00
Download ec3867a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 300 2019-12-05T20:21:55+01:00 Download 3a14246
Download 7b11620 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 300 2019-12-05T19:34:08+01:00 Download c608485
Download c3719c4 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2019-12-04T01:29 CET (comp)

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download d696f9c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2018-12-08T01:54 CET (sv-comp)
Download 6a28c67 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 29 2018-12-08T01:58:49
Download 68d3e13 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 130 2018-12-07T01:29 CET (sv-comp)
Download ced1e65 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7 186 2018-12-10T18:03:07+01:00
Download d43b990 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 209 2018-12-07T10:59:11+01:00
Download 3d837c2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 203 2018-12-10T20:34:53+01:00 Download ced1e65
Download 2bdcb7e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 203 2018-12-10T10:48:50+01:00 Download 850565c
Download bbd69fa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 204 2018-12-09T18:19:58+01:00 Download c01c7ee
Download 187f242 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 203 2018-12-08T23:43:34+01:00 Download d696f9c
Download dff7a31 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 143 2018-12-08T22:10:37+01:00 Download 6a28c67
Download fb75c6f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 203 2018-12-08T08:25:40+01:00 Download d43b990
Download 0df14fd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 203 2018-12-08T04:56:06+01:00 Download 52c6a8a
Download 1db132d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 203 2018-12-08T04:36:47+01:00 Download 850565c
Download 71e34c6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 203 2018-12-07T17:45:28+01:00 Download 68d3e13
Download b94a416 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 203 2018-12-06T10:20:11+01:00 Download 9b1b9c2
Download 2191088 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 203 2018-12-06T09:49:10+01:00 Download f638cad
Download f638cad Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 186 2018-12-06T03:42:58+01:00
Download f24bbad Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 300 2018-12-06T09:40:40+01:00 Download 8f48c40
Download 16b0097 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 300 2018-12-06T09:17:48+01:00 Download 9ed067b
Download 62696a6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 300 2018-12-06T09:00:50+01:00 Download 3d1360b
Download 7c43cfe Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T16:17 CET (sv-comp)
Download f815fa5 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-06T23:59 CET (sv-comp)

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

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

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

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

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