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/loops/invert_string_false-valid-deref.c |
programSHA |
160e60e7b105ea4b394b7ff1af1478c2fc2bdfab01c677db84a190d24ab9b18a |
witnessName |
results-verified/2ls.2018-12-04_2244.logfiles/sv-comp19_prop-memsafety.invert_string_false-valid-deref.c.files/witness.graphml |
witnessSHA |
95dd0514658f495ba5523906504c176c0e06cb4e96c5735b2a61644b12c90ab4 |
Information about the Witness from Competition Database
from https://sv-comp.sosy-lab.org/2019/results/witnessInfoByHash/95dd0514658f495ba5523906504c176c0e06cb4e96c5735b2a61644b12c90ab4.json
Key |
Value |
architecture |
32bit |
creationtime |
2018-12-04T23:52 CET (sv-comp) |
error-specification-length |
Key 'specification' longer than 100 characters. |
producer |
2LS |
programfile |
../../sv-benchmarks/c/loops/invert_string_false-valid-deref.c |
programhash |
01c8dcbf548ac0eef8cebe655947adbb13d26f9a |
sourcecodelang |
C |
specification |
CHECK( init(main()), LTL(G valid-free) )
CHECK( init(main()), LTL(G valid-deref) )
CHECK( init(main()), LTL(G valid-memtrack) ) |
witness-file |
witnessFileByHash/95dd0514658f495ba5523906504c176c0e06cb4e96c5735b2a61644b12c90ab4.graphml |
witness-sha256 |
95dd0514658f495ba5523906504c176c0e06cb4e96c5735b2a61644b12c90ab4 |
witness-size |
4168 |
witness-type |
violation_witness |
Available Results for the Program from Witness Store SV-COMP '24
Trying to find witnesses for program (160e60e7b105ea4b394b7ff1af1478c2fc2bdfab01c677db84a190d24ab9b18a, sv-benchmarks/c/loops/invert_string_false-valid-deref.c).
Found 0 witnesses for program sv-benchmarks/c/loops/invert_string_false-valid-deref.c, 160e60e7b105ea4b394b7ff1af1478c2fc2bdfab01c677db84a190d24ab9b18a
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/160e60e7b105ea4b394b7ff1af1478c2fc2bdfab01c677db84a190d24ab9b18a.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 (160e60e7b105ea4b394b7ff1af1478c2fc2bdfab01c677db84a190d24ab9b18a, sv-benchmarks/c/loops/invert_string_false-valid-deref.c).
Found 0 witnesses for program sv-benchmarks/c/loops/invert_string_false-valid-deref.c, 160e60e7b105ea4b394b7ff1af1478c2fc2bdfab01c677db84a190d24ab9b18a
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/160e60e7b105ea4b394b7ff1af1478c2fc2bdfab01c677db84a190d24ab9b18a.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 (160e60e7b105ea4b394b7ff1af1478c2fc2bdfab01c677db84a190d24ab9b18a, sv-benchmarks/c/loops/invert_string_false-valid-deref.c).
Found 0 witnesses for program sv-benchmarks/c/loops/invert_string_false-valid-deref.c, 160e60e7b105ea4b394b7ff1af1478c2fc2bdfab01c677db84a190d24ab9b18a
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/160e60e7b105ea4b394b7ff1af1478c2fc2bdfab01c677db84a190d24ab9b18a.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 (160e60e7b105ea4b394b7ff1af1478c2fc2bdfab01c677db84a190d24ab9b18a, sv-benchmarks/c/loops/invert_string_false-valid-deref.c).
Found 0 witnesses for program sv-benchmarks/c/loops/invert_string_false-valid-deref.c, 160e60e7b105ea4b394b7ff1af1478c2fc2bdfab01c677db84a190d24ab9b18a
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/160e60e7b105ea4b394b7ff1af1478c2fc2bdfab01c677db84a190d24ab9b18a.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 (160e60e7b105ea4b394b7ff1af1478c2fc2bdfab01c677db84a190d24ab9b18a, sv-benchmarks/c/loops/invert_string_false-valid-deref.c).
Found 13 witnesses for program sv-benchmarks/c/loops/invert_string_false-valid-deref.c, 160e60e7b105ea4b394b7ff1af1478c2fc2bdfab01c677db84a190d24ab9b18a
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/160e60e7b105ea4b394b7ff1af1478c2fc2bdfab01c677db84a190d24ab9b18a.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
2b9b5c1 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
violation_witness |
Symbiotic |
1 |
2019-12-02 02:13:56 |
|
29394ee |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
violation_witness |
CPAchecker 1.9 |
5 |
2019-12-11T21:09:00+01:00 |
2b9b5c1 |
6a93e8c |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 1.9 |
7 |
2019-12-08T00:26:09+01:00 |
fdd5135 |
bc3b66b |
Inspect |
|
CHECK( init(main()), LTL(G valid-free) ) |
correctness_witness |
CPAchecker 1.9 |
7 |
2019-12-11T21:48:57+01:00 |
5bc25ca |
074091d |
Inspect |
|
CHECK( init(main()), LTL(G valid-free) ) |
correctness_witness |
CPAchecker 1.9 |
7 |
2019-12-11T21:44:41+01:00 |
87e6a1d |
3700d69 |
Inspect |
|
CHECK( init(main()), LTL(G valid-free) ) |
correctness_witness |
CPAchecker 1.9 |
7 |
2019-12-11T20:54:59+01:00 |
278f1a3 |
55bd66e |
Inspect |
|
CHECK( init(main()), LTL(G valid-free) ) |
correctness_witness |
CPAchecker 1.9 |
7 |
2019-12-07T21:17:13+01:00 |
acfa2b6 |
6513c49 |
Inspect |
|
CHECK( init(main()), LTL(G valid-free) ) |
correctness_witness |
CPAchecker 1.9 |
7 |
2019-12-06T02:38:42+01:00 |
f882d11 |
84ae189 |
Inspect |
|
CHECK( init(main()), LTL(G valid-free) ) |
correctness_witness |
CPAchecker 1.9 |
7 |
2019-11-29T18:36:17+01:00 |
|
fd0ac55 |
Inspect |
|
CHECK( init(main()), LTL(G valid-deref) ) |
correctness_witness |
CPAchecker 1.9 |
7 |
2019-12-08T00:07:42+01:00 |
53c050f |
9cfebd4 |
Inspect |
|
CHECK( init(main()), LTL(G valid-deref) ) |
correctness_witness |
CPAchecker 1.9 |
7 |
2019-12-05T20:20:51+01:00 |
9f4a6ac |
dfa4d06 |
Inspect |
|
CHECK( init(main()), LTL(G valid-deref) ) |
correctness_witness |
CPAchecker 1.9 |
7 |
2019-12-03T08:09:38+01:00 |
84ae189 |
87e6a1d |
Inspect |
|
CHECK( init(main()), LTL(G valid-deref) ) |
correctness_witness |
CPAchecker 1.8-svn-35b8bb3bb3+ |
7 |
2019-12-01T02:03:41+01:00 |
|
Available Results for the Program from Witness Store SV-COMP '19
Trying to find witnesses for program (160e60e7b105ea4b394b7ff1af1478c2fc2bdfab01c677db84a190d24ab9b18a, sv-benchmarks/c/loops/invert_string_false-valid-deref.c).
Found 15 witnesses for program sv-benchmarks/c/loops/invert_string_false-valid-deref.c, 160e60e7b105ea4b394b7ff1af1478c2fc2bdfab01c677db84a190d24ab9b18a
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/160e60e7b105ea4b394b7ff1af1478c2fc2bdfab01c677db84a190d24ab9b18a.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
fe80202 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
violation_witness |
Symbiotic |
1 |
2018-12-08T05:10 CET (sv-comp) |
|
5adbd88 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
5 |
2018-12-06T10:19:11+01:00 |
e2f30c4 |
6b5da62 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
5 |
2018-12-06T09:41:10+01:00 |
95dd051 |
7ca140a |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 1.7-svn b8d6131600+ |
7 |
2018-12-07T22:42:26+01:00 |
|
1795cae |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
7 |
2018-12-09T20:53:04+01:00 |
83c692d |
1ca0fe8 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
7 |
2018-12-09T20:23:52+01:00 |
687e00d |
e8406ae |
Inspect |
|
CHECK( init(main()), LTL(G valid-free) )
CHECK( init(main()), LTL(G valid-deref) )
CHECK( init(main()), LTL(G valid-memtrack) ) |
violation_witness |
SMACK 1.9.3 |
4 |
2018-12-08T17:34:55 |
|
4d6bd4f |
Inspect |
|
CHECK( init(main()), LTL(G valid-deref) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
5 |
2018-12-08T23:43:51+01:00 |
fe80202 |
93ce597 |
Inspect |
|
CHECK( init(main()), LTL(G valid-deref) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
5 |
2018-12-08T22:10:24+01:00 |
e8406ae |
1eeab06 |
Inspect |
|
CHECK( init(main()), LTL(G valid-deref) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
5 |
2018-12-08T04:55:30+01:00 |
c6aceed |
c4f7179 |
Inspect |
|
CHECK( init(main()), LTL(G valid-deref) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
7 |
2018-12-09T20:40:05+01:00 |
edc2641 |
71d6236 |
Inspect |
|
CHECK( init(main()), LTL(G valid-deref) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
7 |
2018-12-07T01:07:20+01:00 |
6f017e2 |
2d91a25 |
Inspect |
|
CHECK( init(main()), LTL(G valid-deref) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
7 |
2018-12-06T09:12:24+01:00 |
9d41245 |
f47b3e4 |
Inspect |
|
CHECK( init(main()), LTL(G valid-deref) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
7 |
2018-12-06T09:00:06+01:00 |
5138e62 |
cbd585d |
Inspect |
|
CHECK( init(main()), LTL(G valid-deref) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
7 |
2018-12-06T06:24:06+01:00 |
|
Available Results for the Program from Witness Store SV-COMP '18
Trying to find witnesses for program (160e60e7b105ea4b394b7ff1af1478c2fc2bdfab01c677db84a190d24ab9b18a, sv-benchmarks/c/loops/invert_string_false-valid-deref.c).
Found 0 witnesses for program sv-benchmarks/c/loops/invert_string_false-valid-deref.c, 160e60e7b105ea4b394b7ff1af1478c2fc2bdfab01c677db84a190d24ab9b18a
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/160e60e7b105ea4b394b7ff1af1478c2fc2bdfab01c677db84a190d24ab9b18a.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 (160e60e7b105ea4b394b7ff1af1478c2fc2bdfab01c677db84a190d24ab9b18a, sv-benchmarks/c/loops/invert_string_false-valid-deref.c).
Found 0 witnesses for program sv-benchmarks/c/loops/invert_string_false-valid-deref.c, 160e60e7b105ea4b394b7ff1af1478c2fc2bdfab01c677db84a190d24ab9b18a
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/160e60e7b105ea4b394b7ff1af1478c2fc2bdfab01c677db84a190d24ab9b18a.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |