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/email_spec1_product33_false-unreach-call_true-termination.cil.c
programSHA 386027027778a31fd9090100d572c0dd0ebc8bcb4f76d08020d2dff8baa6a1dd
witnessName results-verified/esbmc-kind.2017-12-01_1259.logfiles/sv-comp18.email_spec1_product33_false-unreach-call_true-termination.cil.c.files/witness.graphml
witnessSHA 26b2eea5215c0d48cb4232cda09e2cd5e58f2b499be6901a5cf5955a8639329e

Information about the Witness from Competition Database

from https://sv-comp.sosy-lab.org/2018/results/witnessInfoByHash/26b2eea5215c0d48cb4232cda09e2cd5e58f2b499be6901a5cf5955a8639329e.json

Key Value
architecture 32bit
creationtime 2017-12-01T13:53:37.725051
producer ESBMC 4.6.0 kind
program-sha256 386027027778a31fd9090100d572c0dd0ebc8bcb4f76d08020d2dff8baa6a1dd
programfile ../../sv-benchmarks/c/product-lines/email_spec1_product33_false-unreach-call_true-termination.cil.c
programhash d32220fceacecebaa5db7cb0ef53bc112418ed34
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/26b2eea5215c0d48cb4232cda09e2cd5e58f2b499be6901a5cf5955a8639329e.graphml
witness-sha256 26b2eea5215c0d48cb4232cda09e2cd5e58f2b499be6901a5cf5955a8639329e
witness-size 13912
witness-type violation_witness

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

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

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

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

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 9360297 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 2 2019-12-01 01:38:35
Download aed3c5b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 176 2019-12-11T21:45:24+01:00 Download bce3da8
Download 39bde83 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 224 2019-12-11T21:09:18+01:00 Download 9360297
Download 926d6cc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 176 2019-12-11T20:54:22+01:00 Download ab9efb1
Download 071b885 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 228 2019-12-11T20:44:33+01:00 Download f54153a
Download 66caf25 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 176 2019-12-08T01:51:28+01:00 Download b68a7f3
Download 7c2cdfe Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 229 2019-12-03T08:58:00+01:00 Download f469748
Download 931dfa0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 176 2019-12-03T08:08:21+01:00 Download 957e866
Download 957e866 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 164 2019-11-29T15:24:26+01:00
Download b68a7f3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8 179 2019-12-07T11:57:43+01:00
Download bce3da8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 176 2019-12-01T16:48:52+01:00
Download 014ca39 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 182 2019-12-05T20:20:26+01:00 Download c9236f5
Download 0c51b41 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 182 2019-12-05T19:34:11+01:00 Download 8827b35

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download d924204 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2018-12-08T02:10 CET (sv-comp)
Download 55d5bbc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 29 2018-12-08T08:39:36
Download ffaa22a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 161 2018-12-07T09:20 CET (sv-comp)
Download 275fd12 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7 168 2018-12-10T17:15:04+01:00
Download d02f9a6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 180 2018-12-06T21:15:56+01:00
Download a8cd9d1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 176 2018-12-10T20:36:57+01:00 Download 275fd12
Download 65ac31a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 232 2018-12-09T18:20:07+01:00 Download 510f43d
Download 2a7b66a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 229 2018-12-08T23:43:58+01:00 Download d924204
Download 2ef5b7f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 113 2018-12-08T22:09:29+01:00 Download 55d5bbc
Download 16f517e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 176 2018-12-08T08:37:38+01:00 Download d02f9a6
Download 1f4354c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 224 2018-12-07T17:38:41+01:00 Download ffaa22a
Download 6e20829 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 176 2018-12-06T09:48:23+01:00 Download 73d2a88
Download 73d2a88 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 164 2018-12-05T14:15:15+01:00
Download 67ea003 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 182 2018-12-08T05:01:45+01:00 Download 49d1a4a
Download 8590de3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 182 2018-12-06T10:14:15+01:00 Download c22de84
Download 647e524 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 183 2018-12-06T09:40:37+01:00 Download 1451a9b
Download 37e01b3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 182 2018-12-06T09:13:50+01:00 Download 14d8aff
Download 9097954 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T02:46 CET (sv-comp)

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

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

Found 13 witnesses for program sv-benchmarks/c/product-lines/email_spec1_product33_false-unreach-call_true-termination.cil.c, 386027027778a31fd9090100d572c0dd0ebc8bcb4f76d08020d2dff8baa6a1dd
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/386027027778a31fd9090100d572c0dd0ebc8bcb4f76d08020d2dff8baa6a1dd.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 3001ff1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2017-12-02T12:54 CET (sv-comp)
Download 26b2eea Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 14 2017-12-01T13:53:37.725051
Download e7b3698 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 14 2017-12-01T11:27:06.650459
Download c6436ad Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 93 2017-12-01T20:36 CET (sv-comp)
Download 1657174 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 93 2017-12-01T00:43 CET (sv-comp)
Download 0206032 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 154 2017-12-01T01:35:28+01:00
Download e635835 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 137 2017-11-30T15:19:18+01:00
Download ea3895c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 114 2017-12-01T01:03 CET (sv-comp)
Download ba9862f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness 2LS 139 2017-11-30T19:05 CET (sv-comp)
Download ab0725c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-03T00:59:57.570672
Download 6a0ca82 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T11:04:23.001816
Download ad9a341 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 468 2017-12-01T16:01 CET (sv-comp)
Download 1240052 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 1178 2017-12-01T13:42 CET (sv-comp)

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

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

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

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