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_srvr_8_true-unreach-call_false-termination.cil.c |
programSHA | 8d64c9d16fdea339d1dbb0e88b673c88f90daad93b5297dd97d50576a501af66 |
witnessName | results-verified/cpa-seq.2017-11-30_1120.logfiles/sv-comp18.s3_srvr_8_true-unreach-call_false-termination.cil.c.files/witness.graphml |
witnessSHA | cc7d758ddb0b4a016a95c8bdb40bf64a0dee64e5d757e1e72a6480fb839c1a12 |
Key | Value |
architecture | 32bit |
creationtime | 2017-12-01T00:40:44+01:00 |
producer | CPAchecker 1.6.1-svn 26773 |
program-sha256 | 8d64c9d16fdea339d1dbb0e88b673c88f90daad93b5297dd97d50576a501af66 |
programfile | ../../sv-benchmarks/c/ssh-simplified/s3_srvr_8_true-unreach-call_false-termination.cil.c |
programhash | 0e3531ca2da4bd0098c9a389bd0b7db6a2819ab0 |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/cc7d758ddb0b4a016a95c8bdb40bf64a0dee64e5d757e1e72a6480fb839c1a12.graphml |
witness-sha256 | cc7d758ddb0b4a016a95c8bdb40bf64a0dee64e5d757e1e72a6480fb839c1a12 |
witness-size | 56987 |
witness-type | correctness_witness |
Found 0 witnesses for program sv-benchmarks/c/ssh-simplified/s3_srvr_8_true-unreach-call_false-termination.cil.c, 8d64c9d16fdea339d1dbb0e88b673c88f90daad93b5297dd97d50576a501af66
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/8d64c9d16fdea339d1dbb0e88b673c88f90daad93b5297dd97d50576a501af66.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_srvr_8_true-unreach-call_false-termination.cil.c, 8d64c9d16fdea339d1dbb0e88b673c88f90daad93b5297dd97d50576a501af66
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/8d64c9d16fdea339d1dbb0e88b673c88f90daad93b5297dd97d50576a501af66.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_srvr_8_true-unreach-call_false-termination.cil.c, 8d64c9d16fdea339d1dbb0e88b673c88f90daad93b5297dd97d50576a501af66
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/8d64c9d16fdea339d1dbb0e88b673c88f90daad93b5297dd97d50576a501af66.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_srvr_8_true-unreach-call_false-termination.cil.c, 8d64c9d16fdea339d1dbb0e88b673c88f90daad93b5297dd97d50576a501af66
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/8d64c9d16fdea339d1dbb0e88b673c88f90daad93b5297dd97d50576a501af66.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_srvr_8_true-unreach-call_false-termination.cil.c, 8d64c9d16fdea339d1dbb0e88b673c88f90daad93b5297dd97d50576a501af66
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/8d64c9d16fdea339d1dbb0e88b673c88f90daad93b5297dd97d50576a501af66.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 9 witnesses for program sv-benchmarks/c/ssh-simplified/s3_srvr_8_true-unreach-call_false-termination.cil.c, 8d64c9d16fdea339d1dbb0e88b673c88f90daad93b5297dd97d50576a501af66
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/8d64c9d16fdea339d1dbb0e88b673c88f90daad93b5297dd97d50576a501af66.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
268b960 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | SMACK 1.9.3 | 3 | 2018-12-08T10:57:04 | ||
506587b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 57 | 2018-12-07T06:08:47+01:00 | ||
de19578 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 57 | 2018-12-09T20:38:21+01:00 | 75e4500 | |
32201e8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 57 | 2018-12-09T17:50:31+01:00 | 29cd156 | |
5063768 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 57 | 2018-12-08T21:47:10+01:00 | 268b960 | |
12ec363 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 57 | 2018-12-08T07:11:23+01:00 | 506587b | |
b2d4edc | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 57 | 2018-12-06T09:02:24+01:00 | 91d0e32 | |
91d0e32 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 57 | 2018-12-05T13:01:18+01:00 | ||
762b6e1 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn 29852 | 163 | 2018-12-06T06:55:45+01:00 |
Found 14 witnesses for program sv-benchmarks/c/ssh-simplified/s3_srvr_8_true-unreach-call_false-termination.cil.c, 8d64c9d16fdea339d1dbb0e88b673c88f90daad93b5297dd97d50576a501af66
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/8d64c9d16fdea339d1dbb0e88b673c88f90daad93b5297dd97d50576a501af66.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
7f03c51 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn | 4 | 2017-11-30T18:04:52+01:00 | ||
2ba4126 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 57 | 2017-12-03T00:44:03+01:00 | 8737191 | |
3eeceb7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 57 | 2017-12-02T15:45:22+01:00 | 31ad7f4 | |
0d9080a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 57 | 2017-12-01T08:28:10+01:00 | 8cc791d | |
e6792ee | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 57 | 2017-12-01T07:23:43+01:00 | 6a26937 | |
ae612c6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 57 | 2017-12-01T06:09:12+01:00 | e646d73 | |
2c5f7cd | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 57 | 2017-12-01T04:45:12+01:00 | 8499fd8 | |
cc7d758 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 57 | 2017-12-01T00:40:44+01:00 | ||
c692a83 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26758M | 58 | 2017-11-30T18:51:40+01:00 | ||
af1c991 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26725 | 57 | 2017-11-30T13:25:53+01:00 | ||
764814f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker (unknown version) | 50 | 2017-12-01T21:31:57+01:00 | ||
4a00998 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Automizer | 104 | 2017-12-02T09:57Z | ||
aea23aa | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | Automizer | 136 | 2017-12-03T11:12Z | ||
93f3ea8 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | 2LS | 96 | 2017-12-01T17:08 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/ssh-simplified/s3_srvr_8_true-unreach-call_false-termination.cil.c, 8d64c9d16fdea339d1dbb0e88b673c88f90daad93b5297dd97d50576a501af66
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/8d64c9d16fdea339d1dbb0e88b673c88f90daad93b5297dd97d50576a501af66.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |