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/token_ring.09_false-unreach-call_false-termination.cil.c |
programSHA |
00ff1cfee32ce2d3a1261b504e67ec08dcd0f0d4c17d3c30695124a9acc108d3 |
witnessName |
results-verified/esbmc-kind.2018-12-06_1103.logfiles/sv-comp19_prop-reachsafety.token_ring.09_false-unreach-call_false-termination.cil.c.files/witness.graphml |
witnessSHA |
6f1d25a36bfa9045c73730243ff973a01ba596658835784954d0ae2b1c9a5f7c |
Information about the Witness from Competition Database
from https://sv-comp.sosy-lab.org/2019/results/witnessInfoByHash/6f1d25a36bfa9045c73730243ff973a01ba596658835784954d0ae2b1c9a5f7c.json
Key |
Value |
architecture |
32bit |
creationtime |
2018-12-07T00:04:03.490059 |
producer |
ESBMC 6.0.0 kind |
programfile |
../../sv-benchmarks/c/systemc/token_ring.09_false-unreach-call_false-termination.cil.c |
programhash |
7a3850d3a340e3061987e0b807f9867eab4f34a7 |
sourcecodelang |
C |
specification |
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file |
witnessFileByHash/6f1d25a36bfa9045c73730243ff973a01ba596658835784954d0ae2b1c9a5f7c.graphml |
witness-sha256 |
6f1d25a36bfa9045c73730243ff973a01ba596658835784954d0ae2b1c9a5f7c |
witness-size |
17981 |
witness-type |
violation_witness |
Available Results for the Program from Witness Store SV-COMP '24
Trying to find witnesses for program (00ff1cfee32ce2d3a1261b504e67ec08dcd0f0d4c17d3c30695124a9acc108d3, sv-benchmarks/c/systemc/token_ring.09_false-unreach-call_false-termination.cil.c).
Found 0 witnesses for program sv-benchmarks/c/systemc/token_ring.09_false-unreach-call_false-termination.cil.c, 00ff1cfee32ce2d3a1261b504e67ec08dcd0f0d4c17d3c30695124a9acc108d3
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/00ff1cfee32ce2d3a1261b504e67ec08dcd0f0d4c17d3c30695124a9acc108d3.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 (00ff1cfee32ce2d3a1261b504e67ec08dcd0f0d4c17d3c30695124a9acc108d3, sv-benchmarks/c/systemc/token_ring.09_false-unreach-call_false-termination.cil.c).
Found 0 witnesses for program sv-benchmarks/c/systemc/token_ring.09_false-unreach-call_false-termination.cil.c, 00ff1cfee32ce2d3a1261b504e67ec08dcd0f0d4c17d3c30695124a9acc108d3
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/00ff1cfee32ce2d3a1261b504e67ec08dcd0f0d4c17d3c30695124a9acc108d3.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 (00ff1cfee32ce2d3a1261b504e67ec08dcd0f0d4c17d3c30695124a9acc108d3, sv-benchmarks/c/systemc/token_ring.09_false-unreach-call_false-termination.cil.c).
Found 0 witnesses for program sv-benchmarks/c/systemc/token_ring.09_false-unreach-call_false-termination.cil.c, 00ff1cfee32ce2d3a1261b504e67ec08dcd0f0d4c17d3c30695124a9acc108d3
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/00ff1cfee32ce2d3a1261b504e67ec08dcd0f0d4c17d3c30695124a9acc108d3.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 (00ff1cfee32ce2d3a1261b504e67ec08dcd0f0d4c17d3c30695124a9acc108d3, sv-benchmarks/c/systemc/token_ring.09_false-unreach-call_false-termination.cil.c).
Found 0 witnesses for program sv-benchmarks/c/systemc/token_ring.09_false-unreach-call_false-termination.cil.c, 00ff1cfee32ce2d3a1261b504e67ec08dcd0f0d4c17d3c30695124a9acc108d3
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/00ff1cfee32ce2d3a1261b504e67ec08dcd0f0d4c17d3c30695124a9acc108d3.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 (00ff1cfee32ce2d3a1261b504e67ec08dcd0f0d4c17d3c30695124a9acc108d3, sv-benchmarks/c/systemc/token_ring.09_false-unreach-call_false-termination.cil.c).
Found 10 witnesses for program sv-benchmarks/c/systemc/token_ring.09_false-unreach-call_false-termination.cil.c, 00ff1cfee32ce2d3a1261b504e67ec08dcd0f0d4c17d3c30695124a9acc108d3
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/00ff1cfee32ce2d3a1261b504e67ec08dcd0f0d4c17d3c30695124a9acc108d3.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
6332be2 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
519 |
2019-12-11T21:59:19+01:00 |
9c0aa75 |
3847529 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
1755 |
2019-12-11T20:54:26+01:00 |
133c474 |
997bffa |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
619 |
2019-12-11T20:44:44+01:00 |
410268b |
7625e6f |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
519 |
2019-12-03T08:10:36+01:00 |
8541383 |
8541383 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / svcomp20 |
497 |
2019-11-30T10:45:15+01:00 |
|
9c0aa75 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco |
519 |
2019-12-01T00:27:58+01:00 |
|
38538c8 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
121 |
2019-12-08T01:52:23+01:00 |
5754996 |
943b353 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
121 |
2019-12-05T20:20:32+01:00 |
40dad27 |
72ca642 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
violation_witness |
CPAchecker 1.9 |
324 |
2019-11-30T13:45:26+01:00 |
|
5bf9c5d |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
violation_witness |
CPAchecker 1.8-svn-35b8bb3bb3+ |
324 |
2019-11-30T23:48:31+01:00 |
|
Available Results for the Program from Witness Store SV-COMP '19
Trying to find witnesses for program (00ff1cfee32ce2d3a1261b504e67ec08dcd0f0d4c17d3c30695124a9acc108d3, sv-benchmarks/c/systemc/token_ring.09_false-unreach-call_false-termination.cil.c).
Found 15 witnesses for program sv-benchmarks/c/systemc/token_ring.09_false-unreach-call_false-termination.cil.c, 00ff1cfee32ce2d3a1261b504e67ec08dcd0f0d4c17d3c30695124a9acc108d3
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/00ff1cfee32ce2d3a1261b504e67ec08dcd0f0d4c17d3c30695124a9acc108d3.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
7bf7e2a |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
Symbiotic |
1 |
2018-12-08T20:54 CET (sv-comp) |
|
39ba51e |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
SMACK 1.9.3 |
66 |
2018-12-08T08:32:07 |
|
ff90901 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn b8d6131600+ |
523 |
2018-12-07T00:19:00+01:00 |
|
a254120 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
519 |
2018-12-09T17:58:04+01:00 |
144c6f5 |
b62d17e |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
520 |
2018-12-08T23:44:45+01:00 |
7bf7e2a |
c7a48bb |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
519 |
2018-12-08T22:10:50+01:00 |
39ba51e |
ebbd606 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
519 |
2018-12-08T08:02:59+01:00 |
ff90901 |
a9dc2e7 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
519 |
2018-12-08T05:03:32+01:00 |
6f1d25a |
51860ab |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
519 |
2018-12-06T09:49:04+01:00 |
8b43c2b |
c93f84a |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
556 |
2018-12-06T09:10:33+01:00 |
d36547f |
8b43c2b |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
498 |
2018-12-06T05:18:39+01:00 |
|
8cba782 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
121 |
2018-12-10T20:35:10+01:00 |
0b5a8e5 |
6213b30 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
121 |
2018-12-06T10:19:10+01:00 |
7f31543 |
ff39e8a |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
violation_witness |
CPAchecker 1.7-svn b8d6131600+ |
324 |
2018-12-07T06:48:46+01:00 |
|
25f37da |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
324 |
2018-12-06T01:46:36+01:00 |
|
Available Results for the Program from Witness Store SV-COMP '18
Trying to find witnesses for program (00ff1cfee32ce2d3a1261b504e67ec08dcd0f0d4c17d3c30695124a9acc108d3, sv-benchmarks/c/systemc/token_ring.09_false-unreach-call_false-termination.cil.c).
Found 9 witnesses for program sv-benchmarks/c/systemc/token_ring.09_false-unreach-call_false-termination.cil.c, 00ff1cfee32ce2d3a1261b504e67ec08dcd0f0d4c17d3c30695124a9acc108d3
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/00ff1cfee32ce2d3a1261b504e67ec08dcd0f0d4c17d3c30695124a9acc108d3.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
f9fbe2a |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
VeriAbs 1.3 |
263 |
Sat Dec 2 23:53:30 2017 |
|
694b94b |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
Symbiotic |
1 |
2017-12-02T17:40 CET (sv-comp) |
|
85dba9c |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
ESBMC 4.6.0 kind |
20 |
2017-12-01T20:13:57.489833 |
|
711bc99 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
ESBMC 4.6.0 incr |
20 |
2017-12-01T19:19:07.537684 |
|
66030ef |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
ESBMC 3.1 |
188 |
2017-12-01T16:13 CET (sv-comp) |
|
9ef8231 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
ESBMC 3.1 |
188 |
2017-11-30T20:16 CET (sv-comp) |
|
2b792a9 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.6.1-svn 26773 |
450 |
2017-11-30T16:19:36+01:00 |
|
81389ad |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CBMC |
281 |
2017-12-01T00:10 CET (sv-comp) |
|
b5b5cea |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
violation_witness |
CPAchecker 1.6.1-svn 26773 |
322 |
2017-12-01T16:57:00+01:00 |
|
Available Results for the Program from Witness Store SV-COMP '17
Trying to find witnesses for program (00ff1cfee32ce2d3a1261b504e67ec08dcd0f0d4c17d3c30695124a9acc108d3, sv-benchmarks/c/systemc/token_ring.09_false-unreach-call_false-termination.cil.c).
Found 0 witnesses for program sv-benchmarks/c/systemc/token_ring.09_false-unreach-call_false-termination.cil.c, 00ff1cfee32ce2d3a1261b504e67ec08dcd0f0d4c17d3c30695124a9acc108d3
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/00ff1cfee32ce2d3a1261b504e67ec08dcd0f0d4c17d3c30695124a9acc108d3.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |