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_product01_true-unreach-call_true-termination.cil.c
programSHA 7ed3a19276277d834a0976c5443bf69eb4f172a09d82404852bb2068c838115b
witnessName results-verified/esbmc-kind.2018-12-06_1103.logfiles/sv-comp19_prop-reachsafety.elevator_spec2_product01_true-unreach-call_true-termination.cil.c.files/witness.graphml
witnessSHA 49091f602a6816844c14a10ba38fa6d4e59c8518094cae9fc41ac49a293c362d

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-07T23:52:33.752477
producer ESBMC 6.0.0 kind
programfile ../../sv-benchmarks/c/product-lines/elevator_spec2_product01_true-unreach-call_true-termination.cil.c
programhash 765eea1d747655d15d06f685c945a710ffef8473
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/49091f602a6816844c14a10ba38fa6d4e59c8518094cae9fc41ac49a293c362d.graphml
witness-sha256 49091f602a6816844c14a10ba38fa6d4e59c8518094cae9fc41ac49a293c362d
witness-size 3433
witness-type correctness_witness

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

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

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

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

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 3d04add Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2019-12-03T23:21 CET (comp)
Download 6b88b0d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 285 2019-12-11T20:22:59+01:00 Download 37d1e0c
Download 1b0cec7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 285 2019-12-11T20:17:27+01:00 Download e1490d6
Download 8ca64e6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 285 2019-12-11T20:02:22+01:00 Download 5c428e1
Download 4ea4515 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 285 2019-12-08T01:00:42+01:00 Download 2eb9d5a
Download 36bc5ea Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 285 2019-12-05T19:16:04+01:00 Download 6f86d47
Download 2c38a7b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 285 2019-12-05T19:03:03+01:00 Download 0e35b68
Download bab8d47 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 285 2019-12-04T02:07:46+01:00 Download 3d04add
Download 106892a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 285 2019-11-30T19:22:48+01:00 Download 3fede0d
Download 2cf8981 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 285 2019-11-30T16:42:14+01:00 Download ccab7f0
Download ccab7f0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / svcomp20 286 2019-11-29T20:13:48+01:00
Download 2eb9d5a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8 285 2019-12-07T22:23:22+01:00
Download e1490d6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 286 2019-12-01T01:35:11+01:00
Download 4916bca Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2019-12-04T00:07 CET (comp)

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download ce4240d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2018-12-07T23:31 CET (sv-comp)
Download ca4bc76 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-07T23:02:30
Download 1b44e7c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2018-12-07T01:01 CET (sv-comp)
Download 55ff0f0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7 285 2018-12-10T18:53:35+01:00
Download 9052505 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 295 2018-12-06T13:15:12+01:00
Download 0bc8999 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 285 2018-12-10T20:17:15+01:00 Download 55ff0f0
Download 01490e7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 285 2018-12-10T10:31:48+01:00 Download 85b9206
Download 79d1510 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 285 2018-12-08T23:15:39+01:00 Download ce4240d
Download 55e824e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 285 2018-12-08T21:12:40+01:00 Download ca4bc76
Download 627802a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 292 2018-12-08T07:05:51+01:00 Download 9052505
Download 2b3eb0e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 285 2018-12-08T02:40:34+01:00 Download 49091f6
Download 779410f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 285 2018-12-08T02:38:16+01:00 Download 85b9206
Download 7940194 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 285 2018-12-07T16:39:02+01:00 Download 1b44e7c
Download 1644d46 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 285 2018-12-06T09:28:42+01:00 Download cb56af3
Download d4b9939 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 285 2018-12-06T08:45:50+01:00 Download 5c82161
Download c3e2648 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 285 2018-12-06T07:45:35+01:00 Download 8b25794
Download 20ddb5b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 285 2018-12-06T07:22:19+01:00 Download 9c88844
Download 5c82161 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 286 2018-12-06T00:02:17+01:00
Download 6ed1f6a Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T13:09 CET (sv-comp)
Download 1042dbe Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-07T14:45 CET (sv-comp)

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

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

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

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

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