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/list-properties/list_false-unreach-call_false-valid-memcleanup.i |
programSHA |
fbbdbe28a5adf49f98129009b1e642d650a7192213ec6c4c9ffe96c4711bbd7c |
witnessName |
results-verified/predatorhp.2017-12-01_2024.logfiles/sv-comp18.list_false-unreach-call_false-valid-memcleanup.i.files/witness.graphml |
witnessSHA |
eb5a43a376d6bdadb5472e3f5b8a539e9349d334acb5d1fbd984b3aba091666c |
Information about the Witness from Competition Database
from https://sv-comp.sosy-lab.org/2018/results/witnessInfoByHash/eb5a43a376d6bdadb5472e3f5b8a539e9349d334acb5d1fbd984b3aba091666c.json
Key |
Value |
architecture |
32bit |
creationtime |
2017-12-01T20:44 CET (sv-comp) |
memorymodel |
precise |
producer |
PredatorHP |
program-sha256 |
fbbdbe28a5adf49f98129009b1e642d650a7192213ec6c4c9ffe96c4711bbd7c |
programfile |
../../sv-benchmarks/c/list-properties/list_false-unreach-call_false-valid-memcleanup.i |
programhash |
9d5c9e73019496cf8de6b5e77c9588d54710972f |
sourcecodelang |
C |
specification |
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file |
witnessFileByHash/eb5a43a376d6bdadb5472e3f5b8a539e9349d334acb5d1fbd984b3aba091666c.graphml |
witness-sha256 |
eb5a43a376d6bdadb5472e3f5b8a539e9349d334acb5d1fbd984b3aba091666c |
witness-size |
4749 |
witness-type |
violation_witness |
Available Results for the Program from Witness Store SV-COMP '24
Trying to find witnesses for program (fbbdbe28a5adf49f98129009b1e642d650a7192213ec6c4c9ffe96c4711bbd7c, ../../../comp/sv-benchmarks/c/list-properties/list_false-unreach-call_false-valid-memcleanup.i).
Found 0 witnesses for program ../../../comp/sv-benchmarks/c/list-properties/list_false-unreach-call_false-valid-memcleanup.i, fbbdbe28a5adf49f98129009b1e642d650a7192213ec6c4c9ffe96c4711bbd7c
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/fbbdbe28a5adf49f98129009b1e642d650a7192213ec6c4c9ffe96c4711bbd7c.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 (fbbdbe28a5adf49f98129009b1e642d650a7192213ec6c4c9ffe96c4711bbd7c, ../../../comp/sv-benchmarks/c/list-properties/list_false-unreach-call_false-valid-memcleanup.i).
Found 0 witnesses for program ../../../comp/sv-benchmarks/c/list-properties/list_false-unreach-call_false-valid-memcleanup.i, fbbdbe28a5adf49f98129009b1e642d650a7192213ec6c4c9ffe96c4711bbd7c
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/fbbdbe28a5adf49f98129009b1e642d650a7192213ec6c4c9ffe96c4711bbd7c.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 (fbbdbe28a5adf49f98129009b1e642d650a7192213ec6c4c9ffe96c4711bbd7c, ../../../comp/sv-benchmarks/c/list-properties/list_false-unreach-call_false-valid-memcleanup.i).
Found 0 witnesses for program ../../../comp/sv-benchmarks/c/list-properties/list_false-unreach-call_false-valid-memcleanup.i, fbbdbe28a5adf49f98129009b1e642d650a7192213ec6c4c9ffe96c4711bbd7c
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/fbbdbe28a5adf49f98129009b1e642d650a7192213ec6c4c9ffe96c4711bbd7c.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 (fbbdbe28a5adf49f98129009b1e642d650a7192213ec6c4c9ffe96c4711bbd7c, ../../../comp/sv-benchmarks/c/list-properties/list_false-unreach-call_false-valid-memcleanup.i).
Found 0 witnesses for program ../../../comp/sv-benchmarks/c/list-properties/list_false-unreach-call_false-valid-memcleanup.i, fbbdbe28a5adf49f98129009b1e642d650a7192213ec6c4c9ffe96c4711bbd7c
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/fbbdbe28a5adf49f98129009b1e642d650a7192213ec6c4c9ffe96c4711bbd7c.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 (fbbdbe28a5adf49f98129009b1e642d650a7192213ec6c4c9ffe96c4711bbd7c, ../../../comp/sv-benchmarks/c/list-properties/list_false-unreach-call_false-valid-memcleanup.i).
Found 0 witnesses for program ../../../comp/sv-benchmarks/c/list-properties/list_false-unreach-call_false-valid-memcleanup.i, fbbdbe28a5adf49f98129009b1e642d650a7192213ec6c4c9ffe96c4711bbd7c
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/fbbdbe28a5adf49f98129009b1e642d650a7192213ec6c4c9ffe96c4711bbd7c.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 (fbbdbe28a5adf49f98129009b1e642d650a7192213ec6c4c9ffe96c4711bbd7c, ../../../comp/sv-benchmarks/c/list-properties/list_false-unreach-call_false-valid-memcleanup.i).
Found 0 witnesses for program ../../../comp/sv-benchmarks/c/list-properties/list_false-unreach-call_false-valid-memcleanup.i, fbbdbe28a5adf49f98129009b1e642d650a7192213ec6c4c9ffe96c4711bbd7c
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/fbbdbe28a5adf49f98129009b1e642d650a7192213ec6c4c9ffe96c4711bbd7c.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 (fbbdbe28a5adf49f98129009b1e642d650a7192213ec6c4c9ffe96c4711bbd7c, ../../../comp/sv-benchmarks/c/list-properties/list_false-unreach-call_false-valid-memcleanup.i).
Found 12 witnesses for program ../../../comp/sv-benchmarks/c/list-properties/list_false-unreach-call_false-valid-memcleanup.i, fbbdbe28a5adf49f98129009b1e642d650a7192213ec6c4c9ffe96c4711bbd7c
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/fbbdbe28a5adf49f98129009b1e642d650a7192213ec6c4c9ffe96c4711bbd7c.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
b948049 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
VeriAbs 1.3 |
53 |
Sun Dec 3 00:57:07 2017 |
|
8491b12 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
Symbiotic |
1 |
2017-12-02T07:02 CET (sv-comp) |
|
eb5a43a |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
PredatorHP |
5 |
2017-12-01T20:44 CET (sv-comp) |
|
fc1e9c0 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
Map2Check |
3 |
2017-12-01T20:15 CET (sv-comp) |
|
62ef9b5 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
Kojak |
13 |
2017-12-02T18:13Z |
|
a493771 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
ESBMC 4.6.0 kind |
5 |
2017-12-01T22:59:19.307312 |
|
f829bf6 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
ESBMC 4.6.0 incr |
5 |
2017-12-01T16:59:22.753588 |
|
71954e2 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
ESBMC 3.1 |
4 |
2017-11-30T17:07 CET (sv-comp) |
|
c021a4f |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.6.1-svn 26773 |
11 |
2017-11-30T14:36:55+01:00 |
|
a436def |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.6.1-svn 26758M |
18 |
2017-11-30T18:51:54+01:00 |
|
3e348a4 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CBMC |
10 |
2017-12-01T03:37 CET (sv-comp) |
|
53c5801 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
Automizer |
13 |
2017-12-02T21:48Z |
|
Available Results for the Program from Witness Store SV-COMP '17
Trying to find witnesses for program (fbbdbe28a5adf49f98129009b1e642d650a7192213ec6c4c9ffe96c4711bbd7c, ../../../comp/sv-benchmarks/c/list-properties/list_false-unreach-call_false-valid-memcleanup.i).
Found 0 witnesses for program ../../../comp/sv-benchmarks/c/list-properties/list_false-unreach-call_false-valid-memcleanup.i, fbbdbe28a5adf49f98129009b1e642d650a7192213ec6c4c9ffe96c4711bbd7c
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/fbbdbe28a5adf49f98129009b1e642d650a7192213ec6c4c9ffe96c4711bbd7c.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |