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/Problem03_label52_false-unreach-call.c |
programSHA |
298c53c55da2f9a0850df007856c1242aa182e4120e893e20abcd0af3dffff10 |
witnessName |
results-verified/uautomizer.2017-12-02_0106.logfiles/sv-comp18.Problem03_label52_false-unreach-call.c.files/witness.graphml |
witnessSHA |
6217eb36a68b967f0d8ee8257833988e39854e8d04f801e6c904541d1a7d6379 |
Information about the Witness from Competition Database
from https://sv-comp.sosy-lab.org/2018/results/witnessInfoByHash/6217eb36a68b967f0d8ee8257833988e39854e8d04f801e6c904541d1a7d6379.json
Key |
Value |
architecture |
32bit |
creationtime |
2017-12-02T08:24Z |
producer |
Automizer |
program-sha256 |
298c53c55da2f9a0850df007856c1242aa182e4120e893e20abcd0af3dffff10 |
programfile |
/tmp/vcloud-vcloud-master/worker/working_dir_d5bf769d-2773-41dc-9d3b-b548fbd5da75/sv-benchmarks/c/eca-rers2012/Problem03_label52_false-unreach-call.c |
programhash |
a8ebdf64f0077e22b80debc67321cfe2296f5e0e |
sourcecodelang |
C |
specification |
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
|
witness-file |
witnessFileByHash/6217eb36a68b967f0d8ee8257833988e39854e8d04f801e6c904541d1a7d6379.graphml |
witness-sha256 |
6217eb36a68b967f0d8ee8257833988e39854e8d04f801e6c904541d1a7d6379 |
witness-size |
526596 |
witness-type |
violation_witness |
Available Results for the Program from Witness Store SV-COMP '24
Trying to find witnesses for program (298c53c55da2f9a0850df007856c1242aa182e4120e893e20abcd0af3dffff10, sv-benchmarks/c/eca-rers2012/Problem03_label52_false-unreach-call.c).
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem03_label52_false-unreach-call.c, 298c53c55da2f9a0850df007856c1242aa182e4120e893e20abcd0af3dffff10
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/298c53c55da2f9a0850df007856c1242aa182e4120e893e20abcd0af3dffff10.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 (298c53c55da2f9a0850df007856c1242aa182e4120e893e20abcd0af3dffff10, sv-benchmarks/c/eca-rers2012/Problem03_label52_false-unreach-call.c).
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem03_label52_false-unreach-call.c, 298c53c55da2f9a0850df007856c1242aa182e4120e893e20abcd0af3dffff10
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/298c53c55da2f9a0850df007856c1242aa182e4120e893e20abcd0af3dffff10.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 (298c53c55da2f9a0850df007856c1242aa182e4120e893e20abcd0af3dffff10, sv-benchmarks/c/eca-rers2012/Problem03_label52_false-unreach-call.c).
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem03_label52_false-unreach-call.c, 298c53c55da2f9a0850df007856c1242aa182e4120e893e20abcd0af3dffff10
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/298c53c55da2f9a0850df007856c1242aa182e4120e893e20abcd0af3dffff10.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 (298c53c55da2f9a0850df007856c1242aa182e4120e893e20abcd0af3dffff10, sv-benchmarks/c/eca-rers2012/Problem03_label52_false-unreach-call.c).
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem03_label52_false-unreach-call.c, 298c53c55da2f9a0850df007856c1242aa182e4120e893e20abcd0af3dffff10
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/298c53c55da2f9a0850df007856c1242aa182e4120e893e20abcd0af3dffff10.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 (298c53c55da2f9a0850df007856c1242aa182e4120e893e20abcd0af3dffff10, sv-benchmarks/c/eca-rers2012/Problem03_label52_false-unreach-call.c).
Found 11 witnesses for program sv-benchmarks/c/eca-rers2012/Problem03_label52_false-unreach-call.c, 298c53c55da2f9a0850df007856c1242aa182e4120e893e20abcd0af3dffff10
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/298c53c55da2f9a0850df007856c1242aa182e4120e893e20abcd0af3dffff10.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
40ba804 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
Symbiotic |
2 |
2019-12-02 03:45:27 |
|
0913d24 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
Pinaka |
161 |
2019-12-03T21:45 CET (comp) |
|
843fe18 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
552 |
2019-12-11T21:44:59+01:00 |
6f6fae7 |
e7b5f10 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
552 |
2019-12-11T21:09:13+01:00 |
40ba804 |
90f8d38 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
552 |
2019-12-11T20:55:28+01:00 |
3137273 |
b92f5f1 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
552 |
2019-12-11T20:44:55+01:00 |
a076511 |
44f3719 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
555 |
2019-12-08T01:52:42+01:00 |
9e2665a |
26e1172 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
740 |
2019-12-04T02:58:10+01:00 |
0913d24 |
196f8d8 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
552 |
2019-12-03T08:08:11+01:00 |
acdb36b |
acdb36b |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / svcomp20 |
553 |
2019-11-29T18:50:33+01:00 |
|
6f6fae7 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco |
553 |
2019-11-30T23:46:05+01:00 |
|
Available Results for the Program from Witness Store SV-COMP '19
Trying to find witnesses for program (298c53c55da2f9a0850df007856c1242aa182e4120e893e20abcd0af3dffff10, sv-benchmarks/c/eca-rers2012/Problem03_label52_false-unreach-call.c).
Found 15 witnesses for program sv-benchmarks/c/eca-rers2012/Problem03_label52_false-unreach-call.c, 298c53c55da2f9a0850df007856c1242aa182e4120e893e20abcd0af3dffff10
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/298c53c55da2f9a0850df007856c1242aa182e4120e893e20abcd0af3dffff10.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
33156e8 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
Symbiotic |
1 |
2018-12-08T13:35 CET (sv-comp) |
|
de44a25 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
SMACK 1.9.3 |
13 |
2018-12-07T20:24:00 |
|
69b764b |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
Pinaka |
175 |
2018-12-07T07:44 CET (sv-comp) |
|
fbd0e84 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn b8d6131600+ |
557 |
2018-12-07T15:50:12+01:00 |
|
794378a |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
555 |
2018-12-10T20:36:52+01:00 |
7ae5660 |
4c327aa |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
552 |
2018-12-09T18:17:24+01:00 |
c6fb56f |
49891b2 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
557 |
2018-12-08T23:43:06+01:00 |
33156e8 |
40f3050 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
552 |
2018-12-08T22:10:10+01:00 |
de44a25 |
3597b4d |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
552 |
2018-12-08T09:01:53+01:00 |
fbd0e84 |
2feea51 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
552 |
2018-12-08T05:01:59+01:00 |
e341863 |
d453aa7 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
740 |
2018-12-07T17:43:00+01:00 |
69b764b |
f91243b |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
552 |
2018-12-06T10:12:40+01:00 |
d5d67fd |
9142552 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
552 |
2018-12-06T09:48:28+01:00 |
b8476c9 |
793d642 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
740 |
2018-12-06T09:18:12+01:00 |
785652a |
b8476c9 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
553 |
2018-12-05T20:02:35+01:00 |
|
Available Results for the Program from Witness Store SV-COMP '18
Trying to find witnesses for program (298c53c55da2f9a0850df007856c1242aa182e4120e893e20abcd0af3dffff10, sv-benchmarks/c/eca-rers2012/Problem03_label52_false-unreach-call.c).
Found 10 witnesses for program sv-benchmarks/c/eca-rers2012/Problem03_label52_false-unreach-call.c, 298c53c55da2f9a0850df007856c1242aa182e4120e893e20abcd0af3dffff10
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/298c53c55da2f9a0850df007856c1242aa182e4120e893e20abcd0af3dffff10.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
baaea51 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
VeriAbs 1.3 |
321 |
Sun Dec 3 02:36:52 2017 |
|
f72d8cc |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
Symbiotic |
1 |
2017-12-02T02:18 CET (sv-comp) |
|
e7151cc |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
ESBMC 4.6.0 kind |
5 |
2017-12-01T13:43:56.417978 |
|
50b4e87 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
ESBMC 4.6.0 incr |
5 |
2017-12-01T10:35:41.800352 |
|
09198e5 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
ESBMC 3.1 |
20 |
2017-12-01T05:21 CET (sv-comp) |
|
15decf5 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.6.1-svn 26773 |
316 |
2017-11-30T14:10:28+01:00 |
|
18001d2 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.6.1-svn 26758M |
1244 |
2017-11-30T15:50:02+01:00 |
|
0b312d8 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CBMC |
198 |
2017-11-30T16:42 CET (sv-comp) |
|
6217eb3 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
Automizer |
527 |
2017-12-02T08:24Z |
|
48211d6 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
2LS |
199 |
2017-11-30T21:17 CET (sv-comp) |
|
Available Results for the Program from Witness Store SV-COMP '17
Trying to find witnesses for program (298c53c55da2f9a0850df007856c1242aa182e4120e893e20abcd0af3dffff10, sv-benchmarks/c/eca-rers2012/Problem03_label52_false-unreach-call.c).
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem03_label52_false-unreach-call.c, 298c53c55da2f9a0850df007856c1242aa182e4120e893e20abcd0af3dffff10
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/298c53c55da2f9a0850df007856c1242aa182e4120e893e20abcd0af3dffff10.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |