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_spec11_product32_false-unreach-call_true-termination.cil.c
programSHA 51b2677cef4da493ee5c88b1a471414cf45ad082107adf395e85b5113e5ebfbc
witnessName results-verified/esbmc-kind.2018-12-06_1103.logfiles/sv-comp19_prop-reachsafety.email_spec11_product32_false-unreach-call_true-termination.cil.c.files/witness.graphml
witnessSHA 800464db1e5741b02045558c21d551fbbc2b982be0edb10aa35bd383e938aa76

Information about the Witness from Competition Database

from https://sv-comp.sosy-lab.org/2019/results/witnessInfoByHash/800464db1e5741b02045558c21d551fbbc2b982be0edb10aa35bd383e938aa76.json

Key Value
architecture 32bit
creationtime 2018-12-07T23:23:03.845320
producer ESBMC 6.0.0 kind
programfile ../../sv-benchmarks/c/product-lines/email_spec11_product32_false-unreach-call_true-termination.cil.c
programhash 41a8515974e55238c7bd0948e6758bbf73783527
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/800464db1e5741b02045558c21d551fbbc2b982be0edb10aa35bd383e938aa76.graphml
witness-sha256 800464db1e5741b02045558c21d551fbbc2b982be0edb10aa35bd383e938aa76
witness-size 12117
witness-type violation_witness

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

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

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

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

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 90badff Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 2 2019-12-01 19:58:33
Download caa9158 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 141 2019-12-11T21:40:06+01:00 Download b23beb7
Download d5628f4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 131 2019-12-11T21:09:43+01:00 Download 90badff
Download af45fc2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 132 2019-12-11T20:54:29+01:00 Download 72e5af8
Download bd84a52 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 138 2019-12-11T20:44:33+01:00 Download 717800d
Download dedd2c4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 134 2019-12-03T08:57:40+01:00 Download 95cf00b
Download 9af8dcb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 128 2019-12-03T08:10:04+01:00 Download a2f3aef
Download a2f3aef Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 120 2019-11-29T22:32:09+01:00
Download b23beb7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 141 2019-12-01T16:30:50+01:00
Download b15fa08 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 205 2019-12-08T01:51:28+01:00 Download 5aeb588
Download 2b5aade Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 205 2019-12-05T20:20:25+01:00 Download 3b29fe9
Download 11d7f5f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 205 2019-12-05T19:34:47+01:00 Download e3c1690

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 96ced2a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2018-12-08T05:40 CET (sv-comp)
Download d5a1b4b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 21 2018-12-08T18:14:03
Download 2f9f5dc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 91 2018-12-07T07:53 CET (sv-comp)
Download 647ce42 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 145 2018-12-06T13:20:56+01:00
Download e8a29f5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 138 2018-12-09T17:53:54+01:00 Download 2876487
Download 1805f00 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 197 2018-12-08T23:42:16+01:00 Download 96ced2a
Download f449fc7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 83 2018-12-08T22:11:21+01:00 Download d5a1b4b
Download b5ab31f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 142 2018-12-08T07:59:13+01:00 Download 647ce42
Download 72510bd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 191 2018-12-08T05:00:17+01:00 Download 800464d
Download 4af757c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 131 2018-12-07T17:44:34+01:00 Download 2f9f5dc
Download be030ce Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 126 2018-12-06T10:18:18+01:00 Download 48742d9
Download 50f2325 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 128 2018-12-06T09:48:24+01:00 Download e6cddd4
Download e6cddd4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 120 2018-12-06T02:48:42+01:00
Download 94908a7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 205 2018-12-10T20:35:01+01:00 Download 2f4320f
Download bc21298 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 205 2018-12-06T09:41:57+01:00 Download a51e7f6
Download 8b68a40 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 205 2018-12-06T09:17:02+01:00 Download 3e1af47
Download 7cf1f73 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 205 2018-12-06T09:08:55+01:00 Download 5d54e7a
Download 70e1018 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-07T22:42 CET (sv-comp)

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

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

Found 12 witnesses for program sv-benchmarks/c/product-lines/email_spec11_product32_false-unreach-call_true-termination.cil.c, 51b2677cef4da493ee5c88b1a471414cf45ad082107adf395e85b5113e5ebfbc
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/51b2677cef4da493ee5c88b1a471414cf45ad082107adf395e85b5113e5ebfbc.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 6609c15 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2017-12-02T09:37 CET (sv-comp)
Download 142ddec Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 9 2017-12-01T23:59:15.150169
Download edf8cd0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 15 2017-12-01T08:05:26.895122
Download 2d00583 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 89 2017-12-01T19:08 CET (sv-comp)
Download a71dba8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 74 2017-12-01T00:49 CET (sv-comp)
Download edfe268 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 112 2017-11-30T11:38:22+01:00
Download d9306ce Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 132 2017-12-01T00:08 CET (sv-comp)
Download d0b4a8b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness 2LS 94 2017-11-30T14:39 CET (sv-comp)
Download 70c350b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T21:45:31.952599
Download 29bd9b4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T15:07:45.717983
Download d9f0885 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 734 2017-12-01T14:26 CET (sv-comp)
Download 649853b Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 2177 2017-12-01T16:11 CET (sv-comp)

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

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

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

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