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).
Key | Value |
programName | sv-benchmarks/c/ssh-simplified/s3_clnt_2_false-unreach-call_true-termination.cil.c |
programSHA | 01cac1b76ec9eb5ef92345a0fcbd0fe27584a4ec279b6252da6304339b3faf10 |
witnessName | results-verified/cpa-bam-slicing.2017-11-30_1120.logfiles/sv-comp18.s3_clnt_2_false-unreach-call_true-termination.cil.c.files/witness.graphml |
witnessSHA | 7fd617262a096ed57585d4d11ca84b1e5916e64ef6ac4eee2cd4a2c9462ed4d3 |
Key | Value |
architecture | 32bit |
creationtime | 2017-11-30T14:43:52+01:00 |
producer | CPAchecker 1.6.1-svn 26758M |
program-sha256 | 01cac1b76ec9eb5ef92345a0fcbd0fe27584a4ec279b6252da6304339b3faf10 |
programfile | ../../sv-benchmarks/c/ssh-simplified/s3_clnt_2_false-unreach-call_true-termination.cil.c |
programhash | 0ff0314320984fb195ac6057440730ec5a81b029 |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/7fd617262a096ed57585d4d11ca84b1e5916e64ef6ac4eee2cd4a2c9462ed4d3.graphml |
witness-sha256 | 7fd617262a096ed57585d4d11ca84b1e5916e64ef6ac4eee2cd4a2c9462ed4d3 |
witness-size | 87532 |
witness-type | violation_witness |
Found 0 witnesses for program sv-benchmarks/c/ssh-simplified/s3_clnt_2_false-unreach-call_true-termination.cil.c, 01cac1b76ec9eb5ef92345a0fcbd0fe27584a4ec279b6252da6304339b3faf10
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/01cac1b76ec9eb5ef92345a0fcbd0fe27584a4ec279b6252da6304339b3faf10.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/ssh-simplified/s3_clnt_2_false-unreach-call_true-termination.cil.c, 01cac1b76ec9eb5ef92345a0fcbd0fe27584a4ec279b6252da6304339b3faf10
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/01cac1b76ec9eb5ef92345a0fcbd0fe27584a4ec279b6252da6304339b3faf10.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/ssh-simplified/s3_clnt_2_false-unreach-call_true-termination.cil.c, 01cac1b76ec9eb5ef92345a0fcbd0fe27584a4ec279b6252da6304339b3faf10
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/01cac1b76ec9eb5ef92345a0fcbd0fe27584a4ec279b6252da6304339b3faf10.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/ssh-simplified/s3_clnt_2_false-unreach-call_true-termination.cil.c, 01cac1b76ec9eb5ef92345a0fcbd0fe27584a4ec279b6252da6304339b3faf10
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/01cac1b76ec9eb5ef92345a0fcbd0fe27584a4ec279b6252da6304339b3faf10.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/ssh-simplified/s3_clnt_2_false-unreach-call_true-termination.cil.c, 01cac1b76ec9eb5ef92345a0fcbd0fe27584a4ec279b6252da6304339b3faf10
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/01cac1b76ec9eb5ef92345a0fcbd0fe27584a4ec279b6252da6304339b3faf10.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 22 witnesses for program sv-benchmarks/c/ssh-simplified/s3_clnt_2_false-unreach-call_true-termination.cil.c, 01cac1b76ec9eb5ef92345a0fcbd0fe27584a4ec279b6252da6304339b3faf10
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/01cac1b76ec9eb5ef92345a0fcbd0fe27584a4ec279b6252da6304339b3faf10.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
50a93da | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2018-12-08T10:40 CET (sv-comp) | ||
c4e7db3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | SMACK 1.9.3 | 12 | 2018-12-08T05:33:19 | ||
bab74bd | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Pinaka | 64 | 2018-12-07T15:44 CET (sv-comp) | ||
930cf9e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7 | 66 | 2018-12-10T18:41:42+01:00 | ||
3081eb7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 62 | 2018-12-08T00:07:59+01:00 | ||
684255c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 74 | 2018-12-10T20:38:19+01:00 | 930cf9e | |
d4cb15f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 74 | 2018-12-09T20:53:18+01:00 | b44613f | |
106d985 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 74 | 2018-12-09T20:37:39+01:00 | cf9bef6 | |
38ec1fd | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 75 | 2018-12-09T20:18:33+01:00 | 4930a71 | |
7db5891 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 77 | 2018-12-09T18:21:06+01:00 | c5edd50 | |
cb759cc | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 74 | 2018-12-08T23:44:09+01:00 | 50a93da | |
7fb24b8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 75 | 2018-12-08T22:09:55+01:00 | c4e7db3 | |
14dfccd | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 74 | 2018-12-08T09:01:12+01:00 | 3081eb7 | |
100dcff | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 90 | 2018-12-08T04:57:00+01:00 | e2653cb | |
236d510 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 96 | 2018-12-07T17:44:02+01:00 | bab74bd | |
2b07729 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 74 | 2018-12-06T10:18:12+01:00 | 9602f0e | |
d8b9804 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 74 | 2018-12-06T09:49:06+01:00 | 217bbd1 | |
fe4b0a4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 75 | 2018-12-06T09:19:27+01:00 | 8d15de6 | |
217bbd1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 62 | 2018-12-05T21:18:52+01:00 | ||
423f48e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 48 | 2018-12-06T09:42:09+01:00 | 6babddb | |
d9708fa | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 48 | 2018-12-06T09:05:35+01:00 | 9932a29 | |
4267fe8 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T13:12 CET (sv-comp) |
Found 18 witnesses for program sv-benchmarks/c/ssh-simplified/s3_clnt_2_false-unreach-call_true-termination.cil.c, 01cac1b76ec9eb5ef92345a0fcbd0fe27584a4ec279b6252da6304339b3faf10
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/01cac1b76ec9eb5ef92345a0fcbd0fe27584a4ec279b6252da6304339b3faf10.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
9ce677a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Taipan | 81 | 2017-12-02T16:41Z | ||
9ee76b6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2017-12-02T17:46 CET (sv-comp) | ||
9ccea61 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Kojak | 82 | 2017-12-02T13:53Z | ||
caf29c9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 kind | 9 | 2017-12-01T18:23:50.175024 | ||
24f1537 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 incr | 11 | 2017-12-01T08:19:31.575764 | ||
c7a5006 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 21 | 2017-12-01T20:44 CET (sv-comp) | ||
d66e2f8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 21 | 2017-11-30T17:20 CET (sv-comp) | ||
755fa33 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn | 66 | 2017-12-03T02:57:44+01:00 | ||
ecdf079 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 56 | 2017-11-30T15:33:02+01:00 | ||
7fd6172 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26758M | 88 | 2017-11-30T14:43:52+01:00 | ||
e0c5cb3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26725 | 44 | 2017-11-30T14:06:25+01:00 | ||
d27df32 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker (unknown version) | 31 | 2017-12-01T22:49:06+01:00 | ||
7f3bb32 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CBMC | 53 | 2017-11-30T13:05 CET (sv-comp) | ||
1836037 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Automizer | 81 | 2017-12-02T21:38Z | ||
3cc88e9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | 2LS | 56 | 2017-11-30T15:37 CET (sv-comp) | ||
732c9b3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-03T01:08:11.078106 | ||
1d9e0a5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T14:03:01.167857 | ||
3a27794 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 881 | 2017-12-01T16:08 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/ssh-simplified/s3_clnt_2_false-unreach-call_true-termination.cil.c, 01cac1b76ec9eb5ef92345a0fcbd0fe27584a4ec279b6252da6304339b3faf10
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/01cac1b76ec9eb5ef92345a0fcbd0fe27584a4ec279b6252da6304339b3faf10.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |