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_product28_false-unreach-call_true-termination.cil.c
programSHA 11186cbd1b390b6e08e592bd8e3dfa24fcdaf5b1241ffca70bb1eac61930a26c
witnessName results-validated/cpa-seq-validate-violation-witnesses-pesco.2018-12-08_0739.logfiles/sv-comp19_prop-reachsafety.elevator_spec14_product28_false-unreach-call_true-termination.cil.c.files/witness.graphml
witnessSHA 518bc08b51c5a2b0abd6bc1ee9c104ee49377a02ff3d197aa27cd7df1ec3a759

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-08T08:20:04+01:00
inputwitnesshash 355048e7fb23d838175f51f059c0ddba74579beed4d6f4755d7112cfe019b96d
producer CPAchecker 1.7-svn 29852
program-sha256 11186cbd1b390b6e08e592bd8e3dfa24fcdaf5b1241ffca70bb1eac61930a26c
programfile ../../sv-benchmarks/c/product-lines/elevator_spec14_product28_false-unreach-call_true-termination.cil.c
programhash 11186cbd1b390b6e08e592bd8e3dfa24fcdaf5b1241ffca70bb1eac61930a26c
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/518bc08b51c5a2b0abd6bc1ee9c104ee49377a02ff3d197aa27cd7df1ec3a759.graphml
witness-sha256 518bc08b51c5a2b0abd6bc1ee9c104ee49377a02ff3d197aa27cd7df1ec3a759
witness-size 190336
witness-type violation_witness

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

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

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

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

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

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download a996d87 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2019-12-01 10:08:52
Download 6de61a8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 106 2019-12-03T22:43 CET (comp)
Download 6d52333 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 190 2019-12-11T21:39:38+01:00 Download 69c5aad
Download eb02ca0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 191 2019-12-11T21:09:48+01:00 Download a996d87
Download 40fe5a0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 190 2019-12-11T20:54:22+01:00 Download 2636f94
Download 567633b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 191 2019-12-11T20:44:27+01:00 Download 0be8049
Download 4459b69 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 190 2019-12-08T01:52:22+01:00 Download 6fd8c3b
Download 95e5645 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 190 2019-12-04T02:58:26+01:00 Download 6de61a8
Download e42483a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 190 2019-12-03T08:57:18+01:00 Download 508b548
Download 5d01a91 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 190 2019-12-03T08:02:47+01:00 Download d136221
Download d136221 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 174 2019-11-29T17:35:25+01:00
Download 6fd8c3b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8 193 2019-12-07T14:43:57+01:00
Download 69c5aad Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 190 2019-11-30T23:33:50+01:00
Download 3ad1783 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 296 2019-12-05T20:20:16+01:00 Download a90be4c
Download e09344a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 296 2019-12-05T19:34:08+01:00 Download 9f9e1e7
Download 4feb0a3 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2019-12-03T22:05 CET (comp)

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 5b22032 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2018-12-08T05:29 CET (sv-comp)
Download 5661daf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 26 2018-12-08T08:46:52
Download a6c5b3e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 121 2018-12-07T13:27 CET (sv-comp)
Download 5f9fb17 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7 175 2018-12-10T17:50:00+01:00
Download 355048e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 180 2018-12-06T13:22:27+01:00
Download 97161b9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 190 2018-12-10T20:36:38+01:00 Download 5f9fb17
Download 759e5ce Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 190 2018-12-10T10:48:53+01:00 Download 3ec705b
Download 9084892 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 191 2018-12-09T18:21:40+01:00 Download c0eb404
Download b6f87b6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 190 2018-12-08T23:44:49+01:00 Download 5b22032
Download 8e31b40 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 137 2018-12-08T22:08:48+01:00 Download 5661daf
Download 518bc08 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 190 2018-12-08T08:20:04+01:00 Download 355048e
Download 09fcd8c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 190 2018-12-08T05:00:22+01:00 Download 753cd08
Download 070212b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 190 2018-12-08T04:10:21+01:00 Download 3ec705b
Download b2754ac Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 190 2018-12-07T17:43:29+01:00 Download a6c5b3e
Download f38a39e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 190 2018-12-06T10:19:49+01:00 Download 8576d1d
Download 7ea5334 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 190 2018-12-06T09:47:57+01:00 Download 1e265ea
Download 1e265ea Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 174 2018-12-06T07:15:11+01:00
Download 7bceb52 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 296 2018-12-06T09:41:20+01:00 Download 57698f5
Download 250b686 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 296 2018-12-06T09:17:48+01:00 Download e4d9beb
Download deff511 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 296 2018-12-06T09:16:49+01:00 Download 1dca77f
Download b37e42e Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T12:23 CET (sv-comp)
Download 61b30f3 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-07T09:54 CET (sv-comp)

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

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

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

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

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