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

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

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

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

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download c9ab3ae Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2018-12-08T02:08 CET (sv-comp)
Download 0cc7cb9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 11 2018-12-08T02:02:43
Download 9a0e492 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 35 2018-12-07T01:20 CET (sv-comp)
Download f4f92ad Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7 44 2018-12-10T18:57:55+01:00
Download 67d6589 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 45 2018-12-07T10:50:05+01:00
Download fe7993b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 49 2018-12-10T20:36:00+01:00 Download f4f92ad
Download 12a0006 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 48 2018-12-09T20:53:13+01:00 Download 809555a
Download 8839484 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 48 2018-12-09T20:40:01+01:00 Download 37dd647
Download 7bc0505 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 47 2018-12-09T20:30:46+01:00 Download 18acd09
Download 93185e0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 48 2018-12-09T18:20:39+01:00 Download ca744f1
Download 55a040a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 49 2018-12-08T23:44:46+01:00 Download c9ab3ae
Download 84681fa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 47 2018-12-08T22:10:57+01:00 Download 0cc7cb9
Download 20d7a73 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 48 2018-12-08T09:00:47+01:00 Download 67d6589
Download 3758dbe Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 48 2018-12-08T05:04:44+01:00 Download 69b41d0
Download 97cd062 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 49 2018-12-07T17:45:11+01:00 Download 9a0e492
Download 3b26678 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 48 2018-12-06T10:18:18+01:00 Download e2074e3
Download d58db58 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 50 2018-12-06T09:48:00+01:00 Download 0c887b9
Download 3476473 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 50 2018-12-06T09:17:49+01:00 Download d5f1044
Download 0c887b9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 48 2018-12-05T11:40:08+01:00
Download 8463e48 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 59 2018-12-06T09:41:35+01:00 Download 29c80e1
Download 0abd81a Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn 29852 169 2018-12-06T05:47:39+01:00

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 01b3613 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Taipan 57 2017-12-03T00:06Z
Download 0f06c3a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2017-12-02T17:08 CET (sv-comp)
Download 3755568 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Kojak 58 2017-12-02T10:27Z
Download a618037 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 9 2017-12-01T19:43:58.548060
Download 138c3eb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 9 2017-12-01T13:38:47.870959
Download 08513d9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 15 2017-12-01T17:28 CET (sv-comp)
Download a28ed52 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 15 2017-12-01T04:52 CET (sv-comp)
Download 990598c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 44 2017-12-02T22:14:47+01:00
Download 2e55122 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 43 2017-12-01T00:19:09+01:00
Download c5994c5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 70 2017-11-30T12:16:39+01:00
Download 85e06a1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 27 2017-11-30T12:45:35+01:00
Download 796eb26 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 17 2017-12-01T21:12:41+01:00
Download daaf247 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 35 2017-11-30T11:58 CET (sv-comp)
Download 40bb7d0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Automizer 58 2017-12-02T01:15Z
Download bb00c94 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness 2LS 33 2017-11-30T20:49 CET (sv-comp)
Download 94b97d1 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Automizer 151 2017-12-03T11:16Z
Download 1db9e6a Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness 2LS 102 2017-12-01T16:22 CET (sv-comp)

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

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

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

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