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.02_true-unreach-call_false-termination.cil.c |
programSHA |
403fe230a852bf1ff90c224c8ad101752c12e041751795435b361434f4f71ae9 |
witnessName |
results-verified/utaipan.2018-12-08_1419.logfiles/sv-comp19_prop-reachsafety.token_ring.02_true-unreach-call_false-termination.cil.c.files/witness.graphml |
witnessSHA |
1007f63b58955a24498a3fa729cc92b4564e284403ba763cabb268e120ba9f9a |
Information about the Witness from Competition Database
from https://sv-comp.sosy-lab.org/2019/results/witnessInfoByHash/1007f63b58955a24498a3fa729cc92b4564e284403ba763cabb268e120ba9f9a.json
Key |
Value |
architecture |
32bit |
creationtime |
2018-12-09T08:15Z |
producer |
Taipan |
programfile |
/tmp/vcloud-vcloud-master/worker/working_dir_67888dcd-c8c9-4013-8990-7ab3a02a51e3/sv-benchmarks/c/systemc/token_ring.02_true-unreach-call_false-termination.cil.c |
programhash |
e3d58fadf54daed6107b58402b79d250d23d0301 |
sourcecodelang |
C |
specification |
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
|
witness-file |
witnessFileByHash/1007f63b58955a24498a3fa729cc92b4564e284403ba763cabb268e120ba9f9a.graphml |
witness-sha256 |
1007f63b58955a24498a3fa729cc92b4564e284403ba763cabb268e120ba9f9a |
witness-size |
80103 |
witness-type |
correctness_witness |
Available Results for the Program from Witness Store SV-COMP '24
Trying to find witnesses for program (403fe230a852bf1ff90c224c8ad101752c12e041751795435b361434f4f71ae9, sv-benchmarks/c/systemc/token_ring.02_true-unreach-call_false-termination.cil.c).
Found 0 witnesses for program sv-benchmarks/c/systemc/token_ring.02_true-unreach-call_false-termination.cil.c, 403fe230a852bf1ff90c224c8ad101752c12e041751795435b361434f4f71ae9
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/403fe230a852bf1ff90c224c8ad101752c12e041751795435b361434f4f71ae9.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 (403fe230a852bf1ff90c224c8ad101752c12e041751795435b361434f4f71ae9, sv-benchmarks/c/systemc/token_ring.02_true-unreach-call_false-termination.cil.c).
Found 0 witnesses for program sv-benchmarks/c/systemc/token_ring.02_true-unreach-call_false-termination.cil.c, 403fe230a852bf1ff90c224c8ad101752c12e041751795435b361434f4f71ae9
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/403fe230a852bf1ff90c224c8ad101752c12e041751795435b361434f4f71ae9.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 (403fe230a852bf1ff90c224c8ad101752c12e041751795435b361434f4f71ae9, sv-benchmarks/c/systemc/token_ring.02_true-unreach-call_false-termination.cil.c).
Found 0 witnesses for program sv-benchmarks/c/systemc/token_ring.02_true-unreach-call_false-termination.cil.c, 403fe230a852bf1ff90c224c8ad101752c12e041751795435b361434f4f71ae9
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/403fe230a852bf1ff90c224c8ad101752c12e041751795435b361434f4f71ae9.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 (403fe230a852bf1ff90c224c8ad101752c12e041751795435b361434f4f71ae9, sv-benchmarks/c/systemc/token_ring.02_true-unreach-call_false-termination.cil.c).
Found 0 witnesses for program sv-benchmarks/c/systemc/token_ring.02_true-unreach-call_false-termination.cil.c, 403fe230a852bf1ff90c224c8ad101752c12e041751795435b361434f4f71ae9
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/403fe230a852bf1ff90c224c8ad101752c12e041751795435b361434f4f71ae9.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 (403fe230a852bf1ff90c224c8ad101752c12e041751795435b361434f4f71ae9, sv-benchmarks/c/systemc/token_ring.02_true-unreach-call_false-termination.cil.c).
Found 8 witnesses for program sv-benchmarks/c/systemc/token_ring.02_true-unreach-call_false-termination.cil.c, 403fe230a852bf1ff90c224c8ad101752c12e041751795435b361434f4f71ae9
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/403fe230a852bf1ff90c224c8ad101752c12e041751795435b361434f4f71ae9.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
91dd8ba |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
48 |
2019-12-11T20:14:36+01:00 |
3ed5f06 |
205ccbf |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
48 |
2019-12-07T23:32:27+01:00 |
462d980 |
b3271d1 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
48 |
2019-12-07T19:44:27+01:00 |
278664a |
8b32a43 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
48 |
2019-11-30T16:26:40+01:00 |
4107234 |
4107234 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / svcomp20 |
48 |
2019-11-30T04:41:29+01:00 |
|
3ed5f06 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco |
48 |
2019-11-30T20:51:49+01:00 |
|
b7568ad |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
violation_witness |
CPAchecker 1.9 |
59 |
2019-11-29T21:28:08+01:00 |
|
6d2ec67 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
violation_witness |
CPAchecker 1.8-svn-35b8bb3bb3+ |
59 |
2019-11-30T23:44:35+01:00 |
|
Available Results for the Program from Witness Store SV-COMP '19
Trying to find witnesses for program (403fe230a852bf1ff90c224c8ad101752c12e041751795435b361434f4f71ae9, sv-benchmarks/c/systemc/token_ring.02_true-unreach-call_false-termination.cil.c).
Found 11 witnesses for program sv-benchmarks/c/systemc/token_ring.02_true-unreach-call_false-termination.cil.c, 403fe230a852bf1ff90c224c8ad101752c12e041751795435b361434f4f71ae9
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/403fe230a852bf1ff90c224c8ad101752c12e041751795435b361434f4f71ae9.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
782d3fa |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
SMACK 1.9.3 |
3 |
2018-12-08T09:34:34 |
|
5b87c0b |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn b8d6131600+ |
48 |
2018-12-08T02:50:22+01:00 |
|
64a4716 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
49 |
2018-12-09T20:49:10+01:00 |
1007f63 |
f59c879 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
49 |
2018-12-09T20:17:00+01:00 |
ae764ff |
e06ea83 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
49 |
2018-12-08T21:57:10+01:00 |
782d3fa |
6c98dda |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
49 |
2018-12-08T07:33:26+01:00 |
5b87c0b |
dcd43c0 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
49 |
2018-12-06T09:42:59+01:00 |
a54ae8a |
acf7095 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
49 |
2018-12-06T09:00:16+01:00 |
d9f18ef |
d9f18ef |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
48 |
2018-12-05T12:46:21+01:00 |
|
d9fb55d |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
violation_witness |
CPAchecker 1.7-svn b8d6131600+ |
59 |
2018-12-08T00:34:01+01:00 |
|
7a3d40f |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
59 |
2018-12-05T19:07:32+01:00 |
|
Available Results for the Program from Witness Store SV-COMP '18
Trying to find witnesses for program (403fe230a852bf1ff90c224c8ad101752c12e041751795435b361434f4f71ae9, sv-benchmarks/c/systemc/token_ring.02_true-unreach-call_false-termination.cil.c).
Found 10 witnesses for program sv-benchmarks/c/systemc/token_ring.02_true-unreach-call_false-termination.cil.c, 403fe230a852bf1ff90c224c8ad101752c12e041751795435b361434f4f71ae9
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/403fe230a852bf1ff90c224c8ad101752c12e041751795435b361434f4f71ae9.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
22a4e6f |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.6.1-svn 26773 |
48 |
2017-12-03T02:52:55+01:00 |
2a88eca |
f4a2a6f |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.6.1-svn 26773 |
48 |
2017-12-02T14:47:23+01:00 |
28e6bd0 |
7040929 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.6.1-svn 26773 |
48 |
2017-12-01T07:09:38+01:00 |
6b93477 |
af40b60 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.6.1-svn 26773 |
48 |
2017-12-01T05:26:39+01:00 |
8b9dfd6 |
d5d2035 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.6.1-svn 26773 |
48 |
2017-11-30T22:11:55+01:00 |
|
8f5eae5 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.6.1-svn 26725 |
48 |
2017-11-30T18:39:19+01:00 |
|
ea0f4ca |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker (unknown version) |
43 |
2017-12-01T23:32:10+01:00 |
|
9b7f822 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
Automizer |
85 |
2017-12-02T09:17Z |
|
b9d5291 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
violation_witness |
CPAchecker 1.6.1-svn 26773 |
59 |
2017-12-01T15:53:21+01:00 |
|
e117692 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
violation_witness |
Automizer |
43 |
2017-12-03T11:13Z |
|
Available Results for the Program from Witness Store SV-COMP '17
Trying to find witnesses for program (403fe230a852bf1ff90c224c8ad101752c12e041751795435b361434f4f71ae9, sv-benchmarks/c/systemc/token_ring.02_true-unreach-call_false-termination.cil.c).
Found 0 witnesses for program sv-benchmarks/c/systemc/token_ring.02_true-unreach-call_false-termination.cil.c, 403fe230a852bf1ff90c224c8ad101752c12e041751795435b361434f4f71ae9
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/403fe230a852bf1ff90c224c8ad101752c12e041751795435b361434f4f71ae9.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |