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_product21_true-unreach-call_true-termination.cil.c
programSHA 49c44ceadb5b8fb7e656a2b78aa85f0e414e791c35003e2e0df7aa9806447668
witnessName results-verified/pinaka.2018-12-06_2014.logfiles/sv-comp19_prop-reachsafety.elevator_spec2_product21_true-unreach-call_true-termination.cil.c.files/witness.graphml
witnessSHA 3639baaadb4d152c704090b20458f2428ab65b24d9643aa80f9e745372267c47

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-07T02:57 CET (sv-comp)
producer Pinaka
program-sha256 49c44ceadb5b8fb7e656a2b78aa85f0e414e791c35003e2e0df7aa9806447668
programfile ../../sv-benchmarks/c/product-lines/elevator_spec2_product21_true-unreach-call_true-termination.cil.c
programhash 49c44ceadb5b8fb7e656a2b78aa85f0e414e791c35003e2e0df7aa9806447668
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/3639baaadb4d152c704090b20458f2428ab65b24d9643aa80f9e745372267c47.graphml
witness-sha256 3639baaadb4d152c704090b20458f2428ab65b24d9643aa80f9e745372267c47
witness-size 3222
witness-type correctness_witness

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

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

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

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

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

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download ae96b09 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2019-12-03T22:50 CET (comp)
Download c38c83c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 304 2019-12-11T20:15:29+01:00 Download 1e09e71
Download 5c452bb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 304 2019-12-11T20:09:17+01:00 Download 8b7da43
Download 1be0f44 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 304 2019-12-11T20:02:34+01:00 Download b8014d9
Download bd84164 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 304 2019-12-08T00:36:23+01:00 Download 5091fac
Download 57f8731 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 304 2019-12-05T19:20:57+01:00 Download f4b2d38
Download 97a1660 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 304 2019-12-05T19:03:03+01:00 Download 39b9868
Download af787de Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 304 2019-12-04T02:07:55+01:00 Download ae96b09
Download d8e9007 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 304 2019-11-30T19:03:04+01:00 Download 8e3f920
Download fbcd7bf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 304 2019-11-30T17:15:29+01:00 Download ac062f9
Download ac062f9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / svcomp20 305 2019-11-29T23:45:52+01:00
Download 5091fac Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8 304 2019-12-07T12:20:13+01:00
Download 8b7da43 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 305 2019-12-01T00:16:38+01:00
Download 1539761 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2019-12-03T22:30 CET (comp)

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 63db3f6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2018-12-08T09:12 CET (sv-comp)
Download b80e5d0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-08T06:30:12
Download 3639baa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2018-12-07T02:57 CET (sv-comp)
Download 97ee7ba Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7 304 2018-12-10T18:23:16+01:00
Download fd600a8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 314 2018-12-07T10:37:50+01:00
Download c915170 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 304 2018-12-10T20:08:32+01:00 Download 97ee7ba
Download ff8d2bf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 304 2018-12-10T10:31:10+01:00 Download a57a979
Download a8b8717 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 304 2018-12-08T23:11:14+01:00 Download 63db3f6
Download 5e4620c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 304 2018-12-08T21:30:09+01:00 Download b80e5d0
Download 32af290 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 311 2018-12-08T05:15:25+01:00 Download fd600a8
Download b805c41 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 304 2018-12-08T03:08:51+01:00 Download 0b8a811
Download 6d2f190 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 304 2018-12-08T02:15:24+01:00 Download a57a979
Download 3cc7f5f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 304 2018-12-07T16:39:23+01:00 Download 3639baa
Download 06dc962 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 304 2018-12-06T09:28:59+01:00 Download 60e58cf
Download 67deec8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 304 2018-12-06T09:16:03+01:00 Download 3535c05
Download 23d6f34 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 304 2018-12-06T08:21:40+01:00 Download 508af23
Download 7f8f230 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 304 2018-12-06T08:20:10+01:00 Download dee61eb
Download 3535c05 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 305 2018-12-06T01:26:31+01:00
Download a6a6d6d Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T16:36 CET (sv-comp)
Download 2e11397 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-07T13:20 CET (sv-comp)

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

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

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

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

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