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/eca-rers2012/Problem04_label45_false-unreach-call.c |
programSHA |
908f14d17c5d46378bef8bcd0f2fc540ebcd798d38e019b04475fc59574779d5 |
witnessName |
results-verified/cpa-seq.2017-11-30_1120.logfiles/sv-comp18.Problem04_label45_false-unreach-call.c.files/witness.graphml |
witnessSHA |
ff0f520b1d29fe4e9482c500df38d07111e7706eab6dbdf062bc1152629957c2 |
Information about the Witness from Competition Database
from https://sv-comp.sosy-lab.org/2018/results/witnessInfoByHash/ff0f520b1d29fe4e9482c500df38d07111e7706eab6dbdf062bc1152629957c2.json
Key |
Value |
architecture |
32bit |
creationtime |
2017-11-30T17:02:04+01:00 |
producer |
CPAchecker 1.6.1-svn 26773 |
program-sha256 |
908f14d17c5d46378bef8bcd0f2fc540ebcd798d38e019b04475fc59574779d5 |
programfile |
../../sv-benchmarks/c/eca-rers2012/Problem04_label45_false-unreach-call.c |
programhash |
86cdab67fbe37529224b5eae1ceb4ce204cc0091 |
sourcecodelang |
C |
specification |
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file |
witnessFileByHash/ff0f520b1d29fe4e9482c500df38d07111e7706eab6dbdf062bc1152629957c2.graphml |
witness-sha256 |
ff0f520b1d29fe4e9482c500df38d07111e7706eab6dbdf062bc1152629957c2 |
witness-size |
3030281 |
witness-type |
violation_witness |
Available Results for the Program from Witness Store SV-COMP '24
Trying to find witnesses for program (908f14d17c5d46378bef8bcd0f2fc540ebcd798d38e019b04475fc59574779d5, sv-benchmarks/c/eca-rers2012/Problem04_label45_false-unreach-call.c).
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem04_label45_false-unreach-call.c, 908f14d17c5d46378bef8bcd0f2fc540ebcd798d38e019b04475fc59574779d5
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/908f14d17c5d46378bef8bcd0f2fc540ebcd798d38e019b04475fc59574779d5.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 (908f14d17c5d46378bef8bcd0f2fc540ebcd798d38e019b04475fc59574779d5, sv-benchmarks/c/eca-rers2012/Problem04_label45_false-unreach-call.c).
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem04_label45_false-unreach-call.c, 908f14d17c5d46378bef8bcd0f2fc540ebcd798d38e019b04475fc59574779d5
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/908f14d17c5d46378bef8bcd0f2fc540ebcd798d38e019b04475fc59574779d5.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 (908f14d17c5d46378bef8bcd0f2fc540ebcd798d38e019b04475fc59574779d5, sv-benchmarks/c/eca-rers2012/Problem04_label45_false-unreach-call.c).
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem04_label45_false-unreach-call.c, 908f14d17c5d46378bef8bcd0f2fc540ebcd798d38e019b04475fc59574779d5
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/908f14d17c5d46378bef8bcd0f2fc540ebcd798d38e019b04475fc59574779d5.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 (908f14d17c5d46378bef8bcd0f2fc540ebcd798d38e019b04475fc59574779d5, sv-benchmarks/c/eca-rers2012/Problem04_label45_false-unreach-call.c).
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem04_label45_false-unreach-call.c, 908f14d17c5d46378bef8bcd0f2fc540ebcd798d38e019b04475fc59574779d5
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/908f14d17c5d46378bef8bcd0f2fc540ebcd798d38e019b04475fc59574779d5.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 (908f14d17c5d46378bef8bcd0f2fc540ebcd798d38e019b04475fc59574779d5, sv-benchmarks/c/eca-rers2012/Problem04_label45_false-unreach-call.c).
Found 6 witnesses for program sv-benchmarks/c/eca-rers2012/Problem04_label45_false-unreach-call.c, 908f14d17c5d46378bef8bcd0f2fc540ebcd798d38e019b04475fc59574779d5
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/908f14d17c5d46378bef8bcd0f2fc540ebcd798d38e019b04475fc59574779d5.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
4d8a1d5 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
Symbiotic |
4 |
2019-12-01 12:28:45 |
|
30256ec |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
5444 |
2019-12-11T21:09:19+01:00 |
4d8a1d5 |
492e202 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
5444 |
2019-12-11T20:55:05+01:00 |
7bb9073 |
29fa85b |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
5444 |
2019-12-11T20:44:54+01:00 |
ea4239f |
33f1133 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
5444 |
2019-12-03T08:10:17+01:00 |
261bc78 |
261bc78 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / svcomp20 |
5484 |
2019-11-30T09:55:14+01:00 |
|
Available Results for the Program from Witness Store SV-COMP '19
Trying to find witnesses for program (908f14d17c5d46378bef8bcd0f2fc540ebcd798d38e019b04475fc59574779d5, sv-benchmarks/c/eca-rers2012/Problem04_label45_false-unreach-call.c).
Found 5 witnesses for program sv-benchmarks/c/eca-rers2012/Problem04_label45_false-unreach-call.c, 908f14d17c5d46378bef8bcd0f2fc540ebcd798d38e019b04475fc59574779d5
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/908f14d17c5d46378bef8bcd0f2fc540ebcd798d38e019b04475fc59574779d5.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
c6561cf |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
5486 |
2018-12-10T20:38:04+01:00 |
e0e0633 |
0df21dc |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
5444 |
2018-12-09T18:20:13+01:00 |
e8146e6 |
3a3ba96 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
5444 |
2018-12-08T04:57:16+01:00 |
0acdf1f |
3f5ce95 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
5444 |
2018-12-06T09:48:59+01:00 |
8999e23 |
8999e23 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
5484 |
2018-12-06T06:25:46+01:00 |
|
Available Results for the Program from Witness Store SV-COMP '18
Trying to find witnesses for program (908f14d17c5d46378bef8bcd0f2fc540ebcd798d38e019b04475fc59574779d5, sv-benchmarks/c/eca-rers2012/Problem04_label45_false-unreach-call.c).
Found 5 witnesses for program sv-benchmarks/c/eca-rers2012/Problem04_label45_false-unreach-call.c, 908f14d17c5d46378bef8bcd0f2fc540ebcd798d38e019b04475fc59574779d5
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/908f14d17c5d46378bef8bcd0f2fc540ebcd798d38e019b04475fc59574779d5.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
1959f8a |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
ESBMC 4.6.0 kind |
7 |
2017-12-01T17:57:55.096024 |
|
22af404 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
ESBMC 4.6.0 incr |
7 |
2017-12-01T15:47:38.030661 |
|
ff0f520 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.6.1-svn 26773 |
3030 |
2017-11-30T17:02:04+01:00 |
|
4d70dc2 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.6.1-svn 26758M |
6937 |
2017-12-01T03:45:39+01:00 |
|
a30364b |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
2LS |
1989 |
2017-11-30T16:23 CET (sv-comp) |
|
Available Results for the Program from Witness Store SV-COMP '17
Trying to find witnesses for program (908f14d17c5d46378bef8bcd0f2fc540ebcd798d38e019b04475fc59574779d5, sv-benchmarks/c/eca-rers2012/Problem04_label45_false-unreach-call.c).
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem04_label45_false-unreach-call.c, 908f14d17c5d46378bef8bcd0f2fc540ebcd798d38e019b04475fc59574779d5
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/908f14d17c5d46378bef8bcd0f2fc540ebcd798d38e019b04475fc59574779d5.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |