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.5_false-unreach-call.1.ufo.BOUNDED-10.pals_true-termination.c |
programSHA |
173643450ebab49578d9af3e999dd5688eec7747f6cb440bb1db51105809a8ff |
witnessName |
results-verified/2ls.2017-11-30_1120.logfiles/sv-comp18.pals_lcr.5_false-unreach-call.1.ufo.BOUNDED-10.pals_true-termination.c.files/witness.graphml |
witnessSHA |
b9b6cc8d2330eb830bd260aa53d4777e1f449bd4c7317c50d3e5b44624fea4a4 |
Information about the Witness from Competition Database
from https://sv-comp.sosy-lab.org/2018/results/witnessInfoByHash/b9b6cc8d2330eb830bd260aa53d4777e1f449bd4c7317c50d3e5b44624fea4a4.json
Key |
Value |
architecture |
32bit |
creationtime |
2017-11-30T22:56 CET (sv-comp) |
producer |
2LS |
program-sha256 |
173643450ebab49578d9af3e999dd5688eec7747f6cb440bb1db51105809a8ff |
programfile |
../../sv-benchmarks/c/seq-mthreaded/pals_lcr.5_false-unreach-call.1.ufo.BOUNDED-10.pals_true-termination.c |
programhash |
6191f76ca1968cb0b63f42b60887059af617e3ab |
sourcecodelang |
C |
specification |
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file |
witnessFileByHash/b9b6cc8d2330eb830bd260aa53d4777e1f449bd4c7317c50d3e5b44624fea4a4.graphml |
witness-sha256 |
b9b6cc8d2330eb830bd260aa53d4777e1f449bd4c7317c50d3e5b44624fea4a4 |
witness-size |
172540 |
witness-type |
violation_witness |
Available Results for the Program from Witness Store SV-COMP '24
Trying to find witnesses for program (173643450ebab49578d9af3e999dd5688eec7747f6cb440bb1db51105809a8ff, sv-benchmarks/c/seq-mthreaded/pals_lcr.5_false-unreach-call.1.ufo.BOUNDED-10.pals_true-termination.c).
Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr.5_false-unreach-call.1.ufo.BOUNDED-10.pals_true-termination.c, 173643450ebab49578d9af3e999dd5688eec7747f6cb440bb1db51105809a8ff
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/173643450ebab49578d9af3e999dd5688eec7747f6cb440bb1db51105809a8ff.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 (173643450ebab49578d9af3e999dd5688eec7747f6cb440bb1db51105809a8ff, sv-benchmarks/c/seq-mthreaded/pals_lcr.5_false-unreach-call.1.ufo.BOUNDED-10.pals_true-termination.c).
Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr.5_false-unreach-call.1.ufo.BOUNDED-10.pals_true-termination.c, 173643450ebab49578d9af3e999dd5688eec7747f6cb440bb1db51105809a8ff
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/173643450ebab49578d9af3e999dd5688eec7747f6cb440bb1db51105809a8ff.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 (173643450ebab49578d9af3e999dd5688eec7747f6cb440bb1db51105809a8ff, sv-benchmarks/c/seq-mthreaded/pals_lcr.5_false-unreach-call.1.ufo.BOUNDED-10.pals_true-termination.c).
Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr.5_false-unreach-call.1.ufo.BOUNDED-10.pals_true-termination.c, 173643450ebab49578d9af3e999dd5688eec7747f6cb440bb1db51105809a8ff
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/173643450ebab49578d9af3e999dd5688eec7747f6cb440bb1db51105809a8ff.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 (173643450ebab49578d9af3e999dd5688eec7747f6cb440bb1db51105809a8ff, sv-benchmarks/c/seq-mthreaded/pals_lcr.5_false-unreach-call.1.ufo.BOUNDED-10.pals_true-termination.c).
Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr.5_false-unreach-call.1.ufo.BOUNDED-10.pals_true-termination.c, 173643450ebab49578d9af3e999dd5688eec7747f6cb440bb1db51105809a8ff
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/173643450ebab49578d9af3e999dd5688eec7747f6cb440bb1db51105809a8ff.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 (173643450ebab49578d9af3e999dd5688eec7747f6cb440bb1db51105809a8ff, sv-benchmarks/c/seq-mthreaded/pals_lcr.5_false-unreach-call.1.ufo.BOUNDED-10.pals_true-termination.c).
Found 12 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr.5_false-unreach-call.1.ufo.BOUNDED-10.pals_true-termination.c, 173643450ebab49578d9af3e999dd5688eec7747f6cb440bb1db51105809a8ff
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/173643450ebab49578d9af3e999dd5688eec7747f6cb440bb1db51105809a8ff.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
059870b |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
Pinaka |
186 |
2019-12-03T22:10 CET (comp) |
|
1dc1727 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
285 |
2019-12-11T21:59:51+01:00 |
47f2631 |
2e8d370 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
287 |
2019-12-11T20:44:52+01:00 |
91e25b7 |
224c6fa |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
285 |
2019-12-03T08:10:07+01:00 |
9ba4f78 |
9ba4f78 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / svcomp20 |
290 |
2019-11-30T05:16:52+01:00 |
|
47f2631 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco |
286 |
2019-12-01T02:16:14+01:00 |
|
ef5e2ec |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
42 |
2019-12-11T20:55:01+01:00 |
69c8780 |
2827633 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
42 |
2019-12-08T01:51:30+01:00 |
3e55251 |
226c5f9 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
42 |
2019-12-05T20:21:08+01:00 |
0f9d6be |
e9b0d25 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
42 |
2019-12-05T19:34:38+01:00 |
6816753 |
e84b054 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
42 |
2019-12-04T02:58:10+01:00 |
059870b |
95c9b29 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
Pinaka |
3 |
2019-12-04T00:09 CET (comp) |
|
Available Results for the Program from Witness Store SV-COMP '19
Trying to find witnesses for program (173643450ebab49578d9af3e999dd5688eec7747f6cb440bb1db51105809a8ff, sv-benchmarks/c/seq-mthreaded/pals_lcr.5_false-unreach-call.1.ufo.BOUNDED-10.pals_true-termination.c).
Found 16 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr.5_false-unreach-call.1.ufo.BOUNDED-10.pals_true-termination.c, 173643450ebab49578d9af3e999dd5688eec7747f6cb440bb1db51105809a8ff
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/173643450ebab49578d9af3e999dd5688eec7747f6cb440bb1db51105809a8ff.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
aea2621 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
Symbiotic |
10 |
2018-12-08T14:17 CET (sv-comp) |
|
74009d6 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
SMACK 1.9.3 |
75 |
2018-12-07T21:34:25 |
|
51e230d |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn b8d6131600+ |
289 |
2018-12-07T21:37:49+01:00 |
|
7b7a9d6 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
287 |
2018-12-09T18:21:28+01:00 |
1a40918 |
84392bb |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
286 |
2018-12-08T23:43:52+01:00 |
aea2621 |
c40f7e1 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
285 |
2018-12-08T08:28:34+01:00 |
51e230d |
174d604 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
285 |
2018-12-06T09:48:38+01:00 |
c48ce73 |
c48ce73 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
290 |
2018-12-05T15:35:17+01:00 |
|
161024f |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
42 |
2018-12-10T20:36:31+01:00 |
39bdd57 |
0976b91 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
42 |
2018-12-08T22:10:50+01:00 |
74009d6 |
32efcf4 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
42 |
2018-12-08T04:58:32+01:00 |
a85fd21 |
15f1d2a |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
42 |
2018-12-06T10:17:54+01:00 |
e832345 |
533be52 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
42 |
2018-12-06T09:41:48+01:00 |
f68eb14 |
4fb330f |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
42 |
2018-12-06T09:14:34+01:00 |
6ea7142 |
74c4c2e |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
Symbiotic |
1 |
2018-12-08T06:15 CET (sv-comp) |
|
42ac2a5 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
Pinaka |
3 |
2018-12-07T00:15 CET (sv-comp) |
|
Available Results for the Program from Witness Store SV-COMP '18
Trying to find witnesses for program (173643450ebab49578d9af3e999dd5688eec7747f6cb440bb1db51105809a8ff, sv-benchmarks/c/seq-mthreaded/pals_lcr.5_false-unreach-call.1.ufo.BOUNDED-10.pals_true-termination.c).
Found 13 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr.5_false-unreach-call.1.ufo.BOUNDED-10.pals_true-termination.c, 173643450ebab49578d9af3e999dd5688eec7747f6cb440bb1db51105809a8ff
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/173643450ebab49578d9af3e999dd5688eec7747f6cb440bb1db51105809a8ff.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
6520a99 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
VeriAbs 1.3 |
198 |
Sat Dec 2 23:15:25 2017 |
|
e453709 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
Symbiotic |
10 |
2017-12-02T17:05 CET (sv-comp) |
|
d3c5328 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
ESBMC 4.6.0 kind |
34 |
2017-12-02T03:32:50.717554 |
|
223c497 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
ESBMC 4.6.0 incr |
34 |
2017-12-01T18:10:06.023762 |
|
0b83989 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
ESBMC 3.1 |
93 |
2017-12-01T18:59 CET (sv-comp) |
|
59de491 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
ESBMC 3.1 |
91 |
2017-12-01T02:00 CET (sv-comp) |
|
a1cb3a7 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.6.1-svn 26773 |
284 |
2017-11-30T17:00:05+01:00 |
|
5775dbf |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CBMC |
207 |
2017-11-30T14:58 CET (sv-comp) |
|
b9b6cc8 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
2LS |
173 |
2017-11-30T22:56 CET (sv-comp) |
|
27df4f5 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
ESBMC 4.6.0 |
3 |
2017-12-03T00:42:29.315598 |
|
30490e4 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
ESBMC 4.6.0 |
3 |
2017-12-02T13:06:54.143293 |
|
e82acc2 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
CBMC |
325 |
2017-12-01T14:31 CET (sv-comp) |
|
c161076 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
2LS |
82 |
2017-12-01T13:35 CET (sv-comp) |
|
Available Results for the Program from Witness Store SV-COMP '17
Trying to find witnesses for program (173643450ebab49578d9af3e999dd5688eec7747f6cb440bb1db51105809a8ff, sv-benchmarks/c/seq-mthreaded/pals_lcr.5_false-unreach-call.1.ufo.BOUNDED-10.pals_true-termination.c).
Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr.5_false-unreach-call.1.ufo.BOUNDED-10.pals_true-termination.c, 173643450ebab49578d9af3e999dd5688eec7747f6cb440bb1db51105809a8ff
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/173643450ebab49578d9af3e999dd5688eec7747f6cb440bb1db51105809a8ff.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |