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 |
../../../comp/sv-benchmarks/c/reducercommutativity/sep_true-unreach-call_true-termination.i |
programSHA |
50dc59d36af6d5eed248e08b307abe8deeb382344339bd05ed5d2dc08c8e7830 |
witnessName |
results-verified/depthk.2017-11-30_1601.logfiles/sv-comp18.sep_true-unreach-call_true-termination.i.files/witness.graphml |
witnessSHA |
b0eab24f3129b8e17905e39402213eb4c8cbc9529aab3aed04f4954ea5a3633c |
Information about the Witness from Competition Database
from https://sv-comp.sosy-lab.org/2018/results/witnessInfoByHash/b0eab24f3129b8e17905e39402213eb4c8cbc9529aab3aed04f4954ea5a3633c.json
Key |
Value |
architecture |
32bit |
creationtime |
2017-12-01T06:07 CET (sv-comp) |
memoryModel |
precise |
producer |
ESBMC 3.1 |
program-sha256 |
50dc59d36af6d5eed248e08b307abe8deeb382344339bd05ed5d2dc08c8e7830 |
programfile |
/tmp/vcloud-vcloud-master/worker/working_dir_0a53e04d-024d-4134-8de5-b1b55f373681/sv-benchmarks/c/reducercommutativity/sep_true-unreach-call_true-termination.i |
programhash |
e150e83dea41703782a488455769a24bf6c8f600 |
sourcecodelang |
C |
specification |
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file |
witnessFileByHash/b0eab24f3129b8e17905e39402213eb4c8cbc9529aab3aed04f4954ea5a3633c.graphml |
witness-sha256 |
b0eab24f3129b8e17905e39402213eb4c8cbc9529aab3aed04f4954ea5a3633c |
witness-size |
14333 |
witness-type |
correctness_witness |
Available Results for the Program from Witness Store SV-COMP '24
Trying to find witnesses for program (50dc59d36af6d5eed248e08b307abe8deeb382344339bd05ed5d2dc08c8e7830, ../../../comp/sv-benchmarks/c/reducercommutativity/sep_true-unreach-call_true-termination.i).
Found 0 witnesses for program ../../../comp/sv-benchmarks/c/reducercommutativity/sep_true-unreach-call_true-termination.i, 50dc59d36af6d5eed248e08b307abe8deeb382344339bd05ed5d2dc08c8e7830
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/50dc59d36af6d5eed248e08b307abe8deeb382344339bd05ed5d2dc08c8e7830.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 (50dc59d36af6d5eed248e08b307abe8deeb382344339bd05ed5d2dc08c8e7830, ../../../comp/sv-benchmarks/c/reducercommutativity/sep_true-unreach-call_true-termination.i).
Found 0 witnesses for program ../../../comp/sv-benchmarks/c/reducercommutativity/sep_true-unreach-call_true-termination.i, 50dc59d36af6d5eed248e08b307abe8deeb382344339bd05ed5d2dc08c8e7830
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/50dc59d36af6d5eed248e08b307abe8deeb382344339bd05ed5d2dc08c8e7830.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 (50dc59d36af6d5eed248e08b307abe8deeb382344339bd05ed5d2dc08c8e7830, ../../../comp/sv-benchmarks/c/reducercommutativity/sep_true-unreach-call_true-termination.i).
Found 0 witnesses for program ../../../comp/sv-benchmarks/c/reducercommutativity/sep_true-unreach-call_true-termination.i, 50dc59d36af6d5eed248e08b307abe8deeb382344339bd05ed5d2dc08c8e7830
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/50dc59d36af6d5eed248e08b307abe8deeb382344339bd05ed5d2dc08c8e7830.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 (50dc59d36af6d5eed248e08b307abe8deeb382344339bd05ed5d2dc08c8e7830, ../../../comp/sv-benchmarks/c/reducercommutativity/sep_true-unreach-call_true-termination.i).
Found 0 witnesses for program ../../../comp/sv-benchmarks/c/reducercommutativity/sep_true-unreach-call_true-termination.i, 50dc59d36af6d5eed248e08b307abe8deeb382344339bd05ed5d2dc08c8e7830
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/50dc59d36af6d5eed248e08b307abe8deeb382344339bd05ed5d2dc08c8e7830.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 (50dc59d36af6d5eed248e08b307abe8deeb382344339bd05ed5d2dc08c8e7830, ../../../comp/sv-benchmarks/c/reducercommutativity/sep_true-unreach-call_true-termination.i).
Found 4 witnesses for program ../../../comp/sv-benchmarks/c/reducercommutativity/sep_true-unreach-call_true-termination.i, 50dc59d36af6d5eed248e08b307abe8deeb382344339bd05ed5d2dc08c8e7830
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/50dc59d36af6d5eed248e08b307abe8deeb382344339bd05ed5d2dc08c8e7830.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
8128d0e |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
8 |
2019-12-08T01:05:20+01:00 |
eed50c7 |
f7c5998 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
8 |
2019-12-06T02:20:05+01:00 |
c0201c1 |
b49a7c9 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
8 |
2019-11-30T17:38:16+01:00 |
ab99725 |
ab99725 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / svcomp20 |
278 |
2019-11-29T23:46:26+01:00 |
|
Available Results for the Program from Witness Store SV-COMP '19
Trying to find witnesses for program (50dc59d36af6d5eed248e08b307abe8deeb382344339bd05ed5d2dc08c8e7830, ../../../comp/sv-benchmarks/c/reducercommutativity/sep_true-unreach-call_true-termination.i).
Found 7 witnesses for program ../../../comp/sv-benchmarks/c/reducercommutativity/sep_true-unreach-call_true-termination.i, 50dc59d36af6d5eed248e08b307abe8deeb382344339bd05ed5d2dc08c8e7830
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/50dc59d36af6d5eed248e08b307abe8deeb382344339bd05ed5d2dc08c8e7830.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
bcae711 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
SMACK 1.9.3 |
3 |
2018-12-08T00:22:45 |
|
d82af50 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn b8d6131600+ |
10 |
2018-12-06T13:37:18+01:00 |
|
ab343c5 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
8 |
2018-12-09T21:21:20+01:00 |
79cf7a5 |
03ab271 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
8 |
2018-12-08T22:03:54+01:00 |
bcae711 |
deb4821 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
8 |
2018-12-08T06:27:37+01:00 |
d82af50 |
8b15c58 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
8 |
2018-12-06T09:14:42+01:00 |
8e10769 |
8e10769 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
343 |
2018-12-06T05:21:51+01:00 |
|
Available Results for the Program from Witness Store SV-COMP '18
Trying to find witnesses for program (50dc59d36af6d5eed248e08b307abe8deeb382344339bd05ed5d2dc08c8e7830, ../../../comp/sv-benchmarks/c/reducercommutativity/sep_true-unreach-call_true-termination.i).
Found 7 witnesses for program ../../../comp/sv-benchmarks/c/reducercommutativity/sep_true-unreach-call_true-termination.i, 50dc59d36af6d5eed248e08b307abe8deeb382344339bd05ed5d2dc08c8e7830
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/50dc59d36af6d5eed248e08b307abe8deeb382344339bd05ed5d2dc08c8e7830.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
a519cce |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.6.1-svn 26758M |
35 |
2017-12-01T03:28:21+01:00 |
|
304f5dd |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker (unknown version) |
5 |
2017-12-02T12:34:12+01:00 |
|
e082d33 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
Map2Check |
5 |
2017-12-01T20:35 CET (sv-comp) |
|
b0eab24 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
ESBMC 3.1 |
14 |
2017-12-01T06:07 CET (sv-comp) |
|
6a9c11c |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.6.1-svn 26773 |
8 |
2017-12-01T22:19:21+01:00 |
30462f6 |
1cb4b98 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.6.1-svn 26773 |
8 |
2017-12-01T08:28:23+01:00 |
c93b409 |
b4a69f7 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
2LS |
28 |
2017-12-01T12:22 CET (sv-comp) |
|
Available Results for the Program from Witness Store SV-COMP '17
Trying to find witnesses for program (50dc59d36af6d5eed248e08b307abe8deeb382344339bd05ed5d2dc08c8e7830, ../../../comp/sv-benchmarks/c/reducercommutativity/sep_true-unreach-call_true-termination.i).
Found 0 witnesses for program ../../../comp/sv-benchmarks/c/reducercommutativity/sep_true-unreach-call_true-termination.i, 50dc59d36af6d5eed248e08b307abe8deeb382344339bd05ed5d2dc08c8e7830
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/50dc59d36af6d5eed248e08b307abe8deeb382344339bd05ed5d2dc08c8e7830.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |