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/ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--block--paride--fit2.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i |
programSHA | f26f6c3f2c1fbccdfb17bf2bd106ab190786e5892f771d5bc987efadf2f0cdc9 |
witnessName | results-verified/utaipan.2018-12-08_1419.logfiles/sv-comp19_prop-reachsafety.32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--block--paride--fit2.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i.files/witness.graphml |
witnessSHA | 11c2588c9383b1633a8420e2f78d78b9deabd52d2cf24696e1c21cd79dcf49d0 |
Key | Value |
architecture | 64bit |
creationtime | 2018-12-08T16:03Z |
producer | Taipan |
programfile | /tmp/vcloud-vcloud-master/worker/working_dir_1cf4a95d-ff33-4cf3-bb32-26b22e343136/sv-benchmarks/c/ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--block--paride--fit2.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i |
programhash | b855770f0efb4e17edfb1c6f0c0ea7a8c0570c4f |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/11c2588c9383b1633a8420e2f78d78b9deabd52d2cf24696e1c21cd79dcf49d0.graphml |
witness-sha256 | 11c2588c9383b1633a8420e2f78d78b9deabd52d2cf24696e1c21cd79dcf49d0 |
witness-size | 413191 |
witness-type | correctness_witness |
Found 0 witnesses for program sv-benchmarks/c/ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--block--paride--fit2.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i, f26f6c3f2c1fbccdfb17bf2bd106ab190786e5892f771d5bc987efadf2f0cdc9
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/f26f6c3f2c1fbccdfb17bf2bd106ab190786e5892f771d5bc987efadf2f0cdc9.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--block--paride--fit2.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i, f26f6c3f2c1fbccdfb17bf2bd106ab190786e5892f771d5bc987efadf2f0cdc9
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/f26f6c3f2c1fbccdfb17bf2bd106ab190786e5892f771d5bc987efadf2f0cdc9.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--block--paride--fit2.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i, f26f6c3f2c1fbccdfb17bf2bd106ab190786e5892f771d5bc987efadf2f0cdc9
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/f26f6c3f2c1fbccdfb17bf2bd106ab190786e5892f771d5bc987efadf2f0cdc9.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--block--paride--fit2.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i, f26f6c3f2c1fbccdfb17bf2bd106ab190786e5892f771d5bc987efadf2f0cdc9
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/f26f6c3f2c1fbccdfb17bf2bd106ab190786e5892f771d5bc987efadf2f0cdc9.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--block--paride--fit2.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i, f26f6c3f2c1fbccdfb17bf2bd106ab190786e5892f771d5bc987efadf2f0cdc9
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/f26f6c3f2c1fbccdfb17bf2bd106ab190786e5892f771d5bc987efadf2f0cdc9.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 15 witnesses for program sv-benchmarks/c/ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--block--paride--fit2.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i, f26f6c3f2c1fbccdfb17bf2bd106ab190786e5892f771d5bc987efadf2f0cdc9
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/f26f6c3f2c1fbccdfb17bf2bd106ab190786e5892f771d5bc987efadf2f0cdc9.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
74b86a8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T03:45 CET (sv-comp) | ||
3fb5731 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | SMACK 1.9.3 | 3 | 2018-12-08T01:34:22 | ||
aed1209 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 105 | 2018-12-07T23:31:52+01:00 | ||
cd07714 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 105 | 2018-12-10T20:02:24+01:00 | 416cd7f | |
c208bee | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 105 | 2018-12-09T20:33:05+01:00 | 11c2588 | |
63b72b2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 105 | 2018-12-09T19:58:55+01:00 | d708a0a | |
584cf1d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 105 | 2018-12-09T17:37:21+01:00 | e16ee4a | |
cb89091 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 105 | 2018-12-08T23:27:45+01:00 | 74b86a8 | |
5211431 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 105 | 2018-12-08T21:56:26+01:00 | 3fb5731 | |
2c0986b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 105 | 2018-12-08T05:59:55+01:00 | aed1209 | |
5fb9b73 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 105 | 2018-12-08T02:36:04+01:00 | 8b587e5 | |
d28e232 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 105 | 2018-12-06T09:00:18+01:00 | 9cbd64e | |
9cbd64e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 105 | 2018-12-06T07:41:27+01:00 | ||
a4031e5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 105 | 2018-12-05T14:59:39+01:00 | 5941b20 | |
5941b20 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29794 | 198 | 2018-12-05T10:46:24+01:00 |
Found 0 witnesses for program sv-benchmarks/c/ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--block--paride--fit2.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i, f26f6c3f2c1fbccdfb17bf2bd106ab190786e5892f771d5bc987efadf2f0cdc9
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/f26f6c3f2c1fbccdfb17bf2bd106ab190786e5892f771d5bc987efadf2f0cdc9.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--block--paride--fit2.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i, f26f6c3f2c1fbccdfb17bf2bd106ab190786e5892f771d5bc987efadf2f0cdc9
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/f26f6c3f2c1fbccdfb17bf2bd106ab190786e5892f771d5bc987efadf2f0cdc9.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |