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--gpu--drm--i2c--sil164.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c |
programSHA | 4534796805ca370b4ea1fd0c385e2122775dc6dea89c2293e6c87029b0229b81 |
witnessName | results-verified/cpa-seq.2017-11-30_1120.logfiles/sv-comp18.32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--gpu--drm--i2c--sil164.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.files/witness.graphml |
witnessSHA | a6913d7fb2e013ae86de9f445ba744e1b52831bf22fa77cdeec5e43272972782 |
Key | Value |
architecture | 64bit |
creationtime | 2017-11-30T16:17:24+01:00 |
producer | CPAchecker 1.6.1-svn 26773 |
program-sha256 | 4534796805ca370b4ea1fd0c385e2122775dc6dea89c2293e6c87029b0229b81 |
programfile | ../../sv-benchmarks/c/ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--gpu--drm--i2c--sil164.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c |
programhash | 7751ba17d43764b0c21a621e1cdadc91c0bab864 |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/a6913d7fb2e013ae86de9f445ba744e1b52831bf22fa77cdeec5e43272972782.graphml |
witness-sha256 | a6913d7fb2e013ae86de9f445ba744e1b52831bf22fa77cdeec5e43272972782 |
witness-size | 76794 |
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--gpu--drm--i2c--sil164.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c, 4534796805ca370b4ea1fd0c385e2122775dc6dea89c2293e6c87029b0229b81
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/4534796805ca370b4ea1fd0c385e2122775dc6dea89c2293e6c87029b0229b81.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--gpu--drm--i2c--sil164.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c, 4534796805ca370b4ea1fd0c385e2122775dc6dea89c2293e6c87029b0229b81
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/4534796805ca370b4ea1fd0c385e2122775dc6dea89c2293e6c87029b0229b81.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--gpu--drm--i2c--sil164.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c, 4534796805ca370b4ea1fd0c385e2122775dc6dea89c2293e6c87029b0229b81
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/4534796805ca370b4ea1fd0c385e2122775dc6dea89c2293e6c87029b0229b81.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--gpu--drm--i2c--sil164.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c, 4534796805ca370b4ea1fd0c385e2122775dc6dea89c2293e6c87029b0229b81
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/4534796805ca370b4ea1fd0c385e2122775dc6dea89c2293e6c87029b0229b81.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--gpu--drm--i2c--sil164.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c, 4534796805ca370b4ea1fd0c385e2122775dc6dea89c2293e6c87029b0229b81
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/4534796805ca370b4ea1fd0c385e2122775dc6dea89c2293e6c87029b0229b81.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--gpu--drm--i2c--sil164.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c, 4534796805ca370b4ea1fd0c385e2122775dc6dea89c2293e6c87029b0229b81
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/4534796805ca370b4ea1fd0c385e2122775dc6dea89c2293e6c87029b0229b81.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--gpu--drm--i2c--sil164.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c, 4534796805ca370b4ea1fd0c385e2122775dc6dea89c2293e6c87029b0229b81
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/4534796805ca370b4ea1fd0c385e2122775dc6dea89c2293e6c87029b0229b81.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
5668064 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Taipan | 280 | 2017-12-03T03:17Z | ||
4c3171c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Kojak | 280 | 2017-12-02T21:07Z | ||
f4a7a5c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 kind | 4 | 2017-12-01T15:16:06.437696 | ||
d710f47 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 76 | 2017-12-03T07:11:46+01:00 | e15656a | |
dae275f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 76 | 2017-12-03T01:38:12+01:00 | 436ea99 | |
5b6dc89 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 76 | 2017-12-02T23:36:28+01:00 | 997b97a | |
b4df138 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 76 | 2017-12-02T08:13:30+01:00 | 0d910f7 | |
ad1a479 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 76 | 2017-12-01T06:41:18+01:00 | 98276c2 | |
8c9a4c0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 76 | 2017-12-01T06:05:57+01:00 | 0c31606 | |
d3ff8f9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 77 | 2017-12-01T05:48:06+01:00 | e78b18b | |
a6913d7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 77 | 2017-11-30T16:17:24+01:00 | ||
de737c7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26758M | 18 | 2017-11-30T18:45:56+01:00 | ||
f2fb4bf | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26725 | 76 | 2017-11-30T19:06:47+01:00 | ||
fdd4e98 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker (unknown version) | 62 | 2017-12-02T11:36:03+01:00 | ||
c7a65b0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Automizer | 280 | 2017-12-02T07:13Z |
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--gpu--drm--i2c--sil164.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c, 4534796805ca370b4ea1fd0c385e2122775dc6dea89c2293e6c87029b0229b81
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/4534796805ca370b4ea1fd0c385e2122775dc6dea89c2293e6c87029b0229b81.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |