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 (dacb675a509e100cd9761391d26fd1c46320f67e4b401a592394238dddb66e9c, sv-benchmarks/c/ssh-simplified/s3_srvr_1a_true-unreach-call_false-termination.cil.c).

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

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

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

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

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

Found 15 witnesses for program sv-benchmarks/c/ssh-simplified/s3_srvr_1a_true-unreach-call_false-termination.cil.c, dacb675a509e100cd9761391d26fd1c46320f67e4b401a592394238dddb66e9c
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/dacb675a509e100cd9761391d26fd1c46320f67e4b401a592394238dddb66e9c.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download b6ad80d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-08T04:52:40
Download a3052d0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 22 2018-12-07T04:26:09+01:00
Download 4957d1e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 22 2018-12-10T19:48:11+01:00 Download ccae50e
Download ca6175a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 22 2018-12-09T20:21:49+01:00 Download e51b639
Download 173576a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 22 2018-12-09T19:48:26+01:00 Download feb7a4f
Download 04ce962 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 22 2018-12-09T17:28:09+01:00 Download 3e8ee82
Download f0ee1bd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 22 2018-12-08T21:47:11+01:00 Download b6ad80d
Download 5f3b9f1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 22 2018-12-08T06:09:06+01:00 Download a3052d0
Download f4cc1cf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 22 2018-12-06T08:45:31+01:00 Download f48b2f3
Download f24d14b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 22 2018-12-06T07:44:56+01:00 Download 67bae3d
Download f48b2f3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 22 2018-12-05T15:34:04+01:00
Download d75d88a Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 48 2018-12-08T03:01:44+01:00
Download 47438c3 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn 29852 48 2018-12-09T20:36:28+01:00
Download 32000a7 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn 29852 48 2018-12-06T09:40:45+01:00
Download 1094aa8 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn 29852 48 2018-12-05T22:53:40+01:00

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

Trying to find witnesses for program (dacb675a509e100cd9761391d26fd1c46320f67e4b401a592394238dddb66e9c, sv-benchmarks/c/ssh-simplified/s3_srvr_1a_true-unreach-call_false-termination.cil.c).

Found 19 witnesses for program sv-benchmarks/c/ssh-simplified/s3_srvr_1a_true-unreach-call_false-termination.cil.c, dacb675a509e100cd9761391d26fd1c46320f67e4b401a592394238dddb66e9c
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/dacb675a509e100cd9761391d26fd1c46320f67e4b401a592394238dddb66e9c.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download ddcbbae Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Taipan 26 2017-12-03T04:04Z
Download f4e2277 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Kojak 59 2017-12-02T03:58Z
Download 900df87 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 22 2017-12-03T07:05:23+01:00 5b65203
Download 2045f4c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 22 2017-12-03T01:48:51+01:00 97e9b1d
Download e0436bc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 22 2017-12-03T00:51:55+01:00 90668f4
Download 5612f6a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 22 2017-12-02T15:26:59+01:00 720ff33
Download 552b949 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 22 2017-12-01T06:56:23+01:00 247a844
Download 5c664d2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 22 2017-12-01T05:27:51+01:00 ca31695
Download 24a56d0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 22 2017-12-01T05:01:40+01:00 55f511a
Download 192bd96 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 22 2017-12-01T04:37:38+01:00 f18e6f7
Download 746b5f0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 22 2017-11-30T12:52:29+01:00
Download 5bc3d2c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26758M 34 2017-11-30T18:44:21+01:00
Download c6a37e3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26725 22 2017-11-30T23:33:14+01:00
Download 6e421c2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker (unknown version) 21 2017-12-02T07:00:02+01:00
Download cdbcb77 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Automizer 26 2017-12-02T09:57Z
Download ebc6f19 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness 2LS 339 2017-11-30T18:03 CET (sv-comp)
Download bd33d6e Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.6.1-svn 26773 47 2017-12-01T14:08:33+01:00
Download 9377e5b Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Automizer 46 2017-12-03T11:13Z
Download 3ddd38b Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness 2LS 24 2017-12-01T17:09 CET (sv-comp)

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

Trying to find witnesses for program (dacb675a509e100cd9761391d26fd1c46320f67e4b401a592394238dddb66e9c, sv-benchmarks/c/ssh-simplified/s3_srvr_1a_true-unreach-call_false-termination.cil.c).

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

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