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 (54db239ef92273930db7acb76febeffdc3fe3eaa1973502e505f7f766f9b4254, sv-benchmarks/c/ssh-simplified/s3_clnt_4_false-unreach-call_true-termination.cil.c).

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

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

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

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

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

Found 22 witnesses for program sv-benchmarks/c/ssh-simplified/s3_clnt_4_false-unreach-call_true-termination.cil.c, 54db239ef92273930db7acb76febeffdc3fe3eaa1973502e505f7f766f9b4254
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/54db239ef92273930db7acb76febeffdc3fe3eaa1973502e505f7f766f9b4254.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 9e0a130 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2018-12-08T10:06 CET (sv-comp)
Download a544a82 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 13 2018-12-08T01:00:18
Download 7ad10ee Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 65 2018-12-07T03:39 CET (sv-comp)
Download 35bc604 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7 78 2018-12-10T17:09:45+01:00
Download 78b78b0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 62 2018-12-08T02:53:16+01:00
Download 0659322 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 89 2018-12-10T20:36:09+01:00 Download 35bc604
Download c6befa1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 75 2018-12-09T20:53:17+01:00 Download 64b8a83
Download b8d2295 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 75 2018-12-09T20:38:33+01:00 Download 0df1ab1
Download dce5df4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 76 2018-12-09T18:21:15+01:00 Download b46330f
Download f953baf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 75 2018-12-08T23:44:48+01:00 Download 9e0a130
Download cdbc845 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 75 2018-12-08T22:10:43+01:00 Download a544a82
Download f1859a8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 75 2018-12-08T08:41:20+01:00 Download 78b78b0
Download aa523e5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 90 2018-12-08T05:02:22+01:00 Download fd1738f
Download f3aa204 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 75 2018-12-08T03:59:40+01:00 Download 8ec0d1f
Download d9cc625 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 97 2018-12-07T17:44:00+01:00 Download 7ad10ee
Download 6b1dcb0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 75 2018-12-06T10:20:04+01:00 Download 156f1ab
Download 338ec55 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 75 2018-12-06T09:49:15+01:00 Download 08cb52d
Download 5b3f960 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 75 2018-12-06T09:13:26+01:00 Download bfbe16d
Download 08cb52d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 62 2018-12-06T02:18:36+01:00
Download 894638c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 48 2018-12-06T09:42:10+01:00 Download e9ae4a1
Download c7f34a7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 48 2018-12-06T09:16:38+01:00 Download a4b4a82
Download 1b505f7 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T07:36 CET (sv-comp)

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

Trying to find witnesses for program (54db239ef92273930db7acb76febeffdc3fe3eaa1973502e505f7f766f9b4254, sv-benchmarks/c/ssh-simplified/s3_clnt_4_false-unreach-call_true-termination.cil.c).

Found 18 witnesses for program sv-benchmarks/c/ssh-simplified/s3_clnt_4_false-unreach-call_true-termination.cil.c, 54db239ef92273930db7acb76febeffdc3fe3eaa1973502e505f7f766f9b4254
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/54db239ef92273930db7acb76febeffdc3fe3eaa1973502e505f7f766f9b4254.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download d56a4bd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Taipan 81 2017-12-02T20:01Z
Download 26a7c08 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2017-12-02T19:11 CET (sv-comp)
Download 8d55569 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Kojak 82 2017-12-02T19:18Z
Download 2a82de9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 10 2017-12-01T13:08:29.861360
Download 5af5b9a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 11 2017-12-01T11:57:01.715004
Download 8712e94 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 22 2017-12-01T19:15 CET (sv-comp)
Download cfab5ad Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 22 2017-12-01T01:49 CET (sv-comp)
Download 35dc4ff Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 78 2017-12-03T01:15:55+01:00
Download 90b6305 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 55 2017-11-30T20:49:33+01:00
Download 5e6af0e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 89 2017-11-30T16:17:04+01:00
Download 449e42d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 44 2017-11-30T21:55:52+01:00
Download ba4be45 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 31 2017-12-01T23:58:04+01:00
Download e5f1675 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 55 2017-11-30T23:50 CET (sv-comp)
Download 2f93055 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Automizer 81 2017-12-02T07:09Z
Download b1f1ead Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness 2LS 61 2017-12-01T03:09 CET (sv-comp)
Download 687d121 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-03T01:50:38.074474
Download 360dcb9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T14:36:41.705765
Download 7314a67 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 883 2017-12-01T15:37 CET (sv-comp)

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

Trying to find witnesses for program (54db239ef92273930db7acb76febeffdc3fe3eaa1973502e505f7f766f9b4254, sv-benchmarks/c/ssh-simplified/s3_clnt_4_false-unreach-call_true-termination.cil.c).

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

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