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/systemc/transmitter.06_false-unreach-call_false-termination.cil.c |
programSHA |
c860202d9b98d780eb3591998d871d58cf77863f82162bd43e7b308d412c4369 |
witnessName |
results-verified/esbmc-kind.2018-12-06_1103.logfiles/sv-comp19_prop-reachsafety.transmitter.06_false-unreach-call_false-termination.cil.c.files/witness.graphml |
witnessSHA |
12207e7ccffeec202cbd7f8b8a64a043e235e56a30a0fa9baa78d4d69fc9f509 |
Information about the Witness from Competition Database
from https://sv-comp.sosy-lab.org/2019/results/witnessInfoByHash/12207e7ccffeec202cbd7f8b8a64a043e235e56a30a0fa9baa78d4d69fc9f509.json
Key |
Value |
architecture |
32bit |
creationtime |
2018-12-07T16:58:46.715427 |
producer |
ESBMC 6.0.0 kind |
programfile |
../../sv-benchmarks/c/systemc/transmitter.06_false-unreach-call_false-termination.cil.c |
programhash |
7b5159bbdd5292a1bc0941c897062f30a665bf67 |
sourcecodelang |
C |
specification |
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file |
witnessFileByHash/12207e7ccffeec202cbd7f8b8a64a043e235e56a30a0fa9baa78d4d69fc9f509.graphml |
witness-sha256 |
12207e7ccffeec202cbd7f8b8a64a043e235e56a30a0fa9baa78d4d69fc9f509 |
witness-size |
10819 |
witness-type |
violation_witness |
Available Results for the Program from Witness Store SV-COMP '24
Trying to find witnesses for program (c860202d9b98d780eb3591998d871d58cf77863f82162bd43e7b308d412c4369, sv-benchmarks/c/systemc/transmitter.06_false-unreach-call_false-termination.cil.c).
Found 0 witnesses for program sv-benchmarks/c/systemc/transmitter.06_false-unreach-call_false-termination.cil.c, c860202d9b98d780eb3591998d871d58cf77863f82162bd43e7b308d412c4369
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/c860202d9b98d780eb3591998d871d58cf77863f82162bd43e7b308d412c4369.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 (c860202d9b98d780eb3591998d871d58cf77863f82162bd43e7b308d412c4369, sv-benchmarks/c/systemc/transmitter.06_false-unreach-call_false-termination.cil.c).
Found 0 witnesses for program sv-benchmarks/c/systemc/transmitter.06_false-unreach-call_false-termination.cil.c, c860202d9b98d780eb3591998d871d58cf77863f82162bd43e7b308d412c4369
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/c860202d9b98d780eb3591998d871d58cf77863f82162bd43e7b308d412c4369.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 (c860202d9b98d780eb3591998d871d58cf77863f82162bd43e7b308d412c4369, sv-benchmarks/c/systemc/transmitter.06_false-unreach-call_false-termination.cil.c).
Found 0 witnesses for program sv-benchmarks/c/systemc/transmitter.06_false-unreach-call_false-termination.cil.c, c860202d9b98d780eb3591998d871d58cf77863f82162bd43e7b308d412c4369
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/c860202d9b98d780eb3591998d871d58cf77863f82162bd43e7b308d412c4369.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 (c860202d9b98d780eb3591998d871d58cf77863f82162bd43e7b308d412c4369, sv-benchmarks/c/systemc/transmitter.06_false-unreach-call_false-termination.cil.c).
Found 0 witnesses for program sv-benchmarks/c/systemc/transmitter.06_false-unreach-call_false-termination.cil.c, c860202d9b98d780eb3591998d871d58cf77863f82162bd43e7b308d412c4369
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/c860202d9b98d780eb3591998d871d58cf77863f82162bd43e7b308d412c4369.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 (c860202d9b98d780eb3591998d871d58cf77863f82162bd43e7b308d412c4369, sv-benchmarks/c/systemc/transmitter.06_false-unreach-call_false-termination.cil.c).
Found 11 witnesses for program sv-benchmarks/c/systemc/transmitter.06_false-unreach-call_false-termination.cil.c, c860202d9b98d780eb3591998d871d58cf77863f82162bd43e7b308d412c4369
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/c860202d9b98d780eb3591998d871d58cf77863f82162bd43e7b308d412c4369.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
7d1a63d |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
Symbiotic |
4 |
2019-12-01 09:10:33 |
|
211a0b2 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
257 |
2019-12-11T22:00:49+01:00 |
bd8dcef |
8267103 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
257 |
2019-12-11T21:09:02+01:00 |
7d1a63d |
ca56410 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
269 |
2019-12-11T20:55:09+01:00 |
0a394d6 |
fdaccfc |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
286 |
2019-12-11T20:44:51+01:00 |
0bccd94 |
5d945ea |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
257 |
2019-12-08T00:26:08+01:00 |
7979f60 |
d435ec7 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
257 |
2019-12-03T08:09:58+01:00 |
84a5ab2 |
84a5ab2 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / svcomp20 |
225 |
2019-11-30T12:39:18+01:00 |
|
bd8dcef |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco |
256 |
2019-12-01T06:37:10+01:00 |
|
cdc3cf3 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
86 |
2019-12-08T01:51:30+01:00 |
ef01b88 |
1b1cb52 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
85 |
2019-12-05T20:20:23+01:00 |
3510a6b |
Available Results for the Program from Witness Store SV-COMP '19
Trying to find witnesses for program (c860202d9b98d780eb3591998d871d58cf77863f82162bd43e7b308d412c4369, sv-benchmarks/c/systemc/transmitter.06_false-unreach-call_false-termination.cil.c).
Found 14 witnesses for program sv-benchmarks/c/systemc/transmitter.06_false-unreach-call_false-termination.cil.c, c860202d9b98d780eb3591998d871d58cf77863f82162bd43e7b308d412c4369
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/c860202d9b98d780eb3591998d871d58cf77863f82162bd43e7b308d412c4369.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
2f70e60 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
Symbiotic |
1 |
2018-12-08T00:43 CET (sv-comp) |
|
21360be |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
SMACK 1.9.3 |
36 |
2018-12-08T07:46:57 |
|
f572e95 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn b8d6131600+ |
228 |
2018-12-08T03:31:54+01:00 |
|
2fc5221 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
257 |
2018-12-09T20:37:20+01:00 |
721a766 |
426ac5d |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
286 |
2018-12-09T18:20:28+01:00 |
d655d54 |
44bbfd7 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
257 |
2018-12-08T23:43:56+01:00 |
2f70e60 |
7cfb925 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
257 |
2018-12-08T22:10:43+01:00 |
21360be |
d40fce7 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
257 |
2018-12-08T08:26:42+01:00 |
f572e95 |
2f31eb3 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
268 |
2018-12-08T04:58:43+01:00 |
12207e7 |
069c690 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
554 |
2018-12-06T10:10:59+01:00 |
b186499 |
fa116e2 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
257 |
2018-12-06T09:49:20+01:00 |
c9eb871 |
ba4bb31 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
257 |
2018-12-06T09:17:19+01:00 |
a192481 |
c9eb871 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
225 |
2018-12-05T06:01:29+01:00 |
|
658ade6 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
86 |
2018-12-10T20:38:02+01:00 |
f011e18 |
Available Results for the Program from Witness Store SV-COMP '18
Trying to find witnesses for program (c860202d9b98d780eb3591998d871d58cf77863f82162bd43e7b308d412c4369, sv-benchmarks/c/systemc/transmitter.06_false-unreach-call_false-termination.cil.c).
Found 12 witnesses for program sv-benchmarks/c/systemc/transmitter.06_false-unreach-call_false-termination.cil.c, c860202d9b98d780eb3591998d871d58cf77863f82162bd43e7b308d412c4369
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/c860202d9b98d780eb3591998d871d58cf77863f82162bd43e7b308d412c4369.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
b108af5 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
VeriAbs 1.3 |
169 |
Sun Dec 3 02:21:46 2017 |
|
c56241d |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
Symbiotic |
1 |
2017-12-02T03:30 CET (sv-comp) |
|
f11b1d4 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
ESBMC 4.6.0 kind |
8 |
2017-12-01T13:55:47.965501 |
|
7a6f3b9 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
ESBMC 4.6.0 incr |
12 |
2017-12-01T14:20:52.885551 |
|
06ad1b5 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
ESBMC 3.1 |
59 |
2017-12-01T21:29 CET (sv-comp) |
|
bda5c88 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
ESBMC 3.1 |
59 |
2017-12-01T04:50 CET (sv-comp) |
|
c6a5a5b |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.6.1-svn 26773 |
202 |
2017-12-01T00:00:22+01:00 |
|
3f8aede |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.6.1-svn 26725 |
166 |
2017-11-30T11:59:06+01:00 |
|
ab1e13d |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker (unknown version) |
158 |
2017-12-01T20:32:16+01:00 |
|
3edba21 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CBMC |
124 |
2017-11-30T22:54 CET (sv-comp) |
|
64af6bd |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
Automizer |
297 |
2017-12-02T15:38Z |
|
2fd68bd |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
violation_witness |
Automizer |
79 |
2017-12-03T11:14Z |
|
Available Results for the Program from Witness Store SV-COMP '17
Trying to find witnesses for program (c860202d9b98d780eb3591998d871d58cf77863f82162bd43e7b308d412c4369, sv-benchmarks/c/systemc/transmitter.06_false-unreach-call_false-termination.cil.c).
Found 0 witnesses for program sv-benchmarks/c/systemc/transmitter.06_false-unreach-call_false-termination.cil.c, c860202d9b98d780eb3591998d871d58cf77863f82162bd43e7b308d412c4369
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/c860202d9b98d780eb3591998d871d58cf77863f82162bd43e7b308d412c4369.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |