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 (4e93a6c73f49b57d9fc4ee402fc92c61e75e8b2a3dbee25826b03c36cc9029bd, sv-benchmarks/c/ssh-simplified/s3_clnt_4_true-unreach-call_true-termination.cil.c).

Found 0 witnesses for program sv-benchmarks/c/ssh-simplified/s3_clnt_4_true-unreach-call_true-termination.cil.c, 4e93a6c73f49b57d9fc4ee402fc92c61e75e8b2a3dbee25826b03c36cc9029bd
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/4e93a6c73f49b57d9fc4ee402fc92c61e75e8b2a3dbee25826b03c36cc9029bd.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 (4e93a6c73f49b57d9fc4ee402fc92c61e75e8b2a3dbee25826b03c36cc9029bd, sv-benchmarks/c/ssh-simplified/s3_clnt_4_true-unreach-call_true-termination.cil.c).

Found 0 witnesses for program sv-benchmarks/c/ssh-simplified/s3_clnt_4_true-unreach-call_true-termination.cil.c, 4e93a6c73f49b57d9fc4ee402fc92c61e75e8b2a3dbee25826b03c36cc9029bd
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/4e93a6c73f49b57d9fc4ee402fc92c61e75e8b2a3dbee25826b03c36cc9029bd.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 (4e93a6c73f49b57d9fc4ee402fc92c61e75e8b2a3dbee25826b03c36cc9029bd, sv-benchmarks/c/ssh-simplified/s3_clnt_4_true-unreach-call_true-termination.cil.c).

Found 0 witnesses for program sv-benchmarks/c/ssh-simplified/s3_clnt_4_true-unreach-call_true-termination.cil.c, 4e93a6c73f49b57d9fc4ee402fc92c61e75e8b2a3dbee25826b03c36cc9029bd
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/4e93a6c73f49b57d9fc4ee402fc92c61e75e8b2a3dbee25826b03c36cc9029bd.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 (4e93a6c73f49b57d9fc4ee402fc92c61e75e8b2a3dbee25826b03c36cc9029bd, sv-benchmarks/c/ssh-simplified/s3_clnt_4_true-unreach-call_true-termination.cil.c).

Found 0 witnesses for program sv-benchmarks/c/ssh-simplified/s3_clnt_4_true-unreach-call_true-termination.cil.c, 4e93a6c73f49b57d9fc4ee402fc92c61e75e8b2a3dbee25826b03c36cc9029bd
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/4e93a6c73f49b57d9fc4ee402fc92c61e75e8b2a3dbee25826b03c36cc9029bd.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 (4e93a6c73f49b57d9fc4ee402fc92c61e75e8b2a3dbee25826b03c36cc9029bd, sv-benchmarks/c/ssh-simplified/s3_clnt_4_true-unreach-call_true-termination.cil.c).

Found 0 witnesses for program sv-benchmarks/c/ssh-simplified/s3_clnt_4_true-unreach-call_true-termination.cil.c, 4e93a6c73f49b57d9fc4ee402fc92c61e75e8b2a3dbee25826b03c36cc9029bd
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/4e93a6c73f49b57d9fc4ee402fc92c61e75e8b2a3dbee25826b03c36cc9029bd.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 '19

Trying to find witnesses for program (4e93a6c73f49b57d9fc4ee402fc92c61e75e8b2a3dbee25826b03c36cc9029bd, sv-benchmarks/c/ssh-simplified/s3_clnt_4_true-unreach-call_true-termination.cil.c).

Found 16 witnesses for program sv-benchmarks/c/ssh-simplified/s3_clnt_4_true-unreach-call_true-termination.cil.c, 4e93a6c73f49b57d9fc4ee402fc92c61e75e8b2a3dbee25826b03c36cc9029bd
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/4e93a6c73f49b57d9fc4ee402fc92c61e75e8b2a3dbee25826b03c36cc9029bd.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download a32558f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2018-12-08T00:21 CET (sv-comp)
Download 3261751 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-08T11:04:34
Download 4a7915e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 48 2018-12-07T19:09:56+01:00
Download 5a702fc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 48 2018-12-10T20:04:48+01:00 Download 10e519b
Download 708d08c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 48 2018-12-09T20:30:22+01:00 Download 84b9adc
Download 5568eb2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 48 2018-12-09T20:08:19+01:00 Download 37f64d1
Download e6501fc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 48 2018-12-08T23:12:35+01:00 Download a32558f
Download 2a43ca1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 48 2018-12-08T21:43:58+01:00 Download 3261751
Download ad1cf62 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 48 2018-12-08T05:40:37+01:00 Download 4a7915e
Download 74a0796 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 48 2018-12-08T02:34:29+01:00 Download e5be146
Download 603b680 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 48 2018-12-06T09:28:45+01:00 Download 0cda3c2
Download ed86cca Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 48 2018-12-06T08:45:36+01:00 Download ff93d52
Download 22be264 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 48 2018-12-06T08:19:48+01:00 Download 4b58995
Download 7103ec2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 48 2018-12-06T08:12:35+01:00 Download 46699fd
Download ff93d52 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 48 2018-12-06T06:22:22+01:00
Download 352da5d Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T11:02 CET (sv-comp)

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

Trying to find witnesses for program (4e93a6c73f49b57d9fc4ee402fc92c61e75e8b2a3dbee25826b03c36cc9029bd, sv-benchmarks/c/ssh-simplified/s3_clnt_4_true-unreach-call_true-termination.cil.c).

Found 30 witnesses for program sv-benchmarks/c/ssh-simplified/s3_clnt_4_true-unreach-call_true-termination.cil.c, 4e93a6c73f49b57d9fc4ee402fc92c61e75e8b2a3dbee25826b03c36cc9029bd
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/4e93a6c73f49b57d9fc4ee402fc92c61e75e8b2a3dbee25826b03c36cc9029bd.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download b5b1502 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Taipan 92 2017-12-03T03:32Z
Download c172880 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2017-12-02T01:00 CET (sv-comp)
Download 9eae51b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T20:34:58.796867
Download 728c874 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T10:48:26.632394
Download 750e3fb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 kind 3 2017-12-01T21:48:19.046776
Download 7780990 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 incr 3 2017-12-01T08:44:22.472630
Download e631a2a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 3701 2017-12-01T17:01 CET (sv-comp)
Download 3564760 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 53 2017-12-03T01:31:25+01:00
Download 0373730 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 4 2017-12-01T05:33:28+01:00
Download 04c599d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 48 2017-12-03T06:51:05+01:00 c139fc1
Download 74a4689 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 48 2017-12-03T04:13:47+01:00 9275f93
Download a3e54d0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 48 2017-12-03T00:43:32+01:00 ce262fa
Download 5ddc792 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 48 2017-12-02T19:59:31+01:00 b4b533f
Download 8b16967 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 48 2017-12-02T15:07:58+01:00 a005aaf
Download d5693f9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 48 2017-12-02T09:01:22+01:00 81753b7
Download d42c661 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 48 2017-12-01T22:24:23+01:00 cb347cd
Download 2f0c1da Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 48 2017-12-01T08:13:12+01:00 14eba46
Download f0f8424 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 48 2017-12-01T07:15:06+01:00 0ccec08
Download ba33770 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 48 2017-12-01T06:53:27+01:00 4210a83
Download 1aa4cff Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 48 2017-12-01T06:46:56+01:00 1ed7996
Download a20b5cd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 48 2017-12-01T06:02:38+01:00 71570a5
Download 3481483 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 48 2017-12-01T05:20:39+01:00 f3d5c9b
Download 85c3cd5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 48 2017-12-01T00:53:40+01:00
Download b4d106e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26758M 52 2017-11-30T13:12:19+01:00
Download 9bb7d13 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26725 48 2017-12-01T01:06:07+01:00
Download 83fd392 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker (unknown version) 41 2017-12-02T12:19:48+01:00
Download 1eb3407 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CBMC 884 2017-11-30T14:41 CET (sv-comp)
Download acc4e13 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Automizer 92 2017-12-02T01:11Z
Download 19a885c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness 2LS 884 2017-11-30T20:39 CET (sv-comp)
Download a87a8f4 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 884 2017-12-01T17:33 CET (sv-comp)

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

Trying to find witnesses for program (4e93a6c73f49b57d9fc4ee402fc92c61e75e8b2a3dbee25826b03c36cc9029bd, sv-benchmarks/c/ssh-simplified/s3_clnt_4_true-unreach-call_true-termination.cil.c).

Found 0 witnesses for program sv-benchmarks/c/ssh-simplified/s3_clnt_4_true-unreach-call_true-termination.cil.c, 4e93a6c73f49b57d9fc4ee402fc92c61e75e8b2a3dbee25826b03c36cc9029bd
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/4e93a6c73f49b57d9fc4ee402fc92c61e75e8b2a3dbee25826b03c36cc9029bd.json

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