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_product21_true-unreach-call_true-termination.cil.c
programSHA 4379114f83fa645132491e2251f5e2854ffd85547f7629483b92307082947e0a
witnessName results-verified/pesco.2018-12-06_1244.logfiles/sv-comp19_prop-reachsafety.elevator_spec3_product21_true-unreach-call_true-termination.cil.c.files/witness.graphml
witnessSHA 63882a72aae4d8590a2377f3f84ab48495d4eb6394f7d9330bc660355bc37bcf

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-08T04:14:49+01:00
producer CPAchecker 1.7-svn b8d6131600+
program-sha256 4379114f83fa645132491e2251f5e2854ffd85547f7629483b92307082947e0a
programfile ../../sv-benchmarks/c/product-lines/elevator_spec3_product21_true-unreach-call_true-termination.cil.c
programhash 4379114f83fa645132491e2251f5e2854ffd85547f7629483b92307082947e0a
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/63882a72aae4d8590a2377f3f84ab48495d4eb6394f7d9330bc660355bc37bcf.graphml
witness-sha256 63882a72aae4d8590a2377f3f84ab48495d4eb6394f7d9330bc660355bc37bcf
witness-size 308128
witness-type correctness_witness

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

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

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

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

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

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 08a3321 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2019-12-04T00:17 CET (comp)
Download f3a3b86 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 308 2019-12-11T20:23:09+01:00 Download 08bf41f
Download 9992ced Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 308 2019-12-11T20:07:29+01:00 Download 425f362
Download f32690b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 308 2019-12-11T20:02:32+01:00 Download 9ff54a8
Download ada4ba3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 308 2019-12-08T00:36:26+01:00 Download 83cb82c
Download 97e0956 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 308 2019-12-05T19:21:29+01:00 Download 913c23e
Download 14e9df5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 308 2019-12-05T19:03:19+01:00 Download b8584ef
Download bca109a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 308 2019-12-04T02:07:38+01:00 Download 08a3321
Download 782619b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 308 2019-11-30T19:58:49+01:00 Download 2283cee
Download 3c2de50 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 308 2019-11-30T17:14:38+01:00 Download 2fe3d23
Download 2fe3d23 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / svcomp20 308 2019-11-29T16:10:24+01:00
Download 83cb82c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8 308 2019-12-07T22:28:29+01:00
Download 425f362 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 308 2019-11-30T23:49:55+01:00
Download be96f0d Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2019-12-04T00:59 CET (comp)

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download ee542b5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2018-12-08T06:41 CET (sv-comp)
Download 93b13b2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-08T13:13:13
Download b5afaf9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2018-12-07T09:18 CET (sv-comp)
Download fb20a54 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7 308 2018-12-10T17:14:47+01:00
Download 63882a7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 308 2018-12-08T04:14:49+01:00
Download 46b25fc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 308 2018-12-10T20:06:03+01:00 Download fb20a54
Download 8c0d03f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 308 2018-12-10T10:30:51+01:00 Download ec053a7
Download 8c40606 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 308 2018-12-08T23:10:09+01:00 Download ee542b5
Download 73f9b17 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 308 2018-12-08T21:40:37+01:00 Download 93b13b2
Download ea54204 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 308 2018-12-08T06:54:26+01:00 Download 63882a7
Download fc71206 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 308 2018-12-08T03:31:35+01:00 Download 04e6ab6
Download c77024c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 308 2018-12-08T02:42:42+01:00 Download ec053a7
Download c5d5412 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 308 2018-12-07T16:38:14+01:00 Download b5afaf9
Download a1cf60a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 308 2018-12-06T09:28:28+01:00 Download 6fecc4f
Download 3b2f3ea Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 308 2018-12-06T08:50:25+01:00 Download 0f5297d
Download 06c0c68 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 308 2018-12-06T07:22:33+01:00 Download fa18b9c
Download 0f5297d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 309 2018-12-05T19:16:36+01:00
Download 8ac2484 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T16:38 CET (sv-comp)
Download a62588f Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-07T11:12 CET (sv-comp)

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download d0518ce Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2017-12-02T13:57 CET (sv-comp)
Download 96b2755 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T23:31:27.670394
Download e80b0be Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T09:30:49.109574
Download 7c40ab1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 kind 3 2017-12-02T01:22:51.155214
Download a2d6006 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 incr 3 2017-12-01T08:31:14.569944
Download 2f5688e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 1069 2017-12-01T15:38 CET (sv-comp)
Download e82d8b0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 308 2017-12-03T03:35:50+01:00
Download 2cd0041 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 4 2017-11-30T21:58:56+01:00
Download 6fe6fc5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 308 2017-12-03T04:27:45+01:00 e4737c2
Download 87cd6ca Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 308 2017-12-02T20:02:53+01:00 655bae1
Download 7891c8e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 308 2017-12-02T07:37:28+01:00 c91135a
Download ea63e29 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 308 2017-12-01T22:29:14+01:00 025c57f
Download 687aa07 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 308 2017-12-01T08:14:16+01:00 87f1e37
Download 666c653 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 308 2017-12-01T06:57:26+01:00 13a0284
Download 19ebab0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 308 2017-12-01T06:11:15+01:00 a67a59a
Download bcde2fb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 309 2017-11-30T14:06:10+01:00
Download 87606fd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CBMC 560 2017-11-30T15:07 CET (sv-comp)
Download 76fe1a6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness 2LS 14528 2017-11-30T14:16 CET (sv-comp)
Download f432be0 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 560 2017-12-01T15:10 CET (sv-comp)
Download 3014b8d Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 14532 2017-12-01T14:18 CET (sv-comp)

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

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

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

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