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/seq-mthreaded/pals_lcr.6_false-unreach-call.1.ufo.BOUNDED-12.pals_true-termination.c |
programSHA |
3ab610159f56c036f39e8a23e5cb747b7d0a2988f45bbfca01e27a6c34fcfa42 |
witnessName |
results-verified/veriabs.2017-12-02_1804.logfiles/sv-comp18.pals_lcr.6_false-unreach-call.1.ufo.BOUNDED-12.pals_true-termination.c.files/witness.graphml |
witnessSHA |
bcf32c120797358ea6e0db446820a3f1f5e934312c63241e3b2af49a40899096 |
Information about the Witness from Competition Database
from https://sv-comp.sosy-lab.org/2018/results/witnessInfoByHash/bcf32c120797358ea6e0db446820a3f1f5e934312c63241e3b2af49a40899096.json
Key |
Value |
architecture |
32bit |
creationtime |
Sun Dec 3 01:13:37 2017 |
producer |
VeriAbs 1.3 |
program-sha256 |
3ab610159f56c036f39e8a23e5cb747b7d0a2988f45bbfca01e27a6c34fcfa42 |
programfile |
/home/benchexec/ar_abs_temp/pals_lcr_6_false_unreach_call_1_ufo_BOUNDED_12_pals_true_termination_c.c |
programhash |
bd200d2db4e8741128c4082e326a133517d9c82f |
sourcecodelang |
C |
specification |
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file |
witnessFileByHash/bcf32c120797358ea6e0db446820a3f1f5e934312c63241e3b2af49a40899096.graphml |
witness-sha256 |
bcf32c120797358ea6e0db446820a3f1f5e934312c63241e3b2af49a40899096 |
witness-size |
272576 |
witness-type |
violation_witness |
Available Results for the Program from Witness Store SV-COMP '24
Trying to find witnesses for program (3ab610159f56c036f39e8a23e5cb747b7d0a2988f45bbfca01e27a6c34fcfa42, sv-benchmarks/c/seq-mthreaded/pals_lcr.6_false-unreach-call.1.ufo.BOUNDED-12.pals_true-termination.c).
Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr.6_false-unreach-call.1.ufo.BOUNDED-12.pals_true-termination.c, 3ab610159f56c036f39e8a23e5cb747b7d0a2988f45bbfca01e27a6c34fcfa42
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/3ab610159f56c036f39e8a23e5cb747b7d0a2988f45bbfca01e27a6c34fcfa42.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 (3ab610159f56c036f39e8a23e5cb747b7d0a2988f45bbfca01e27a6c34fcfa42, sv-benchmarks/c/seq-mthreaded/pals_lcr.6_false-unreach-call.1.ufo.BOUNDED-12.pals_true-termination.c).
Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr.6_false-unreach-call.1.ufo.BOUNDED-12.pals_true-termination.c, 3ab610159f56c036f39e8a23e5cb747b7d0a2988f45bbfca01e27a6c34fcfa42
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/3ab610159f56c036f39e8a23e5cb747b7d0a2988f45bbfca01e27a6c34fcfa42.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 (3ab610159f56c036f39e8a23e5cb747b7d0a2988f45bbfca01e27a6c34fcfa42, sv-benchmarks/c/seq-mthreaded/pals_lcr.6_false-unreach-call.1.ufo.BOUNDED-12.pals_true-termination.c).
Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr.6_false-unreach-call.1.ufo.BOUNDED-12.pals_true-termination.c, 3ab610159f56c036f39e8a23e5cb747b7d0a2988f45bbfca01e27a6c34fcfa42
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/3ab610159f56c036f39e8a23e5cb747b7d0a2988f45bbfca01e27a6c34fcfa42.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 (3ab610159f56c036f39e8a23e5cb747b7d0a2988f45bbfca01e27a6c34fcfa42, sv-benchmarks/c/seq-mthreaded/pals_lcr.6_false-unreach-call.1.ufo.BOUNDED-12.pals_true-termination.c).
Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr.6_false-unreach-call.1.ufo.BOUNDED-12.pals_true-termination.c, 3ab610159f56c036f39e8a23e5cb747b7d0a2988f45bbfca01e27a6c34fcfa42
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/3ab610159f56c036f39e8a23e5cb747b7d0a2988f45bbfca01e27a6c34fcfa42.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 (3ab610159f56c036f39e8a23e5cb747b7d0a2988f45bbfca01e27a6c34fcfa42, sv-benchmarks/c/seq-mthreaded/pals_lcr.6_false-unreach-call.1.ufo.BOUNDED-12.pals_true-termination.c).
Found 9 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr.6_false-unreach-call.1.ufo.BOUNDED-12.pals_true-termination.c, 3ab610159f56c036f39e8a23e5cb747b7d0a2988f45bbfca01e27a6c34fcfa42
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/3ab610159f56c036f39e8a23e5cb747b7d0a2988f45bbfca01e27a6c34fcfa42.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
3a7ec75 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
392 |
2019-12-11T21:42:25+01:00 |
27f5f76 |
732a83a |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
392 |
2019-12-03T08:09:45+01:00 |
1bbc9a1 |
1bbc9a1 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / svcomp20 |
398 |
2019-11-30T09:33:33+01:00 |
|
27f5f76 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco |
393 |
2019-12-01T08:46:31+01:00 |
|
ce2db74 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
50 |
2019-12-11T20:55:21+01:00 |
b0c20d8 |
f4e99c9 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
50 |
2019-12-11T20:45:49+01:00 |
f4292d4 |
9e9c07f |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
50 |
2019-12-08T01:51:18+01:00 |
55493cd |
1eac9fd |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
50 |
2019-12-05T20:21:47+01:00 |
aebab3c |
703e689 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
50 |
2019-12-05T19:34:04+01:00 |
7684acb |
Available Results for the Program from Witness Store SV-COMP '19
Trying to find witnesses for program (3ab610159f56c036f39e8a23e5cb747b7d0a2988f45bbfca01e27a6c34fcfa42, sv-benchmarks/c/seq-mthreaded/pals_lcr.6_false-unreach-call.1.ufo.BOUNDED-12.pals_true-termination.c).
Found 15 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr.6_false-unreach-call.1.ufo.BOUNDED-12.pals_true-termination.c, 3ab610159f56c036f39e8a23e5cb747b7d0a2988f45bbfca01e27a6c34fcfa42
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/3ab610159f56c036f39e8a23e5cb747b7d0a2988f45bbfca01e27a6c34fcfa42.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
bbb7bae |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
Symbiotic |
11 |
2018-12-08T00:21 CET (sv-comp) |
|
8457f4d |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
SMACK 1.9.3 |
104 |
2018-12-08T05:03:07 |
|
ce49f7c |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn b8d6131600+ |
396 |
2018-12-07T19:06:28+01:00 |
|
06c0632 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
392 |
2018-12-08T23:44:08+01:00 |
bbb7bae |
e2e4754 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
392 |
2018-12-08T08:27:10+01:00 |
ce49f7c |
51f0952 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
392 |
2018-12-06T09:48:55+01:00 |
94fe409 |
94fe409 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
398 |
2018-12-05T22:03:12+01:00 |
|
b42a24c |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
50 |
2018-12-10T20:35:14+01:00 |
c6d8fb4 |
ced857d |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
50 |
2018-12-09T18:21:37+01:00 |
a60def9 |
30d4a96 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
50 |
2018-12-08T22:10:37+01:00 |
8457f4d |
9ac7b05 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
50 |
2018-12-08T04:56:32+01:00 |
21a8304 |
0c781f1 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
50 |
2018-12-06T10:11:59+01:00 |
901c561 |
baa4518 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
50 |
2018-12-06T09:42:31+01:00 |
87e326b |
4597add |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
50 |
2018-12-06T09:12:39+01:00 |
994d591 |
b9e0e9f |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
Symbiotic |
1 |
2018-12-08T00:32 CET (sv-comp) |
|
Available Results for the Program from Witness Store SV-COMP '18
Trying to find witnesses for program (3ab610159f56c036f39e8a23e5cb747b7d0a2988f45bbfca01e27a6c34fcfa42, sv-benchmarks/c/seq-mthreaded/pals_lcr.6_false-unreach-call.1.ufo.BOUNDED-12.pals_true-termination.c).
Found 13 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr.6_false-unreach-call.1.ufo.BOUNDED-12.pals_true-termination.c, 3ab610159f56c036f39e8a23e5cb747b7d0a2988f45bbfca01e27a6c34fcfa42
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/3ab610159f56c036f39e8a23e5cb747b7d0a2988f45bbfca01e27a6c34fcfa42.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
bcf32c1 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
VeriAbs 1.3 |
273 |
Sun Dec 3 01:13:37 2017 |
|
b5af582 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
Symbiotic |
11 |
2017-12-01T23:17 CET (sv-comp) |
|
4fc87c3 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
ESBMC 4.6.0 kind |
46 |
2017-12-01T12:06:08.955467 |
|
4ebb908 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
ESBMC 4.6.0 incr |
46 |
2017-12-01T11:15:15.699453 |
|
ef26c04 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
ESBMC 3.1 |
126 |
2017-12-01T18:51 CET (sv-comp) |
|
1fa99a3 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
ESBMC 3.1 |
124 |
2017-12-01T02:43 CET (sv-comp) |
|
d8206c0 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.6.1-svn 26773 |
389 |
2017-12-01T00:38:38+01:00 |
|
27c904f |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CBMC |
284 |
2017-11-30T20:57 CET (sv-comp) |
|
97bc470 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
2LS |
237 |
2017-11-30T16:58 CET (sv-comp) |
|
c75caca |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
ESBMC 4.6.0 |
3 |
2017-12-02T23:45:30.121741 |
|
285cd2e |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
ESBMC 4.6.0 |
3 |
2017-12-02T13:07:46.114061 |
|
a6d090e |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
CBMC |
451 |
2017-12-01T13:48 CET (sv-comp) |
|
b966ec7 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
2LS |
96 |
2017-12-01T13:19 CET (sv-comp) |
|
Available Results for the Program from Witness Store SV-COMP '17
Trying to find witnesses for program (3ab610159f56c036f39e8a23e5cb747b7d0a2988f45bbfca01e27a6c34fcfa42, sv-benchmarks/c/seq-mthreaded/pals_lcr.6_false-unreach-call.1.ufo.BOUNDED-12.pals_true-termination.c).
Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr.6_false-unreach-call.1.ufo.BOUNDED-12.pals_true-termination.c, 3ab610159f56c036f39e8a23e5cb747b7d0a2988f45bbfca01e27a6c34fcfa42
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/3ab610159f56c036f39e8a23e5cb747b7d0a2988f45bbfca01e27a6c34fcfa42.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |