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/list-simple/sll2c_insert_equal_true-unreach-call_true-valid-memsafety.i |
programSHA | b912799ef1236943571630d12117bbcf483be0e2eb4ab78e05fb132fa4f4cfb8 |
witnessName | results-verified/symbiotic.2018-12-07_2142.logfiles/sv-comp19_prop-memsafety.sll2c_insert_equal_true-unreach-call_true-valid-memsafety.i.files/witness.graphml |
witnessSHA | ae097adb8daeea1972c4f89a8a1c36ef99db33d4ab8fded5b6c1abcc61f9f939 |
Key | Value |
architecture | 32bit |
creationtime | 2018-12-08T12:21 CET (sv-comp) |
producer | Symbiotic |
program-sha256 | b912799ef1236943571630d12117bbcf483be0e2eb4ab78e05fb132fa4f4cfb8 |
programfile | /tmp/vcloud-vcloud-master/worker/working_dir_b3e7c48a-3185-48c4-a27e-0f388b39585d/sv-benchmarks/c/list-simple/sll2c_insert_equal_true-unreach-call_true-valid-memsafety.i |
programhash | b912799ef1236943571630d12117bbcf483be0e2eb4ab78e05fb132fa4f4cfb8 |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G valid-memtrack) ) |
witness-file | witnessFileByHash/ae097adb8daeea1972c4f89a8a1c36ef99db33d4ab8fded5b6c1abcc61f9f939.graphml |
witness-sha256 | ae097adb8daeea1972c4f89a8a1c36ef99db33d4ab8fded5b6c1abcc61f9f939 |
witness-size | 940 |
witness-type | correctness_witness |
This witness was created for this program (cf. table above, b912799ef1236943571630d12117bbcf483be0e2eb4ab78e05fb132fa4f4cfb8).
Found 0 witnesses for program sv-benchmarks/c/list-simple/sll2c_insert_equal_true-unreach-call_true-valid-memsafety.i, b912799ef1236943571630d12117bbcf483be0e2eb4ab78e05fb132fa4f4cfb8
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/b912799ef1236943571630d12117bbcf483be0e2eb4ab78e05fb132fa4f4cfb8.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/list-simple/sll2c_insert_equal_true-unreach-call_true-valid-memsafety.i, b912799ef1236943571630d12117bbcf483be0e2eb4ab78e05fb132fa4f4cfb8
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/b912799ef1236943571630d12117bbcf483be0e2eb4ab78e05fb132fa4f4cfb8.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/list-simple/sll2c_insert_equal_true-unreach-call_true-valid-memsafety.i, b912799ef1236943571630d12117bbcf483be0e2eb4ab78e05fb132fa4f4cfb8
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/b912799ef1236943571630d12117bbcf483be0e2eb4ab78e05fb132fa4f4cfb8.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/list-simple/sll2c_insert_equal_true-unreach-call_true-valid-memsafety.i, b912799ef1236943571630d12117bbcf483be0e2eb4ab78e05fb132fa4f4cfb8
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/b912799ef1236943571630d12117bbcf483be0e2eb4ab78e05fb132fa4f4cfb8.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 17 witnesses for program sv-benchmarks/c/list-simple/sll2c_insert_equal_true-unreach-call_true-valid-memsafety.i, b912799ef1236943571630d12117bbcf483be0e2eb4ab78e05fb132fa4f4cfb8
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/b912799ef1236943571630d12117bbcf483be0e2eb4ab78e05fb132fa4f4cfb8.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
7b86a45 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 1.9 | 14 | 2019-11-29T19:01:28+01:00 | ||
f6d0080 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 14 | 2019-12-01T01:50:54+01:00 | ||
a76e9ba | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Pinaka | 3 | 2019-12-04T00:03 CET (comp) | ||
c2c9be9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 14 | 2019-12-11T20:29:05+01:00 | 543e7f6 | |
11463b6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 14 | 2019-12-11T20:22:28+01:00 | 6c351b0 | |
3ae9efb | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 14 | 2019-12-11T20:17:25+01:00 | 305ea29 | |
c78bdac | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 14 | 2019-12-08T01:03:38+01:00 | 8774d53 | |
4f3434a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 14 | 2019-12-08T00:00:04+01:00 | 0126c50 | |
0dc2a21 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 14 | 2019-12-07T20:01:35+01:00 | 687b291 | |
19a3beb | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 14 | 2019-12-06T02:16:26+01:00 | 3c0c11a | |
69a484e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 14 | 2019-12-05T19:28:00+01:00 | 5173b53 | |
4fbcbf3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 14 | 2019-12-04T02:22:27+01:00 | a76e9ba | |
de5f83a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 14 | 2019-11-30T19:25:43+01:00 | 63c7fe4 | |
8e65961 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 14 | 2019-11-30T17:19:32+01:00 | 3fd2ebf | |
3fd2ebf | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / svcomp20 | 17 | 2019-11-30T02:38:41+01:00 | ||
8774d53 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.8 | 16 | 2019-12-07T15:04:57+01:00 | ||
6c351b0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco | 14 | 2019-11-30T20:27:43+01:00 |
Found 22 witnesses for program sv-benchmarks/c/list-simple/sll2c_insert_equal_true-unreach-call_true-valid-memsafety.i, b912799ef1236943571630d12117bbcf483be0e2eb4ab78e05fb132fa4f4cfb8
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/b912799ef1236943571630d12117bbcf483be0e2eb4ab78e05fb132fa4f4cfb8.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
ae097ad | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T12:21 CET (sv-comp) | ||
400c0c2 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 14 | 2018-12-07T00:09:01+01:00 | ||
f783fc5 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 14 | 2018-12-06T02:18:46+01:00 | ||
5b5210e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T12:14 CET (sv-comp) | ||
89442db | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | SMACK 1.9.3 | 3 | 2018-12-08T12:06:35 | ||
678a97d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Pinaka | 3 | 2018-12-07T05:41 CET (sv-comp) | ||
4ed4b9e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7 | 15 | 2018-12-10T17:05:17+01:00 | ||
489d27b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 17 | 2018-12-08T01:47:48+01:00 | ||
5e59f39 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 15 | 2018-12-10T19:37:51+01:00 | 4ed4b9e | |
c8135f2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 14 | 2018-12-10T10:30:42+01:00 | aa940d1 | |
a4b03ab | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 14 | 2018-12-08T23:20:59+01:00 | 5b5210e | |
6fa8254 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 14 | 2018-12-08T21:38:30+01:00 | 89442db | |
dda91a0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 14 | 2018-12-08T05:14:24+01:00 | 489d27b | |
835002d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 14 | 2018-12-08T04:26:10+01:00 | ddc63de | |
6e724ae | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 14 | 2018-12-08T03:11:05+01:00 | aa940d1 | |
e540c86 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 14 | 2018-12-07T16:38:49+01:00 | 678a97d | |
6cafc79 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 14 | 2018-12-07T08:40:30+01:00 | f22f1ea | |
43b8741 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 14 | 2018-12-06T09:28:21+01:00 | a10fba7 | |
5f3c33a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 14 | 2018-12-06T08:45:26+01:00 | 996485f | |
08c214f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 14 | 2018-12-06T07:55:27+01:00 | b910c1b | |
a9e935d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 14 | 2018-12-06T07:42:25+01:00 | aba835d | |
996485f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 17 | 2018-12-06T07:25:27+01:00 |
Found 0 witnesses for program sv-benchmarks/c/list-simple/sll2c_insert_equal_true-unreach-call_true-valid-memsafety.i, b912799ef1236943571630d12117bbcf483be0e2eb4ab78e05fb132fa4f4cfb8
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/b912799ef1236943571630d12117bbcf483be0e2eb4ab78e05fb132fa4f4cfb8.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/list-simple/sll2c_insert_equal_true-unreach-call_true-valid-memsafety.i, b912799ef1236943571630d12117bbcf483be0e2eb4ab78e05fb132fa4f4cfb8
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/b912799ef1236943571630d12117bbcf483be0e2eb4ab78e05fb132fa4f4cfb8.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |