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_spec3_product20_false-unreach-call_true-termination.cil.c
programSHA cdefed6ba27d324d00adcbb0e21da39935083e1b3ffc71bef5fccf6629c2a3ea
witnessName results-verified/cpa-seq.2018-12-05_0546.logfiles/sv-comp19_prop-reachsafety.elevator_spec3_product20_false-unreach-call_true-termination.cil.c.files/witness.graphml
witnessSHA a81591585745d3d627ecf10cefd89fac69f5c7fa7320f2b7ddbb010db85d003c

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-06T03:32:43+01:00
producer CPAchecker 1.7-svn 29852
program-sha256 cdefed6ba27d324d00adcbb0e21da39935083e1b3ffc71bef5fccf6629c2a3ea
programfile ../../sv-benchmarks/c/product-lines/elevator_spec3_product20_false-unreach-call_true-termination.cil.c
programhash cdefed6ba27d324d00adcbb0e21da39935083e1b3ffc71bef5fccf6629c2a3ea
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/a81591585745d3d627ecf10cefd89fac69f5c7fa7320f2b7ddbb010db85d003c.graphml
witness-sha256 a81591585745d3d627ecf10cefd89fac69f5c7fa7320f2b7ddbb010db85d003c
witness-size 291427
witness-type violation_witness

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

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

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

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

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

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 7ab6299 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2019-12-01 16:21:02
Download d5d1782 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 189 2019-12-03T22:45 CET (comp)
Download 2f508d2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 328 2019-12-11T21:56:56+01:00 Download 7212133
Download 9088fb9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 329 2019-12-11T21:09:11+01:00 Download 7ab6299
Download a9652aa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 328 2019-12-11T20:54:58+01:00 Download e6c1379
Download 4ed0023 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 329 2019-12-11T20:44:36+01:00 Download 136271a
Download 2a95025 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 328 2019-12-08T01:51:35+01:00 Download 6e447b0
Download 3042cb3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 328 2019-12-04T02:58:27+01:00 Download d5d1782
Download e186326 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 328 2019-12-03T08:57:59+01:00 Download c4c4a7b
Download 47fe70f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 328 2019-12-03T08:09:04+01:00 Download 771a9bc
Download 771a9bc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 291 2019-11-29T23:45:39+01:00
Download 6e447b0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8 331 2019-12-07T19:32:13+01:00
Download 7212133 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 328 2019-11-30T22:46:26+01:00
Download 041eea6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 310 2019-12-05T20:20:25+01:00 Download ba893b3
Download 1d19a15 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 310 2019-12-05T19:34:05+01:00 Download 42ce17a
Download 07433da Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2019-12-04T00:38 CET (comp)

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 7f7d227 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2018-12-08T07:09 CET (sv-comp)
Download 8ba8f76 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 57 2018-12-08T14:03:33
Download 846c146 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 215 2018-12-07T10:31 CET (sv-comp)
Download a332e2f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7 302 2018-12-10T17:41:20+01:00
Download 8f4480c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 330 2018-12-07T12:55:56+01:00
Download 7b0c665 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 328 2018-12-10T20:38:16+01:00 Download a332e2f
Download 79a7ec5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 328 2018-12-10T10:48:50+01:00 Download 043bcbb
Download 7e0522b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 329 2018-12-09T18:20:41+01:00 Download 05366af
Download d100267 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 328 2018-12-08T23:42:19+01:00 Download 7f7d227
Download a73ec18 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 208 2018-12-08T22:10:25+01:00 Download 8ba8f76
Download 14dd2b4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 328 2018-12-08T08:54:22+01:00 Download 8f4480c
Download 54e4043 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 328 2018-12-08T05:03:25+01:00 Download a31d1be
Download 9ceb70d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 328 2018-12-08T03:40:13+01:00 Download 043bcbb
Download 0cb389c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 328 2018-12-07T17:14:18+01:00 Download 846c146
Download c4d9150 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 328 2018-12-06T10:17:57+01:00 Download 9364da4
Download 5c6bf3c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 328 2018-12-06T09:48:00+01:00 Download a815915
Download a815915 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 291 2018-12-06T03:32:43+01:00
Download 95957b3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 310 2018-12-06T09:42:48+01:00 Download faa0e2f
Download 0d5b075 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 310 2018-12-06T09:17:15+01:00 Download 1b4d3b5
Download 3f68339 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 310 2018-12-06T09:00:47+01:00 Download af8ac0c
Download fabe16b Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T04:31 CET (sv-comp)
Download 01cb1b5 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-07T12:07 CET (sv-comp)

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download c9c5d01 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2017-12-02T17:07 CET (sv-comp)
Download 0af2472 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 4 2017-12-01T21:44:15.796099
Download e6c92d1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 4 2017-12-01T16:40:34.551615
Download c7e70c9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 99 2017-12-01T18:26 CET (sv-comp)
Download 92d7cdb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 99 2017-12-01T00:53 CET (sv-comp)
Download 545d0ac Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 261 2017-11-30T21:50:17+01:00
Download 227eb3b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 175 2017-11-30T16:09 CET (sv-comp)
Download dc3afd9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness 2LS 202 2017-11-30T18:48 CET (sv-comp)
Download a960afc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-03T00:22:32.671284
Download c6eec8d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T14:51:19.735020
Download 5021cac Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 239 2017-12-01T16:33 CET (sv-comp)

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

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

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

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