Witness Inspection
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).
View and Validate the Witness
Input Given to this Service about the Witness (URL Query)
Key |
Value |
programName |
sv-benchmarks/c/ldv-linux-3.4-simple/43_1a_cilled_false-unreach-call_ok_linux-43_1a-drivers--scsi--megaraid--megaraid_mm_true-termination.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i |
programSHA |
7022a341bad2e0f72c0094be9c8bd483e604a4d9b6ba72db9a338db48e7bf4b3 |
witnessName |
results-verified/cbmc.2018-12-04_2248.logfiles/sv-comp19_prop-reachsafety.43_1a_cilled_false-unreach-call_ok_linux-43_1a-drivers--scsi--megaraid--megaraid_mm_true-termination.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i.files/witness.graphml |
witnessSHA |
99ef1c60e42ddb38bf8aef2d08fa61d9e2353962f3d1590520ca78af3a18b04c |
Information about the Witness from Competition Database
from https://sv-comp.sosy-lab.org/2019/results/witnessInfoByHash/99ef1c60e42ddb38bf8aef2d08fa61d9e2353962f3d1590520ca78af3a18b04c.json
Key |
Value |
architecture |
64bit |
creationtime |
2018-12-06T06:38 CET (sv-comp) |
producer |
CBMC |
programfile |
../../sv-benchmarks/c/ldv-linux-3.4-simple/43_1a_cilled_false-unreach-call_ok_linux-43_1a-drivers--scsi--megaraid--megaraid_mm_true-termination.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i |
programhash |
90db1cc862a9efa687a191b3fe57706f106efbbc |
sourcecodelang |
C |
specification |
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file |
witnessFileByHash/99ef1c60e42ddb38bf8aef2d08fa61d9e2353962f3d1590520ca78af3a18b04c.graphml |
witness-sha256 |
99ef1c60e42ddb38bf8aef2d08fa61d9e2353962f3d1590520ca78af3a18b04c |
witness-size |
224246 |
witness-type |
violation_witness |
Available Results for the Program from Witness Store SV-COMP '24
Trying to find witnesses for program (7022a341bad2e0f72c0094be9c8bd483e604a4d9b6ba72db9a338db48e7bf4b3, sv-benchmarks/c/ldv-linux-3.4-simple/43_1a_cilled_false-unreach-call_ok_linux-43_1a-drivers--scsi--megaraid--megaraid_mm_true-termination.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i).
Found 0 witnesses for program sv-benchmarks/c/ldv-linux-3.4-simple/43_1a_cilled_false-unreach-call_ok_linux-43_1a-drivers--scsi--megaraid--megaraid_mm_true-termination.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i, 7022a341bad2e0f72c0094be9c8bd483e604a4d9b6ba72db9a338db48e7bf4b3
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/7022a341bad2e0f72c0094be9c8bd483e604a4d9b6ba72db9a338db48e7bf4b3.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
Available Results for the Program from Witness Store SV-COMP '23
Trying to find witnesses for program (7022a341bad2e0f72c0094be9c8bd483e604a4d9b6ba72db9a338db48e7bf4b3, sv-benchmarks/c/ldv-linux-3.4-simple/43_1a_cilled_false-unreach-call_ok_linux-43_1a-drivers--scsi--megaraid--megaraid_mm_true-termination.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i).
Found 0 witnesses for program sv-benchmarks/c/ldv-linux-3.4-simple/43_1a_cilled_false-unreach-call_ok_linux-43_1a-drivers--scsi--megaraid--megaraid_mm_true-termination.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i, 7022a341bad2e0f72c0094be9c8bd483e604a4d9b6ba72db9a338db48e7bf4b3
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/7022a341bad2e0f72c0094be9c8bd483e604a4d9b6ba72db9a338db48e7bf4b3.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
Available Results for the Program from Witness Store SV-COMP '22
Trying to find witnesses for program (7022a341bad2e0f72c0094be9c8bd483e604a4d9b6ba72db9a338db48e7bf4b3, sv-benchmarks/c/ldv-linux-3.4-simple/43_1a_cilled_false-unreach-call_ok_linux-43_1a-drivers--scsi--megaraid--megaraid_mm_true-termination.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i).
Found 0 witnesses for program sv-benchmarks/c/ldv-linux-3.4-simple/43_1a_cilled_false-unreach-call_ok_linux-43_1a-drivers--scsi--megaraid--megaraid_mm_true-termination.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i, 7022a341bad2e0f72c0094be9c8bd483e604a4d9b6ba72db9a338db48e7bf4b3
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/7022a341bad2e0f72c0094be9c8bd483e604a4d9b6ba72db9a338db48e7bf4b3.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
Available Results for the Program from Witness Store SV-COMP '21
Trying to find witnesses for program (7022a341bad2e0f72c0094be9c8bd483e604a4d9b6ba72db9a338db48e7bf4b3, sv-benchmarks/c/ldv-linux-3.4-simple/43_1a_cilled_false-unreach-call_ok_linux-43_1a-drivers--scsi--megaraid--megaraid_mm_true-termination.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i).
Found 0 witnesses for program sv-benchmarks/c/ldv-linux-3.4-simple/43_1a_cilled_false-unreach-call_ok_linux-43_1a-drivers--scsi--megaraid--megaraid_mm_true-termination.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i, 7022a341bad2e0f72c0094be9c8bd483e604a4d9b6ba72db9a338db48e7bf4b3
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/7022a341bad2e0f72c0094be9c8bd483e604a4d9b6ba72db9a338db48e7bf4b3.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
Available Results for the Program from Witness Store SV-COMP '20
Trying to find witnesses for program (7022a341bad2e0f72c0094be9c8bd483e604a4d9b6ba72db9a338db48e7bf4b3, sv-benchmarks/c/ldv-linux-3.4-simple/43_1a_cilled_false-unreach-call_ok_linux-43_1a-drivers--scsi--megaraid--megaraid_mm_true-termination.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i).
Found 0 witnesses for program sv-benchmarks/c/ldv-linux-3.4-simple/43_1a_cilled_false-unreach-call_ok_linux-43_1a-drivers--scsi--megaraid--megaraid_mm_true-termination.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i, 7022a341bad2e0f72c0094be9c8bd483e604a4d9b6ba72db9a338db48e7bf4b3
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/7022a341bad2e0f72c0094be9c8bd483e604a4d9b6ba72db9a338db48e7bf4b3.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
Available Results for the Program from Witness Store SV-COMP '19
Trying to find witnesses for program (7022a341bad2e0f72c0094be9c8bd483e604a4d9b6ba72db9a338db48e7bf4b3, sv-benchmarks/c/ldv-linux-3.4-simple/43_1a_cilled_false-unreach-call_ok_linux-43_1a-drivers--scsi--megaraid--megaraid_mm_true-termination.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i).
Found 9 witnesses for program sv-benchmarks/c/ldv-linux-3.4-simple/43_1a_cilled_false-unreach-call_ok_linux-43_1a-drivers--scsi--megaraid--megaraid_mm_true-termination.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i, 7022a341bad2e0f72c0094be9c8bd483e604a4d9b6ba72db9a338db48e7bf4b3
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/7022a341bad2e0f72c0094be9c8bd483e604a4d9b6ba72db9a338db48e7bf4b3.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
1e192ba |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
SMACK 1.9.3 |
64 |
2018-12-08T07:48:41 |
|
e27ef03 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7 |
223 |
2018-12-10T17:21:54+01:00 |
|
b2d046f |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn b8d6131600+ |
196 |
2018-12-07T21:55:11+01:00 |
|
7184fba |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
224 |
2018-12-05T15:48:05+01:00 |
162d915 |
162d915 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29794 |
132 |
2018-12-05T04:27:23+01:00 |
|
3d7c655 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
179 |
2018-12-10T20:35:06+01:00 |
e27ef03 |
56353d4 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
179 |
2018-12-08T09:00:56+01:00 |
b2d046f |
4ccf138 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
178 |
2018-12-08T04:55:25+01:00 |
1416749 |
582bd0e |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
178 |
2018-12-06T09:18:27+01:00 |
99ef1c6 |
Available Results for the Program from Witness Store SV-COMP '18
Trying to find witnesses for program (7022a341bad2e0f72c0094be9c8bd483e604a4d9b6ba72db9a338db48e7bf4b3, sv-benchmarks/c/ldv-linux-3.4-simple/43_1a_cilled_false-unreach-call_ok_linux-43_1a-drivers--scsi--megaraid--megaraid_mm_true-termination.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i).
Found 0 witnesses for program sv-benchmarks/c/ldv-linux-3.4-simple/43_1a_cilled_false-unreach-call_ok_linux-43_1a-drivers--scsi--megaraid--megaraid_mm_true-termination.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i, 7022a341bad2e0f72c0094be9c8bd483e604a4d9b6ba72db9a338db48e7bf4b3
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/7022a341bad2e0f72c0094be9c8bd483e604a4d9b6ba72db9a338db48e7bf4b3.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
Available Results for the Program from Witness Store SV-COMP '17
Trying to find witnesses for program (7022a341bad2e0f72c0094be9c8bd483e604a4d9b6ba72db9a338db48e7bf4b3, sv-benchmarks/c/ldv-linux-3.4-simple/43_1a_cilled_false-unreach-call_ok_linux-43_1a-drivers--scsi--megaraid--megaraid_mm_true-termination.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i).
Found 0 witnesses for program sv-benchmarks/c/ldv-linux-3.4-simple/43_1a_cilled_false-unreach-call_ok_linux-43_1a-drivers--scsi--megaraid--megaraid_mm_true-termination.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i, 7022a341bad2e0f72c0094be9c8bd483e604a4d9b6ba72db9a338db48e7bf4b3
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/7022a341bad2e0f72c0094be9c8bd483e604a4d9b6ba72db9a338db48e7bf4b3.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |