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-memsafety/diff_usafe_false-valid-deref.i |
programSHA |
a9f0e356c49a494876defc78ad8dabf1988e565215136c0b9efd4689823385e3 |
witnessName |
results-verified/cbmc.2017-12-01_0819.logfiles/sv-comp18.diff_usafe_false-valid-deref.i.files/witness.graphml |
witnessSHA |
ad88e983fe09147c80e404f8326f115937785c217e1e0fd501e2464226b3c5b6 |
Information about the Witness from Competition Database
from https://sv-comp.sosy-lab.org/2018/results/witnessInfoByHash/ad88e983fe09147c80e404f8326f115937785c217e1e0fd501e2464226b3c5b6.json
Key |
Value |
architecture |
32bit |
creationtime |
2017-12-01T08:28 CET (sv-comp) |
error-specification-length |
Key 'specification' longer than 100 characters. |
producer |
CBMC |
program-sha256 |
a9f0e356c49a494876defc78ad8dabf1988e565215136c0b9efd4689823385e3 |
programfile |
../../sv-benchmarks/c/array-memsafety/diff_usafe_false-valid-deref.i |
programhash |
c4e0be718883e167d4be051b03c3a4364271b932 |
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/ad88e983fe09147c80e404f8326f115937785c217e1e0fd501e2464226b3c5b6.graphml |
witness-sha256 |
ad88e983fe09147c80e404f8326f115937785c217e1e0fd501e2464226b3c5b6 |
witness-size |
6792 |
witness-type |
violation_witness |
Available Results for the Program from Witness Store SV-COMP '24
Trying to find witnesses for program (a9f0e356c49a494876defc78ad8dabf1988e565215136c0b9efd4689823385e3, sv-benchmarks/c/array-memsafety/diff_usafe_false-valid-deref.i).
Found 0 witnesses for program sv-benchmarks/c/array-memsafety/diff_usafe_false-valid-deref.i, a9f0e356c49a494876defc78ad8dabf1988e565215136c0b9efd4689823385e3
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/a9f0e356c49a494876defc78ad8dabf1988e565215136c0b9efd4689823385e3.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 (a9f0e356c49a494876defc78ad8dabf1988e565215136c0b9efd4689823385e3, sv-benchmarks/c/array-memsafety/diff_usafe_false-valid-deref.i).
Found 0 witnesses for program sv-benchmarks/c/array-memsafety/diff_usafe_false-valid-deref.i, a9f0e356c49a494876defc78ad8dabf1988e565215136c0b9efd4689823385e3
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/a9f0e356c49a494876defc78ad8dabf1988e565215136c0b9efd4689823385e3.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 (a9f0e356c49a494876defc78ad8dabf1988e565215136c0b9efd4689823385e3, sv-benchmarks/c/array-memsafety/diff_usafe_false-valid-deref.i).
Found 0 witnesses for program sv-benchmarks/c/array-memsafety/diff_usafe_false-valid-deref.i, a9f0e356c49a494876defc78ad8dabf1988e565215136c0b9efd4689823385e3
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/a9f0e356c49a494876defc78ad8dabf1988e565215136c0b9efd4689823385e3.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 (a9f0e356c49a494876defc78ad8dabf1988e565215136c0b9efd4689823385e3, sv-benchmarks/c/array-memsafety/diff_usafe_false-valid-deref.i).
Found 0 witnesses for program sv-benchmarks/c/array-memsafety/diff_usafe_false-valid-deref.i, a9f0e356c49a494876defc78ad8dabf1988e565215136c0b9efd4689823385e3
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/a9f0e356c49a494876defc78ad8dabf1988e565215136c0b9efd4689823385e3.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 (a9f0e356c49a494876defc78ad8dabf1988e565215136c0b9efd4689823385e3, sv-benchmarks/c/array-memsafety/diff_usafe_false-valid-deref.i).
Found 0 witnesses for program sv-benchmarks/c/array-memsafety/diff_usafe_false-valid-deref.i, a9f0e356c49a494876defc78ad8dabf1988e565215136c0b9efd4689823385e3
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/a9f0e356c49a494876defc78ad8dabf1988e565215136c0b9efd4689823385e3.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 (a9f0e356c49a494876defc78ad8dabf1988e565215136c0b9efd4689823385e3, sv-benchmarks/c/array-memsafety/diff_usafe_false-valid-deref.i).
Found 13 witnesses for program sv-benchmarks/c/array-memsafety/diff_usafe_false-valid-deref.i, a9f0e356c49a494876defc78ad8dabf1988e565215136c0b9efd4689823385e3
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/a9f0e356c49a494876defc78ad8dabf1988e565215136c0b9efd4689823385e3.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
3e8d3ca |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 1.7-svn b8d6131600+ |
7 |
2018-12-07T20:34:12+01:00 |
|
f7973ad |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
8 |
2018-12-09T20:23:05+01:00 |
d6a975c |
739942f |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
8 |
2018-12-08T03:34:34+01:00 |
669f4eb |
0cb8003 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
8 |
2018-12-06T10:21:13+01:00 |
3268cd7 |
9b91e83 |
Inspect |
|
CHECK( init(main()), LTL(G valid-free) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
8 |
2018-12-06T09:19:42+01:00 |
c8cdf94 |
4500caa |
Inspect |
|
CHECK( init(main()), LTL(G valid-free) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
8 |
2018-12-08T22:09:41+01:00 |
54c02d4 |
3fc7545 |
Inspect |
|
CHECK( init(main()), LTL(G valid-free) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
8 |
2018-12-07T09:14:33+01:00 |
65a229f |
484ffca |
Inspect |
|
CHECK( init(main()), LTL(G valid-free) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
8 |
2018-12-06T09:15:18+01:00 |
e71e793 |
54c02d4 |
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-08T07:53:30 |
|
96b4831 |
Inspect |
|
CHECK( init(main()), LTL(G valid-deref) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
8 |
2018-12-09T20:53:09+01:00 |
db1ca47 |
4659ae8 |
Inspect |
|
CHECK( init(main()), LTL(G valid-deref) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
8 |
2018-12-09T20:38:53+01:00 |
9c2d6d8 |
297164d |
Inspect |
|
CHECK( init(main()), LTL(G valid-deref) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
8 |
2018-12-08T05:07:09+01:00 |
0ed94a5 |
a37f98f |
Inspect |
|
CHECK( init(main()), LTL(G valid-deref) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
8 |
2018-12-07T01:14:03+01:00 |
7ac2aa4 |
Available Results for the Program from Witness Store SV-COMP '18
Trying to find witnesses for program (a9f0e356c49a494876defc78ad8dabf1988e565215136c0b9efd4689823385e3, sv-benchmarks/c/array-memsafety/diff_usafe_false-valid-deref.i).
Found 10 witnesses for program sv-benchmarks/c/array-memsafety/diff_usafe_false-valid-deref.i, a9f0e356c49a494876defc78ad8dabf1988e565215136c0b9efd4689823385e3
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/a9f0e356c49a494876defc78ad8dabf1988e565215136c0b9efd4689823385e3.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
d0e7675 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
violation_witness |
Symbiotic |
2 |
2017-12-03T00:01 CET (sv-comp) |
|
ce9e0ea |
Inspect |
|
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) |
violation_witness |
ESBMC 4.6.0 kind |
4 |
2017-12-02T11:59:33.780229 |
|
d57d53c |
Inspect |
|
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) |
violation_witness |
ESBMC 4.6.0 incr |
4 |
2017-12-01T23:02:27.740447 |
|
e1b2879 |
Inspect |
|
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) |
violation_witness |
ESBMC 3.1 |
6 |
2017-12-01T09:34 CET (sv-comp) |
|
5348e23 |
Inspect |
|
CHECK( init(main()), LTL(G valid-free) )
CHECK( init(main()), LTL(G valid-deref) )
CHECK( init(main()), LTL(G valid-memtrack) ) |
violation_witness |
Taipan |
8 |
2017-12-03T06:53Z |
|
a064b3f |
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 |
8 |
2017-12-03T03:56Z |
|
ad88e98 |
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 |
7 |
2017-12-01T08:28 CET (sv-comp) |
|
cd309a9 |
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 |
8 |
2017-12-03T04:06Z |
|
65a229f |
Inspect |
|
CHECK( init(main()), LTL(G valid-deref) ) |
violation_witness |
PredatorHP |
4 |
2017-12-01T22:19 CET (sv-comp) |
|
f221e91 |
Inspect |
|
CHECK( init(main()), LTL(G valid-deref) ) |
violation_witness |
Map2Check |
3 |
2017-12-01T23:39 CET (sv-comp) |
|
Available Results for the Program from Witness Store SV-COMP '17
Trying to find witnesses for program (a9f0e356c49a494876defc78ad8dabf1988e565215136c0b9efd4689823385e3, sv-benchmarks/c/array-memsafety/diff_usafe_false-valid-deref.i).
Found 0 witnesses for program sv-benchmarks/c/array-memsafety/diff_usafe_false-valid-deref.i, a9f0e356c49a494876defc78ad8dabf1988e565215136c0b9efd4689823385e3
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/a9f0e356c49a494876defc78ad8dabf1988e565215136c0b9efd4689823385e3.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |