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_product11_true-unreach-call_true-termination.cil.c
programSHA 32dc5fbf0fb25bcdbf1ba45e2dd69f514ed6249b9fcd18e4432afa5bf5873454
witnessName results-validated/cpa-seq-validate-correctness-witnesses-divine-smt.2018-12-08_0145.logfiles/sv-comp19_prop-reachsafety.elevator_spec2_product11_true-unreach-call_true-termination.cil.c.files/witness.graphml
witnessSHA 026d06005b49a0e9997dcd024c5cb4931ad742f8b6fb6fabe56ec69790e47f34

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-08T02:06:49+01:00
inputwitnesshash bfc36ae937e849850faa5fd35647d6eda83a61964fa3a8b7c30ac2dad6f25b4b
producer CPAchecker 1.7-svn 29852
program-sha256 32dc5fbf0fb25bcdbf1ba45e2dd69f514ed6249b9fcd18e4432afa5bf5873454
programfile ../../sv-benchmarks/c/product-lines/elevator_spec2_product11_true-unreach-call_true-termination.cil.c
programhash 32dc5fbf0fb25bcdbf1ba45e2dd69f514ed6249b9fcd18e4432afa5bf5873454
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/026d06005b49a0e9997dcd024c5cb4931ad742f8b6fb6fabe56ec69790e47f34.graphml
witness-sha256 026d06005b49a0e9997dcd024c5cb4931ad742f8b6fb6fabe56ec69790e47f34
witness-size 299576
witness-type correctness_witness

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

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

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

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

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

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 99f24ff Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2019-12-03T22:41 CET (comp)
Download 73484c8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 300 2019-12-11T20:17:30+01:00 Download c5e44c6
Download e98ea8e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 300 2019-12-11T20:09:40+01:00 Download 187679d
Download 7fea08d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 300 2019-12-11T20:02:58+01:00 Download 464a3fa
Download 731af75 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 300 2019-12-08T00:59:38+01:00 Download 63fa62f
Download 7b6f657 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 300 2019-12-05T19:21:07+01:00 Download 67d807c
Download cdae1a6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 300 2019-12-05T19:03:00+01:00 Download 01f39e0
Download 815b210 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 300 2019-12-04T02:07:35+01:00 Download 99f24ff
Download 25acbc6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 300 2019-11-30T19:51:11+01:00 Download bc17f40
Download b555430 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 300 2019-11-30T16:42:18+01:00 Download 9ba514c
Download 9ba514c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / svcomp20 300 2019-11-30T02:27:06+01:00
Download 63fa62f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8 299 2019-12-07T10:38:43+01:00
Download 187679d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 300 2019-12-01T00:34:18+01:00
Download 2d726bc Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2019-12-04T00:40 CET (comp)

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download fe2d7e0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2018-12-08T13:12 CET (sv-comp)
Download ba932a8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-08T05:23:07
Download 587e9b3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2018-12-07T10:54 CET (sv-comp)
Download 91e9b4a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7 299 2018-12-10T17:11:59+01:00
Download a6d8413 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 305 2018-12-07T00:09:31+01:00
Download 0c66260 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 300 2018-12-10T19:44:33+01:00 Download 91e9b4a
Download 8c9b82a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 300 2018-12-10T10:32:00+01:00 Download bfc36ae
Download 36e82fc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 300 2018-12-08T23:24:21+01:00 Download fe2d7e0
Download cf267fa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 300 2018-12-08T21:20:29+01:00 Download ba932a8
Download a2d5f74 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 300 2018-12-08T06:37:29+01:00 Download a6d8413
Download f8c58b5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 300 2018-12-08T04:11:29+01:00 Download 1c2aa7a
Download 026d060 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 300 2018-12-08T02:06:49+01:00 Download bfc36ae
Download 0217d0a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 300 2018-12-07T16:38:31+01:00 Download 587e9b3
Download 4fdf3dc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 300 2018-12-06T09:29:01+01:00 Download 3ff6a54
Download 2c72cdc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 300 2018-12-06T09:00:56+01:00 Download f914937
Download a3efa9b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 300 2018-12-06T07:38:55+01:00 Download 40e9d9c
Download f914937 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 300 2018-12-05T16:01:27+01:00
Download c5e8076 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T03:15 CET (sv-comp)
Download 11006ce Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-07T05:08 CET (sv-comp)

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 032000b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2017-12-02T19:13 CET (sv-comp)
Download 536dd8b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-03T01:44:26.720617
Download dcfcdc7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T11:17:17.030829
Download b7e8c51 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 kind 3 2017-12-02T05:06:35.348372
Download 68db5eb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 incr 3 2017-12-01T10:20:53.000717
Download ff6d140 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 75 2017-12-01T18:21 CET (sv-comp)
Download 5393adc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 308 2017-12-02T22:22:50+01:00
Download ab5ec65 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 4 2017-12-01T02:11:29+01:00
Download c6573fb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 309 2017-12-03T04:27:00+01:00 7b07e48
Download 0fbd1bc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 300 2017-12-02T20:33:32+01:00 27fe993
Download a48dc1a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 300 2017-12-02T09:01:22+01:00 e8d8d99
Download 0fed68c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 300 2017-12-01T22:21:49+01:00 d8fc126
Download 7ee5470 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 300 2017-12-01T08:13:00+01:00 0c6479a
Download 006f40a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 300 2017-12-01T06:50:58+01:00 f0cfb8d
Download da07196 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 300 2017-12-01T05:14:15+01:00 ba8d989
Download 97adb4c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 300 2017-11-30T22:40:51+01:00
Download a361b64 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CBMC 220 2017-11-30T19:52 CET (sv-comp)
Download c750e4f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness 2LS 10563 2017-11-30T14:01 CET (sv-comp)
Download 9e41bd2 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 220 2017-12-01T13:11 CET (sv-comp)
Download 7f6bb4e Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 3471 2017-12-01T14:23 CET (sv-comp)

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

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

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

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