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_spec14_product23_true-unreach-call_true-termination.cil.c
programSHA fdb7acd71518fe5b72d927fd03fb17c11e3f6bc8f74ba882a943d2e002d8ef01
witnessName results-verified/pinaka.2018-12-06_2014.logfiles/sv-comp19_prop-reachsafety.elevator_spec14_product23_true-unreach-call_true-termination.cil.c.files/witness.graphml
witnessSHA 6beaca15d151898ca171bb5f45c0e04cb334bb2049259729425e5cc8e8f57d88

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-07T01:51 CET (sv-comp)
producer Pinaka
program-sha256 fdb7acd71518fe5b72d927fd03fb17c11e3f6bc8f74ba882a943d2e002d8ef01
programfile ../../sv-benchmarks/c/product-lines/elevator_spec14_product23_true-unreach-call_true-termination.cil.c
programhash fdb7acd71518fe5b72d927fd03fb17c11e3f6bc8f74ba882a943d2e002d8ef01
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/6beaca15d151898ca171bb5f45c0e04cb334bb2049259729425e5cc8e8f57d88.graphml
witness-sha256 6beaca15d151898ca171bb5f45c0e04cb334bb2049259729425e5cc8e8f57d88
witness-size 3224
witness-type correctness_witness

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

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

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

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

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

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 3ca600e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2019-12-03T21:50 CET (comp)
Download d73f828 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 296 2019-12-11T20:29:16+01:00 Download 5fab5e8
Download 46a0ea9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 296 2019-12-11T20:07:13+01:00 Download 11be039
Download 44c686d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 296 2019-12-11T20:02:50+01:00 Download 442b944
Download 3cb446a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 296 2019-12-08T00:58:20+01:00 Download 330fe7f
Download 9c3552a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 296 2019-12-05T19:20:51+01:00 Download e3d7dc6
Download a212f20 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 296 2019-12-05T19:03:04+01:00 Download f66dbff
Download 761fc2a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 296 2019-12-04T02:08:02+01:00 Download 3ca600e
Download 7ec41ff Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 296 2019-11-30T19:53:44+01:00 Download 66a0d99
Download 7a8d2f3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 296 2019-11-30T17:20:20+01:00 Download 3320770
Download 3320770 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / svcomp20 296 2019-11-30T06:48:05+01:00
Download 330fe7f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8 296 2019-12-07T15:05:34+01:00
Download 11be039 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 296 2019-12-01T19:44:23+01:00
Download f0fe141 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2019-12-04T00:49 CET (comp)

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download db0e26d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2018-12-08T12:18 CET (sv-comp)
Download 778acd2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-08T00:26:30
Download 6beaca1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2018-12-07T01:51 CET (sv-comp)
Download 553ca19 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7 296 2018-12-10T18:01:48+01:00
Download dcbd523 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 296 2018-12-06T23:57:41+01:00
Download 6fdd445 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 296 2018-12-10T19:34:59+01:00 Download 553ca19
Download ed1db87 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 296 2018-12-10T10:31:50+01:00 Download 9f77096
Download 57e39de Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 296 2018-12-08T23:07:54+01:00 Download db0e26d
Download 463cc96 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 296 2018-12-08T21:43:12+01:00 Download 778acd2
Download c76cc00 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 296 2018-12-08T07:04:58+01:00 Download dcbd523
Download 1ab9aa3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 296 2018-12-08T03:40:51+01:00 Download cef4716
Download e092db9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 296 2018-12-08T02:04:42+01:00 Download 9f77096
Download 7aa95d1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 296 2018-12-07T16:38:19+01:00 Download 6beaca1
Download 1436bee Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 296 2018-12-06T09:28:28+01:00 Download 935f7fc
Download 0f4b689 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 296 2018-12-06T09:01:32+01:00 Download 527f853
Download 6a6e6cf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 296 2018-12-06T07:33:11+01:00 Download 05eeafd
Download 527f853 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 296 2018-12-06T05:19:43+01:00
Download 2786b77 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T18:24 CET (sv-comp)
Download a741883 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-06T21:21 CET (sv-comp)

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

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

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

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

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