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/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--cpufreq--pcc-cpufreq.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c |
programSHA |
19c1eb6780e43bee7cdaa84a012534fbca1151c420b1c9f938213d69a1d386cb |
witnessName |
results-verified/utaipan.2017-12-02_1723.logfiles/sv-comp18.32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--cpufreq--pcc-cpufreq.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.files/witness.graphml |
witnessSHA |
731be02bfc91978146bad4362c6fdf6a15c8a7fd4c3ba0e03f8c52f49baa87d6 |
Information about the Witness from Competition Database
from https://sv-comp.sosy-lab.org/2018/results/witnessInfoByHash/731be02bfc91978146bad4362c6fdf6a15c8a7fd4c3ba0e03f8c52f49baa87d6.json
Key |
Value |
architecture |
64bit |
creationtime |
2017-12-02T19:16Z |
producer |
Taipan |
program-sha256 |
19c1eb6780e43bee7cdaa84a012534fbca1151c420b1c9f938213d69a1d386cb |
programfile |
/tmp/vcloud-vcloud-master/worker/working_dir_8a0f0324-daf0-4b66-8d66-5715263ae055/sv-benchmarks/c/ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--cpufreq--pcc-cpufreq.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c |
programhash |
2a6eeec2c649170f3a6ab7f2bdf1c9b03783df8f |
sourcecodelang |
C |
specification |
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
|
witness-file |
witnessFileByHash/731be02bfc91978146bad4362c6fdf6a15c8a7fd4c3ba0e03f8c52f49baa87d6.graphml |
witness-sha256 |
731be02bfc91978146bad4362c6fdf6a15c8a7fd4c3ba0e03f8c52f49baa87d6 |
witness-size |
306917 |
witness-type |
correctness_witness |
Available Results for the Program from Witness Store SV-COMP '24
Trying to find witnesses for program (19c1eb6780e43bee7cdaa84a012534fbca1151c420b1c9f938213d69a1d386cb, sv-benchmarks/c/ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--cpufreq--pcc-cpufreq.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c).
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--cpufreq--pcc-cpufreq.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c, 19c1eb6780e43bee7cdaa84a012534fbca1151c420b1c9f938213d69a1d386cb
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/19c1eb6780e43bee7cdaa84a012534fbca1151c420b1c9f938213d69a1d386cb.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 (19c1eb6780e43bee7cdaa84a012534fbca1151c420b1c9f938213d69a1d386cb, sv-benchmarks/c/ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--cpufreq--pcc-cpufreq.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c).
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--cpufreq--pcc-cpufreq.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c, 19c1eb6780e43bee7cdaa84a012534fbca1151c420b1c9f938213d69a1d386cb
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/19c1eb6780e43bee7cdaa84a012534fbca1151c420b1c9f938213d69a1d386cb.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 (19c1eb6780e43bee7cdaa84a012534fbca1151c420b1c9f938213d69a1d386cb, sv-benchmarks/c/ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--cpufreq--pcc-cpufreq.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c).
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--cpufreq--pcc-cpufreq.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c, 19c1eb6780e43bee7cdaa84a012534fbca1151c420b1c9f938213d69a1d386cb
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/19c1eb6780e43bee7cdaa84a012534fbca1151c420b1c9f938213d69a1d386cb.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 (19c1eb6780e43bee7cdaa84a012534fbca1151c420b1c9f938213d69a1d386cb, sv-benchmarks/c/ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--cpufreq--pcc-cpufreq.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c).
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--cpufreq--pcc-cpufreq.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c, 19c1eb6780e43bee7cdaa84a012534fbca1151c420b1c9f938213d69a1d386cb
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/19c1eb6780e43bee7cdaa84a012534fbca1151c420b1c9f938213d69a1d386cb.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 (19c1eb6780e43bee7cdaa84a012534fbca1151c420b1c9f938213d69a1d386cb, sv-benchmarks/c/ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--cpufreq--pcc-cpufreq.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c).
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--cpufreq--pcc-cpufreq.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c, 19c1eb6780e43bee7cdaa84a012534fbca1151c420b1c9f938213d69a1d386cb
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/19c1eb6780e43bee7cdaa84a012534fbca1151c420b1c9f938213d69a1d386cb.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 (19c1eb6780e43bee7cdaa84a012534fbca1151c420b1c9f938213d69a1d386cb, sv-benchmarks/c/ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--cpufreq--pcc-cpufreq.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c).
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--cpufreq--pcc-cpufreq.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c, 19c1eb6780e43bee7cdaa84a012534fbca1151c420b1c9f938213d69a1d386cb
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/19c1eb6780e43bee7cdaa84a012534fbca1151c420b1c9f938213d69a1d386cb.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 '18
Trying to find witnesses for program (19c1eb6780e43bee7cdaa84a012534fbca1151c420b1c9f938213d69a1d386cb, sv-benchmarks/c/ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--cpufreq--pcc-cpufreq.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c).
Found 9 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--cpufreq--pcc-cpufreq.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c, 19c1eb6780e43bee7cdaa84a012534fbca1151c420b1c9f938213d69a1d386cb
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/19c1eb6780e43bee7cdaa84a012534fbca1151c420b1c9f938213d69a1d386cb.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
731be02 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
Taipan |
307 |
2017-12-02T19:16Z |
|
4e50fc8 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
ESBMC 4.6.0 kind |
4 |
2017-12-01T21:57:03.619497 |
|
e8204fe |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.6.1-svn |
4 |
2017-11-30T23:54:47+01:00 |
|
814be04 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.6.1-svn 26773 |
78 |
2017-12-01T06:04:15+01:00 |
8a68781 |
656b08a |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.6.1-svn 26773 |
78 |
2017-11-30T19:58:13+01:00 |
|
d8e34d0 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.6.1-svn 26758M |
24 |
2017-11-30T14:19:47+01:00 |
|
832de62 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.6.1-svn 26725 |
74 |
2017-11-30T18:54:03+01:00 |
|
0b38403 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker (unknown version) |
35 |
2017-12-01T19:19:37+01:00 |
|
0d87c33 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
Automizer |
307 |
2017-12-02T01:08Z |
|
Available Results for the Program from Witness Store SV-COMP '17
Trying to find witnesses for program (19c1eb6780e43bee7cdaa84a012534fbca1151c420b1c9f938213d69a1d386cb, sv-benchmarks/c/ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--cpufreq--pcc-cpufreq.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c).
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--cpufreq--pcc-cpufreq.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c, 19c1eb6780e43bee7cdaa84a012534fbca1151c420b1c9f938213d69a1d386cb
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/19c1eb6780e43bee7cdaa84a012534fbca1151c420b1c9f938213d69a1d386cb.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |