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/array-examples/standard_two_index_01_true-unreach-call.i |
programSHA |
132b17efdc7f53174ddc6ae2b39f7d5de532c56473157ec38f3ccddb23e5324a |
witnessName |
results-verified/map2check.2017-12-01_1946.logfiles/sv-comp18.standard_two_index_01_true-unreach-call.i.files/witness.graphml |
witnessSHA |
38307ebed52ffc89365f90d0bc3ad84a41f488be74108f5d4cc2d000c99ad213 |
Information about the Witness from Competition Database
from https://sv-comp.sosy-lab.org/2018/results/witnessInfoByHash/38307ebed52ffc89365f90d0bc3ad84a41f488be74108f5d4cc2d000c99ad213.json
Key |
Value |
architecture |
32bit |
creationtime |
2017-12-01T20:25 CET (sv-comp) |
producer |
Map2Check |
program-sha256 |
132b17efdc7f53174ddc6ae2b39f7d5de532c56473157ec38f3ccddb23e5324a |
programfile |
../../sv-benchmarks/c/array-examples/standard_two_index_01_true-unreach-call.i |
programhash |
5f310fbcb64657be59077a5518f0d4598cf8d506 |
sourcecodelang |
C |
specification |
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file |
witnessFileByHash/38307ebed52ffc89365f90d0bc3ad84a41f488be74108f5d4cc2d000c99ad213.graphml |
witness-sha256 |
38307ebed52ffc89365f90d0bc3ad84a41f488be74108f5d4cc2d000c99ad213 |
witness-size |
4328 |
witness-type |
correctness_witness |
Available Results for the Program from Witness Store SV-COMP '24
Trying to find witnesses for program (132b17efdc7f53174ddc6ae2b39f7d5de532c56473157ec38f3ccddb23e5324a, sv-benchmarks/c/array-examples/standard_two_index_01_true-unreach-call.i).
Found 0 witnesses for program sv-benchmarks/c/array-examples/standard_two_index_01_true-unreach-call.i, 132b17efdc7f53174ddc6ae2b39f7d5de532c56473157ec38f3ccddb23e5324a
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/132b17efdc7f53174ddc6ae2b39f7d5de532c56473157ec38f3ccddb23e5324a.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 (132b17efdc7f53174ddc6ae2b39f7d5de532c56473157ec38f3ccddb23e5324a, sv-benchmarks/c/array-examples/standard_two_index_01_true-unreach-call.i).
Found 0 witnesses for program sv-benchmarks/c/array-examples/standard_two_index_01_true-unreach-call.i, 132b17efdc7f53174ddc6ae2b39f7d5de532c56473157ec38f3ccddb23e5324a
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/132b17efdc7f53174ddc6ae2b39f7d5de532c56473157ec38f3ccddb23e5324a.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 (132b17efdc7f53174ddc6ae2b39f7d5de532c56473157ec38f3ccddb23e5324a, sv-benchmarks/c/array-examples/standard_two_index_01_true-unreach-call.i).
Found 0 witnesses for program sv-benchmarks/c/array-examples/standard_two_index_01_true-unreach-call.i, 132b17efdc7f53174ddc6ae2b39f7d5de532c56473157ec38f3ccddb23e5324a
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/132b17efdc7f53174ddc6ae2b39f7d5de532c56473157ec38f3ccddb23e5324a.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 (132b17efdc7f53174ddc6ae2b39f7d5de532c56473157ec38f3ccddb23e5324a, sv-benchmarks/c/array-examples/standard_two_index_01_true-unreach-call.i).
Found 0 witnesses for program sv-benchmarks/c/array-examples/standard_two_index_01_true-unreach-call.i, 132b17efdc7f53174ddc6ae2b39f7d5de532c56473157ec38f3ccddb23e5324a
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/132b17efdc7f53174ddc6ae2b39f7d5de532c56473157ec38f3ccddb23e5324a.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 (132b17efdc7f53174ddc6ae2b39f7d5de532c56473157ec38f3ccddb23e5324a, sv-benchmarks/c/array-examples/standard_two_index_01_true-unreach-call.i).
Found 5 witnesses for program sv-benchmarks/c/array-examples/standard_two_index_01_true-unreach-call.i, 132b17efdc7f53174ddc6ae2b39f7d5de532c56473157ec38f3ccddb23e5324a
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/132b17efdc7f53174ddc6ae2b39f7d5de532c56473157ec38f3ccddb23e5324a.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
7cfeaa2 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
Pinaka |
3 |
2019-12-04T01:04 CET (comp) |
|
42caa04 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
7 |
2019-12-11T20:20:23+01:00 |
2c2d694 |
639e5b9 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
7 |
2019-12-08T00:39:19+01:00 |
85086c5 |
663fc75 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
7 |
2019-12-06T02:17:38+01:00 |
f33d606 |
5b93d42 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
7 |
2019-12-04T02:10:38+01:00 |
7cfeaa2 |
Available Results for the Program from Witness Store SV-COMP '19
Trying to find witnesses for program (132b17efdc7f53174ddc6ae2b39f7d5de532c56473157ec38f3ccddb23e5324a, sv-benchmarks/c/array-examples/standard_two_index_01_true-unreach-call.i).
Found 6 witnesses for program sv-benchmarks/c/array-examples/standard_two_index_01_true-unreach-call.i, 132b17efdc7f53174ddc6ae2b39f7d5de532c56473157ec38f3ccddb23e5324a
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/132b17efdc7f53174ddc6ae2b39f7d5de532c56473157ec38f3ccddb23e5324a.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
394e2d5 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
Symbiotic |
1 |
2018-12-08T07:28 CET (sv-comp) |
|
edba469 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
Pinaka |
3 |
2018-12-07T01:19 CET (sv-comp) |
|
e261d9d |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
7 |
2018-12-10T20:25:55+01:00 |
7d37826 |
32016ed |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
7 |
2018-12-09T21:21:13+01:00 |
264869b |
86cba27 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
7 |
2018-12-08T23:36:28+01:00 |
394e2d5 |
64d8fc5 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
7 |
2018-12-07T16:53:27+01:00 |
edba469 |
Available Results for the Program from Witness Store SV-COMP '18
Trying to find witnesses for program (132b17efdc7f53174ddc6ae2b39f7d5de532c56473157ec38f3ccddb23e5324a, sv-benchmarks/c/array-examples/standard_two_index_01_true-unreach-call.i).
Found 6 witnesses for program sv-benchmarks/c/array-examples/standard_two_index_01_true-unreach-call.i, 132b17efdc7f53174ddc6ae2b39f7d5de532c56473157ec38f3ccddb23e5324a
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/132b17efdc7f53174ddc6ae2b39f7d5de532c56473157ec38f3ccddb23e5324a.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
d584bc9 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
Symbiotic |
1 |
2017-12-02T12:00 CET (sv-comp) |
|
38307eb |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
Map2Check |
4 |
2017-12-01T20:25 CET (sv-comp) |
|
61e948f |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.6.12-svcomp17 |
4 |
2017-11-02T13:16:17+05:30 |
|
853c5e5 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.6.1-svn 26773 |
7 |
2017-12-03T04:34:14+01:00 |
efe5b44 |
1a72f6d |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.6.1-svn 26773 |
7 |
2017-12-02T20:30:21+01:00 |
857ce75 |
ab8d75d |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.6.1-svn 26773 |
7 |
2017-12-01T22:23:16+01:00 |
556a506 |
Available Results for the Program from Witness Store SV-COMP '17
Trying to find witnesses for program (132b17efdc7f53174ddc6ae2b39f7d5de532c56473157ec38f3ccddb23e5324a, sv-benchmarks/c/array-examples/standard_two_index_01_true-unreach-call.i).
Found 0 witnesses for program sv-benchmarks/c/array-examples/standard_two_index_01_true-unreach-call.i, 132b17efdc7f53174ddc6ae2b39f7d5de532c56473157ec38f3ccddb23e5324a
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/132b17efdc7f53174ddc6ae2b39f7d5de532c56473157ec38f3ccddb23e5324a.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |