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).

This link does not point to a witness, but below is a list of witnesses for the same program.

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

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

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

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

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 47766a3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 2 2019-12-01 19:18:48
Download 9dee194 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 125 2019-12-11T21:59:03+01:00 Download feca9eb
Download cf01721 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 121 2019-12-11T21:09:16+01:00 Download 47766a3
Download 2a74159 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 192 2019-12-11T20:55:26+01:00 Download 70561f5
Download ac4b455 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 124 2019-12-11T20:44:49+01:00 Download 7c82779
Download 65808f4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 140 2019-12-08T01:51:24+01:00 Download 5dc4187
Download 8fea83a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 136 2019-12-03T08:58:01+01:00 Download e7327f5
Download 1667dec Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 125 2019-12-03T08:09:10+01:00 Download add1b83
Download add1b83 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 117 2019-11-30T08:32:23+01:00
Download 5dc4187 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8 142 2019-12-07T11:18:55+01:00
Download feca9eb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 125 2019-12-01T14:02:36+01:00
Download 08867c0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 194 2019-12-05T20:21:20+01:00 Download c7e1b45
Download f7c3155 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 195 2019-12-05T19:34:32+01:00 Download 34d37a5

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 6d3f4c1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2018-12-08T07:14 CET (sv-comp)
Download 3a52be3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 20 2018-12-08T01:03:43
Download 7aac92e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 86 2018-12-06T21:20 CET (sv-comp)
Download 85754b1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7 133 2018-12-10T17:07:39+01:00
Download 51961a7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 125 2018-12-06T16:19:38+01:00
Download 8ac7c06 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 140 2018-12-10T20:34:50+01:00 Download 85754b1
Download bac5da5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 124 2018-12-09T18:21:10+01:00 Download d82c597
Download 81df7cd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 180 2018-12-08T23:43:02+01:00 Download 6d3f4c1
Download 239456d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 82 2018-12-08T22:10:40+01:00 Download 3a52be3
Download db97c6c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 126 2018-12-08T08:16:34+01:00 Download 51961a7
Download 2b92c12 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 192 2018-12-08T04:54:09+01:00 Download 6420b96
Download d921d90 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 121 2018-12-07T17:43:31+01:00 Download 7aac92e
Download d047ac6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 139 2018-12-06T10:12:50+01:00 Download b1b9793
Download 3357bac Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 126 2018-12-06T09:49:14+01:00 Download c5760ac
Download c5760ac Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 118 2018-12-05T06:49:25+01:00
Download 95784e7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 195 2018-12-06T09:40:48+01:00 Download fca1377
Download d2d7341 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 194 2018-12-06T09:20:01+01:00 Download 2141221
Download 1c3d49c Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T01:53 CET (sv-comp)

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 60e0397 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2017-12-02T09:13 CET (sv-comp)
Download e4d03ed Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 13 2017-12-01T20:50:26.766232
Download 7cd9ee2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 15 2017-12-01T07:49:58.919773
Download 3b005b8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 98 2017-12-01T20:38 CET (sv-comp)
Download 98d18c2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 97 2017-11-30T19:16 CET (sv-comp)
Download 669f3c5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 110 2017-11-30T13:31:06+01:00
Download 7afda47 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 124 2017-11-30T21:48 CET (sv-comp)
Download da490c3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness 2LS 82 2017-11-30T21:43 CET (sv-comp)
Download cf8e2b6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T20:18:20.680793
Download 2cad376 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T13:39:11.692617
Download 5c1539c Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 732 2017-12-01T17:43 CET (sv-comp)
Download acfaa1b Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 2155 2017-12-01T12:20 CET (sv-comp)

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

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

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

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