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_floodmax.4_false-unreach-call.1.ufo.BOUNDED-8.pals_true-termination.c |
programSHA |
ebcfc2636c039ce113df9bd4fa1f4a0e9e0d33e9c8dafec5242235f0c95c3d3d |
witnessName |
results-verified/2ls.2017-11-30_1120.logfiles/sv-comp18.pals_floodmax.4_false-unreach-call.1.ufo.BOUNDED-8.pals_true-termination.c.files/witness.graphml |
witnessSHA |
211eeb437ae0a46bd255ea50c9c03325f2629d3992b5ad1c895dbb92ee4e0433 |
Information about the Witness from Competition Database
from https://sv-comp.sosy-lab.org/2018/results/witnessInfoByHash/211eeb437ae0a46bd255ea50c9c03325f2629d3992b5ad1c895dbb92ee4e0433.json
Key |
Value |
architecture |
32bit |
creationtime |
2017-11-30T18:04 CET (sv-comp) |
producer |
2LS |
program-sha256 |
ebcfc2636c039ce113df9bd4fa1f4a0e9e0d33e9c8dafec5242235f0c95c3d3d |
programfile |
../../sv-benchmarks/c/seq-mthreaded/pals_floodmax.4_false-unreach-call.1.ufo.BOUNDED-8.pals_true-termination.c |
programhash |
188aaf9001adccb91c68b27294cad7318066e2a0 |
sourcecodelang |
C |
specification |
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file |
witnessFileByHash/211eeb437ae0a46bd255ea50c9c03325f2629d3992b5ad1c895dbb92ee4e0433.graphml |
witness-sha256 |
211eeb437ae0a46bd255ea50c9c03325f2629d3992b5ad1c895dbb92ee4e0433 |
witness-size |
199143 |
witness-type |
violation_witness |
Available Results for the Program from Witness Store SV-COMP '24
Trying to find witnesses for program (ebcfc2636c039ce113df9bd4fa1f4a0e9e0d33e9c8dafec5242235f0c95c3d3d, sv-benchmarks/c/seq-mthreaded/pals_floodmax.4_false-unreach-call.1.ufo.BOUNDED-8.pals_true-termination.c).
Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_floodmax.4_false-unreach-call.1.ufo.BOUNDED-8.pals_true-termination.c, ebcfc2636c039ce113df9bd4fa1f4a0e9e0d33e9c8dafec5242235f0c95c3d3d
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/ebcfc2636c039ce113df9bd4fa1f4a0e9e0d33e9c8dafec5242235f0c95c3d3d.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 (ebcfc2636c039ce113df9bd4fa1f4a0e9e0d33e9c8dafec5242235f0c95c3d3d, sv-benchmarks/c/seq-mthreaded/pals_floodmax.4_false-unreach-call.1.ufo.BOUNDED-8.pals_true-termination.c).
Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_floodmax.4_false-unreach-call.1.ufo.BOUNDED-8.pals_true-termination.c, ebcfc2636c039ce113df9bd4fa1f4a0e9e0d33e9c8dafec5242235f0c95c3d3d
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/ebcfc2636c039ce113df9bd4fa1f4a0e9e0d33e9c8dafec5242235f0c95c3d3d.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 (ebcfc2636c039ce113df9bd4fa1f4a0e9e0d33e9c8dafec5242235f0c95c3d3d, sv-benchmarks/c/seq-mthreaded/pals_floodmax.4_false-unreach-call.1.ufo.BOUNDED-8.pals_true-termination.c).
Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_floodmax.4_false-unreach-call.1.ufo.BOUNDED-8.pals_true-termination.c, ebcfc2636c039ce113df9bd4fa1f4a0e9e0d33e9c8dafec5242235f0c95c3d3d
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/ebcfc2636c039ce113df9bd4fa1f4a0e9e0d33e9c8dafec5242235f0c95c3d3d.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 (ebcfc2636c039ce113df9bd4fa1f4a0e9e0d33e9c8dafec5242235f0c95c3d3d, sv-benchmarks/c/seq-mthreaded/pals_floodmax.4_false-unreach-call.1.ufo.BOUNDED-8.pals_true-termination.c).
Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_floodmax.4_false-unreach-call.1.ufo.BOUNDED-8.pals_true-termination.c, ebcfc2636c039ce113df9bd4fa1f4a0e9e0d33e9c8dafec5242235f0c95c3d3d
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/ebcfc2636c039ce113df9bd4fa1f4a0e9e0d33e9c8dafec5242235f0c95c3d3d.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 (ebcfc2636c039ce113df9bd4fa1f4a0e9e0d33e9c8dafec5242235f0c95c3d3d, sv-benchmarks/c/seq-mthreaded/pals_floodmax.4_false-unreach-call.1.ufo.BOUNDED-8.pals_true-termination.c).
Found 10 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_floodmax.4_false-unreach-call.1.ufo.BOUNDED-8.pals_true-termination.c, ebcfc2636c039ce113df9bd4fa1f4a0e9e0d33e9c8dafec5242235f0c95c3d3d
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/ebcfc2636c039ce113df9bd4fa1f4a0e9e0d33e9c8dafec5242235f0c95c3d3d.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
71166cb |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
287 |
2019-12-11T21:42:58+01:00 |
2aacadd |
3c26c89 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
315 |
2019-12-11T20:44:29+01:00 |
ed35c00 |
5643a70 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
315 |
2019-12-08T01:51:18+01:00 |
b4dec37 |
1d02d48 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
316 |
2019-12-03T08:00:48+01:00 |
f67b4dc |
f67b4dc |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / svcomp20 |
322 |
2019-11-29T18:17:02+01:00 |
|
b4dec37 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.8 |
254 |
2019-12-07T20:31:06+01:00 |
|
2aacadd |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco |
281 |
2019-12-01T09:54:23+01:00 |
|
4403ed9 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
126 |
2019-12-11T20:54:56+01:00 |
6813c69 |
0cf01c3 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
126 |
2019-12-05T20:20:45+01:00 |
39249e8 |
7b780f1 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
126 |
2019-12-05T19:34:30+01:00 |
3f2bcb4 |
Available Results for the Program from Witness Store SV-COMP '19
Trying to find witnesses for program (ebcfc2636c039ce113df9bd4fa1f4a0e9e0d33e9c8dafec5242235f0c95c3d3d, sv-benchmarks/c/seq-mthreaded/pals_floodmax.4_false-unreach-call.1.ufo.BOUNDED-8.pals_true-termination.c).
Found 14 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_floodmax.4_false-unreach-call.1.ufo.BOUNDED-8.pals_true-termination.c, ebcfc2636c039ce113df9bd4fa1f4a0e9e0d33e9c8dafec5242235f0c95c3d3d
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/ebcfc2636c039ce113df9bd4fa1f4a0e9e0d33e9c8dafec5242235f0c95c3d3d.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
71fa46a |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
Symbiotic |
18 |
2018-12-08T04:52 CET (sv-comp) |
|
19226ce |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
SMACK 1.9.3 |
76 |
2018-12-08T04:58:21 |
|
4fd033a |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn b8d6131600+ |
283 |
2018-12-07T23:38:18+01:00 |
|
ed8a0da |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
315 |
2018-12-09T18:21:58+01:00 |
8df210c |
08887e7 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
287 |
2018-12-08T23:44:52+01:00 |
71fa46a |
30d48ed |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
287 |
2018-12-08T08:58:31+01:00 |
4fd033a |
34a2fb6 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
289 |
2018-12-08T05:05:10+01:00 |
515d8bc |
60731a6 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
289 |
2018-12-06T10:19:25+01:00 |
3bf1481 |
5e4e8a2 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
316 |
2018-12-06T09:48:08+01:00 |
ef85b91 |
ef85b91 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
322 |
2018-12-05T17:55:00+01:00 |
|
06d6517 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
126 |
2018-12-10T20:38:29+01:00 |
11b6d27 |
476930e |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
126 |
2018-12-08T22:11:26+01:00 |
19226ce |
fa51207 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
126 |
2018-12-06T09:43:06+01:00 |
2e369f7 |
2b732b9 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
126 |
2018-12-06T09:16:03+01:00 |
6e42d58 |
Available Results for the Program from Witness Store SV-COMP '18
Trying to find witnesses for program (ebcfc2636c039ce113df9bd4fa1f4a0e9e0d33e9c8dafec5242235f0c95c3d3d, sv-benchmarks/c/seq-mthreaded/pals_floodmax.4_false-unreach-call.1.ufo.BOUNDED-8.pals_true-termination.c).
Found 13 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_floodmax.4_false-unreach-call.1.ufo.BOUNDED-8.pals_true-termination.c, ebcfc2636c039ce113df9bd4fa1f4a0e9e0d33e9c8dafec5242235f0c95c3d3d
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/ebcfc2636c039ce113df9bd4fa1f4a0e9e0d33e9c8dafec5242235f0c95c3d3d.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
b687984 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
VeriAbs 1.3 |
243 |
Sat Dec 2 23:47:33 2017 |
|
bef3497 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
Symbiotic |
16 |
2017-12-01T23:36 CET (sv-comp) |
|
b17d6b9 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
ESBMC 4.6.0 kind |
32 |
2017-12-01T19:45:44.306359 |
|
fd2289b |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
ESBMC 4.6.0 incr |
35 |
2017-12-01T19:22:19.268648 |
|
96446cf |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
ESBMC 3.1 |
94 |
2017-12-01T20:35 CET (sv-comp) |
|
973057d |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
ESBMC 3.1 |
99 |
2017-11-30T16:17 CET (sv-comp) |
|
db098dd |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.6.1-svn 26773 |
307 |
2017-11-30T12:27:33+01:00 |
|
5d610e0 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CBMC |
247 |
2017-11-30T11:42 CET (sv-comp) |
|
211eeb4 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
2LS |
199 |
2017-11-30T18:04 CET (sv-comp) |
|
7acd1ff |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
ESBMC 4.6.0 |
3 |
2017-12-02T23:22:06.622502 |
|
4cbad51 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
ESBMC 4.6.0 |
3 |
2017-12-02T14:19:45.496819 |
|
9639716 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
CBMC |
609 |
2017-12-01T17:47 CET (sv-comp) |
|
00a53ce |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
2LS |
267 |
2017-12-01T15:01 CET (sv-comp) |
|
Available Results for the Program from Witness Store SV-COMP '17
Trying to find witnesses for program (ebcfc2636c039ce113df9bd4fa1f4a0e9e0d33e9c8dafec5242235f0c95c3d3d, sv-benchmarks/c/seq-mthreaded/pals_floodmax.4_false-unreach-call.1.ufo.BOUNDED-8.pals_true-termination.c).
Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_floodmax.4_false-unreach-call.1.ufo.BOUNDED-8.pals_true-termination.c, ebcfc2636c039ce113df9bd4fa1f4a0e9e0d33e9c8dafec5242235f0c95c3d3d
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/ebcfc2636c039ce113df9bd4fa1f4a0e9e0d33e9c8dafec5242235f0c95c3d3d.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |