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 (5626a6a7551a0f0e32b19ec2a32b2d974fabbbd8eee649eabf297b70a68208c7, sv-benchmarks/c/ssh-simplified/s3_clnt_1_true-unreach-call_true-termination.cil.c).

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

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

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

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 6c99cbd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2018-12-08T09:00 CET (sv-comp)
Download 0619197 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-08T11:02:17
Download fce9459 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 48 2018-12-06T16:21:14+01:00
Download bb7bc50 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 48 2018-12-10T20:00:37+01:00 Download d6b1619
Download d747277 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 48 2018-12-09T20:21:33+01:00 Download 4567eda
Download ee5af7b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 48 2018-12-09T17:36:38+01:00 Download aec32f8
Download ba29213 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 48 2018-12-08T23:16:03+01:00 Download 6c99cbd
Download 8073c98 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 48 2018-12-08T21:38:32+01:00 Download 0619197
Download a1da0d7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 48 2018-12-08T06:11:31+01:00 Download fce9459
Download 54b1aef Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 48 2018-12-08T03:47:57+01:00 Download 86636eb
Download 0c6e4c7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 48 2018-12-06T09:28:22+01:00 Download adccc59
Download ecea440 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 48 2018-12-06T08:51:04+01:00 Download c71468e
Download 13c12a8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 48 2018-12-06T08:14:49+01:00 Download e5a6c72
Download cf20095 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 48 2018-12-06T07:35:27+01:00 Download 7f0ddc5
Download c71468e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 48 2018-12-05T23:13:04+01:00
Download 3841c2e Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T07:09 CET (sv-comp)

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

Trying to find witnesses for program (5626a6a7551a0f0e32b19ec2a32b2d974fabbbd8eee649eabf297b70a68208c7, sv-benchmarks/c/ssh-simplified/s3_clnt_1_true-unreach-call_true-termination.cil.c).

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 0ad03e6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Taipan 92 2017-12-03T04:59Z
Download 211bba2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2017-12-02T01:25 CET (sv-comp)
Download 2d93d1c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T20:02:03.269944
Download 2df5d34 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T12:18:48.133605
Download e9ac834 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 kind 3 2017-12-01T23:49:40.646544
Download 2421b5d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 incr 3 2017-12-01T09:10:14.618255
Download 5d31af3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 3592 2017-12-01T19:31 CET (sv-comp)
Download 9a33d6f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 53 2017-12-03T00:57:31+01:00
Download b0afb7e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 4 2017-12-01T07:30:49+01:00
Download 665f482 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 48 2017-12-03T06:50:49+01:00 f39607e
Download c4dc6a7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 48 2017-12-03T04:13:00+01:00 b4ccc9b
Download b2703df Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 48 2017-12-03T01:16:35+01:00 364aa43
Download e3be35f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 48 2017-12-02T20:44:48+01:00 4e376ee
Download 4a5d38e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 48 2017-12-02T15:09:14+01:00 a726a42
Download 82e126e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 48 2017-12-02T08:47:56+01:00 775a73e
Download e9851cc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 48 2017-12-01T22:21:56+01:00 44a7a25
Download a77baeb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 48 2017-12-01T08:13:38+01:00 fbbdbb5
Download 7159cbd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 48 2017-12-01T07:18:08+01:00 1bb45fd
Download 0c584d9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 48 2017-12-01T05:44:44+01:00 e955e5e
Download d4c50cc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 48 2017-12-01T05:28:56+01:00 59ef264
Download 6f3fbe8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 48 2017-12-01T04:50:04+01:00 ffbf076
Download 778febd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 48 2017-12-01T04:47:32+01:00 c9965c2
Download 5d8f5b6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 48 2017-11-30T13:47:11+01:00
Download 7ea6a86 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26758M 54 2017-11-30T22:21:38+01:00
Download 56ab04d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26725 48 2017-11-30T21:44:04+01:00
Download a771ce1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker (unknown version) 41 2017-12-01T22:22:50+01:00
Download 5f1e8c3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CBMC 879 2017-11-30T16:17 CET (sv-comp)
Download 5ad13c0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Automizer 92 2017-12-02T09:02Z
Download 2d2a5d9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness 2LS 879 2017-11-30T19:08 CET (sv-comp)
Download 70f651f Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 878 2017-12-01T13:47 CET (sv-comp)

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

Trying to find witnesses for program (5626a6a7551a0f0e32b19ec2a32b2d974fabbbd8eee649eabf297b70a68208c7, sv-benchmarks/c/ssh-simplified/s3_clnt_1_true-unreach-call_true-termination.cil.c).

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

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