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_product11_true-unreach-call_true-termination.cil.c
programSHA 1d86cad6f641cc1f4c7e343910fcf26e4d93cc6feec888515a1bc8d950a56406
witnessName results-validated/cpa-seq-validate-correctness-witnesses-cpa-seq.2018-12-06_0837.logfiles/sv-comp19_prop-reachsafety.elevator_spec14_product11_true-unreach-call_true-termination.cil.c.files/witness.graphml
witnessSHA 0dd63ddb5549815357f5a0081b2a0ed0cfc40e6ac9b82129246db7a0832a09d8

Information about the Witness from Competition Database

from https://sv-comp.sosy-lab.org/2019/results/witnessInfoByHash/0dd63ddb5549815357f5a0081b2a0ed0cfc40e6ac9b82129246db7a0832a09d8.json

Key Value
architecture 32bit
creationtime 2018-12-06T09:03:27+01:00
inputwitnesshash 0c792b9bf5ff1ca0bb50dc3e809faf065933bc529f5ff4939b4e66b95072875b
producer CPAchecker 1.7-svn 29852
program-sha256 1d86cad6f641cc1f4c7e343910fcf26e4d93cc6feec888515a1bc8d950a56406
programfile ../../sv-benchmarks/c/product-lines/elevator_spec14_product11_true-unreach-call_true-termination.cil.c
programhash 1d86cad6f641cc1f4c7e343910fcf26e4d93cc6feec888515a1bc8d950a56406
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/0dd63ddb5549815357f5a0081b2a0ed0cfc40e6ac9b82129246db7a0832a09d8.graphml
witness-sha256 0dd63ddb5549815357f5a0081b2a0ed0cfc40e6ac9b82129246db7a0832a09d8
witness-size 284531
witness-type correctness_witness

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

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

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

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

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

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 2540a8b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2019-12-03T23:30 CET (comp)
Download 633959c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 284 2019-12-11T20:17:52+01:00 Download 4a7c643
Download 2c4cb9d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 284 2019-12-11T20:15:42+01:00 Download e892b3a
Download 27b9960 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 284 2019-12-11T20:03:05+01:00 Download 0a3b2fd
Download 48b13dd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 284 2019-12-08T00:51:27+01:00 Download bf2f485
Download 8d183b2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 284 2019-12-05T19:20:48+01:00 Download 72d3cad
Download 48f2e9e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 284 2019-12-05T19:03:09+01:00 Download 367c703
Download bb6ee77 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 284 2019-12-04T02:07:36+01:00 Download 2540a8b
Download 1c19511 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 284 2019-11-30T19:17:04+01:00 Download 04b31af
Download 0c9ec2e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 284 2019-11-30T17:12:47+01:00 Download 0a74b4b
Download 0a74b4b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / svcomp20 285 2019-11-30T02:36:50+01:00
Download bf2f485 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8 284 2019-12-07T15:10:38+01:00
Download 4a7c643 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 285 2019-12-01T17:48:51+01:00
Download 60cb9f9 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2019-12-03T22:04 CET (comp)

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download fa29845 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2018-12-08T02:55 CET (sv-comp)
Download e9ae09c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-08T13:17:59
Download c80ca88 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2018-12-07T09:13 CET (sv-comp)
Download c2485fd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7 284 2018-12-10T19:07:01+01:00
Download bc1ef62 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 284 2018-12-06T13:45:42+01:00
Download 3a38d54 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 285 2018-12-10T19:37:32+01:00 Download c2485fd
Download 1da3125 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 285 2018-12-10T10:31:38+01:00 Download 8c6ca41
Download 784ce51 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 285 2018-12-08T23:15:35+01:00 Download fa29845
Download 269ec68 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 285 2018-12-08T21:38:12+01:00 Download e9ae09c
Download a21147c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 285 2018-12-08T06:26:05+01:00 Download bc1ef62
Download 683b00d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 285 2018-12-08T03:15:22+01:00 Download 578c826
Download 72a1a41 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 285 2018-12-08T02:08:13+01:00 Download 8c6ca41
Download 6f67fd6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 285 2018-12-07T16:39:33+01:00 Download c80ca88
Download 5adb10c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 285 2018-12-06T09:28:41+01:00 Download f868f96
Download 0dd63dd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 285 2018-12-06T09:03:27+01:00 Download 0c792b9
Download 9fe3adc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 285 2018-12-06T07:40:42+01:00 Download 43ce689
Download 0c792b9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 285 2018-12-05T17:49:16+01:00
Download a9575de Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T01:29 CET (sv-comp)
Download c2743af Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-07T09:56 CET (sv-comp)

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

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

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

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

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