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/memsafety/test-0137_false-valid-deref.i |
programSHA |
9d23e8b645690eb1df566bba37e3ad297a1d5cd7a5051a858b78b06a7531c979 |
witnessName |
results-verified/cbmc.2017-12-01_0819.logfiles/sv-comp18.test-0137_false-valid-deref.i.files/witness.graphml |
witnessSHA |
8ee84b75eeede6df97e272c4f25f9e244866801732bac09b821e8b09225c209b |
Information about the Witness from Competition Database
from https://sv-comp.sosy-lab.org/2018/results/witnessInfoByHash/8ee84b75eeede6df97e272c4f25f9e244866801732bac09b821e8b09225c209b.json
Key |
Value |
architecture |
32bit |
creationtime |
2017-12-01T08:30 CET (sv-comp) |
error-specification-length |
Key 'specification' longer than 100 characters. |
producer |
CBMC |
program-sha256 |
9d23e8b645690eb1df566bba37e3ad297a1d5cd7a5051a858b78b06a7531c979 |
programfile |
../../sv-benchmarks/c/memsafety/test-0137_false-valid-deref.i |
programhash |
f8eb9d2f787e4ba2c5d512d4d65134dc7956ccb3 |
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/8ee84b75eeede6df97e272c4f25f9e244866801732bac09b821e8b09225c209b.graphml |
witness-sha256 |
8ee84b75eeede6df97e272c4f25f9e244866801732bac09b821e8b09225c209b |
witness-size |
16779 |
witness-type |
violation_witness |
Available Results for the Program from Witness Store SV-COMP '24
Trying to find witnesses for program (9d23e8b645690eb1df566bba37e3ad297a1d5cd7a5051a858b78b06a7531c979, sv-benchmarks/c/memsafety/test-0137_false-valid-deref.i).
Found 0 witnesses for program sv-benchmarks/c/memsafety/test-0137_false-valid-deref.i, 9d23e8b645690eb1df566bba37e3ad297a1d5cd7a5051a858b78b06a7531c979
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/9d23e8b645690eb1df566bba37e3ad297a1d5cd7a5051a858b78b06a7531c979.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 (9d23e8b645690eb1df566bba37e3ad297a1d5cd7a5051a858b78b06a7531c979, sv-benchmarks/c/memsafety/test-0137_false-valid-deref.i).
Found 0 witnesses for program sv-benchmarks/c/memsafety/test-0137_false-valid-deref.i, 9d23e8b645690eb1df566bba37e3ad297a1d5cd7a5051a858b78b06a7531c979
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/9d23e8b645690eb1df566bba37e3ad297a1d5cd7a5051a858b78b06a7531c979.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 (9d23e8b645690eb1df566bba37e3ad297a1d5cd7a5051a858b78b06a7531c979, sv-benchmarks/c/memsafety/test-0137_false-valid-deref.i).
Found 0 witnesses for program sv-benchmarks/c/memsafety/test-0137_false-valid-deref.i, 9d23e8b645690eb1df566bba37e3ad297a1d5cd7a5051a858b78b06a7531c979
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/9d23e8b645690eb1df566bba37e3ad297a1d5cd7a5051a858b78b06a7531c979.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 (9d23e8b645690eb1df566bba37e3ad297a1d5cd7a5051a858b78b06a7531c979, sv-benchmarks/c/memsafety/test-0137_false-valid-deref.i).
Found 0 witnesses for program sv-benchmarks/c/memsafety/test-0137_false-valid-deref.i, 9d23e8b645690eb1df566bba37e3ad297a1d5cd7a5051a858b78b06a7531c979
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/9d23e8b645690eb1df566bba37e3ad297a1d5cd7a5051a858b78b06a7531c979.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 (9d23e8b645690eb1df566bba37e3ad297a1d5cd7a5051a858b78b06a7531c979, sv-benchmarks/c/memsafety/test-0137_false-valid-deref.i).
Found 0 witnesses for program sv-benchmarks/c/memsafety/test-0137_false-valid-deref.i, 9d23e8b645690eb1df566bba37e3ad297a1d5cd7a5051a858b78b06a7531c979
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/9d23e8b645690eb1df566bba37e3ad297a1d5cd7a5051a858b78b06a7531c979.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 (9d23e8b645690eb1df566bba37e3ad297a1d5cd7a5051a858b78b06a7531c979, sv-benchmarks/c/memsafety/test-0137_false-valid-deref.i).
Found 13 witnesses for program sv-benchmarks/c/memsafety/test-0137_false-valid-deref.i, 9d23e8b645690eb1df566bba37e3ad297a1d5cd7a5051a858b78b06a7531c979
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/9d23e8b645690eb1df566bba37e3ad297a1d5cd7a5051a858b78b06a7531c979.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
7025cdf |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
violation_witness |
Symbiotic |
1 |
2018-12-08T07:37 CET (sv-comp) |
|
a73a0da |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
11 |
2018-12-08T03:39:03+01:00 |
48a9376 |
8a4eb0b |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 1.7-svn b8d6131600+ |
17 |
2018-12-08T03:55:00+01:00 |
|
ba86954 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
17 |
2018-12-06T09:20:02+01:00 |
14c3656 |
42573fa |
Inspect |
|
CHECK( init(main()), LTL(G valid-free) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
11 |
2018-12-08T05:04:41+01:00 |
b443e48 |
5e3010a |
Inspect |
|
CHECK( init(main()), LTL(G valid-free) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
11 |
2018-12-07T09:16:03+01:00 |
e1b2f26 |
b26b151 |
Inspect |
|
CHECK( init(main()), LTL(G valid-free) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
17 |
2018-12-08T22:08:54+01:00 |
3cb524e |
eb17054 |
Inspect |
|
CHECK( init(main()), LTL(G valid-free) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
17 |
2018-12-06T07:08:34+01:00 |
|
3cb524e |
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-08T03:21:55 |
|
96671ff |
Inspect |
|
CHECK( init(main()), LTL(G valid-deref) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
11 |
2018-12-08T23:44:00+01:00 |
7025cdf |
f820d45 |
Inspect |
|
CHECK( init(main()), LTL(G valid-deref) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
12 |
2018-12-07T01:17:05+01:00 |
897e5d2 |
f67d216 |
Inspect |
|
CHECK( init(main()), LTL(G valid-deref) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
11 |
2018-12-06T10:15:39+01:00 |
7267f90 |
0322b93 |
Inspect |
|
CHECK( init(main()), LTL(G valid-deref) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
17 |
2018-12-06T09:18:14+01:00 |
2241025 |
Available Results for the Program from Witness Store SV-COMP '18
Trying to find witnesses for program (9d23e8b645690eb1df566bba37e3ad297a1d5cd7a5051a858b78b06a7531c979, sv-benchmarks/c/memsafety/test-0137_false-valid-deref.i).
Found 9 witnesses for program sv-benchmarks/c/memsafety/test-0137_false-valid-deref.i, 9d23e8b645690eb1df566bba37e3ad297a1d5cd7a5051a858b78b06a7531c979
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/9d23e8b645690eb1df566bba37e3ad297a1d5cd7a5051a858b78b06a7531c979.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
f4294fa |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
violation_witness |
Symbiotic |
1 |
2017-12-03T00:24 CET (sv-comp) |
|
3d49c03 |
Inspect |
|
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) |
violation_witness |
ESBMC 4.6.0 kind |
5 |
2017-12-02T11:14:43.107874 |
|
c460444 |
Inspect |
|
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) |
violation_witness |
ESBMC 4.6.0 incr |
5 |
2017-12-01T23:05:13.676808 |
|
1f7d8b1 |
Inspect |
|
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) |
violation_witness |
ESBMC 3.1 |
7 |
2017-12-01T09:40 CET (sv-comp) |
|
b13c07b |
Inspect |
|
CHECK( init(main()), LTL(G valid-free) )
CHECK( init(main()), LTL(G valid-deref) )
CHECK( init(main()), LTL(G valid-memtrack) ) |
violation_witness |
Kojak |
17 |
2017-12-03T04:12Z |
|
8ee84b7 |
Inspect |
|
CHECK( init(main()), LTL(G valid-free) )
CHECK( init(main()), LTL(G valid-deref) )
CHECK( init(main()), LTL(G valid-memtrack) ) |
violation_witness |
CBMC |
17 |
2017-12-01T08:30 CET (sv-comp) |
|
79e9190 |
Inspect |
|
CHECK( init(main()), LTL(G valid-free) )
CHECK( init(main()), LTL(G valid-deref) )
CHECK( init(main()), LTL(G valid-memtrack) ) |
violation_witness |
Automizer |
16 |
2017-12-03T04:21Z |
|
e1b2f26 |
Inspect |
|
CHECK( init(main()), LTL(G valid-deref) ) |
violation_witness |
PredatorHP |
5 |
2017-12-01T21:58 CET (sv-comp) |
|
4b1fdc7 |
Inspect |
|
CHECK( init(main()), LTL(G valid-deref) ) |
violation_witness |
Map2Check |
3 |
2017-12-01T23:29 CET (sv-comp) |
|
Available Results for the Program from Witness Store SV-COMP '17
Trying to find witnesses for program (9d23e8b645690eb1df566bba37e3ad297a1d5cd7a5051a858b78b06a7531c979, sv-benchmarks/c/memsafety/test-0137_false-valid-deref.i).
Found 0 witnesses for program sv-benchmarks/c/memsafety/test-0137_false-valid-deref.i, 9d23e8b645690eb1df566bba37e3ad297a1d5cd7a5051a858b78b06a7531c979
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/9d23e8b645690eb1df566bba37e3ad297a1d5cd7a5051a858b78b06a7531c979.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |