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.5_false-unreach-call.3.ufo.BOUNDED-10.pals_true-termination.c |
programSHA |
c69e3fc1b5633879ff1dd15ac986efcb8c1de7f43b8e9b2c3b89851992ed3b1d |
witnessName |
results-verified/esbmc-kind.2018-12-06_1103.logfiles/sv-comp19_prop-reachsafety.pals_floodmax.5_false-unreach-call.3.ufo.BOUNDED-10.pals_true-termination.c.files/witness.graphml |
witnessSHA |
1cf4d9526dad7ece23c5a6f6036df3e6940ca5b074e277b380b625bbc056b18f |
Information about the Witness from Competition Database
from https://sv-comp.sosy-lab.org/2019/results/witnessInfoByHash/1cf4d9526dad7ece23c5a6f6036df3e6940ca5b074e277b380b625bbc056b18f.json
Key |
Value |
architecture |
32bit |
creationtime |
2018-12-07T03:03:10.345941 |
producer |
ESBMC 6.0.0 kind |
programfile |
../../sv-benchmarks/c/seq-mthreaded/pals_floodmax.5_false-unreach-call.3.ufo.BOUNDED-10.pals_true-termination.c |
programhash |
474d2340f9eff2b5dd032a957f1601ae4ec7022b |
sourcecodelang |
C |
specification |
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file |
witnessFileByHash/1cf4d9526dad7ece23c5a6f6036df3e6940ca5b074e277b380b625bbc056b18f.graphml |
witness-sha256 |
1cf4d9526dad7ece23c5a6f6036df3e6940ca5b074e277b380b625bbc056b18f |
witness-size |
102735 |
witness-type |
violation_witness |
Available Results for the Program from Witness Store SV-COMP '24
Trying to find witnesses for program (c69e3fc1b5633879ff1dd15ac986efcb8c1de7f43b8e9b2c3b89851992ed3b1d, sv-benchmarks/c/seq-mthreaded/pals_floodmax.5_false-unreach-call.3.ufo.BOUNDED-10.pals_true-termination.c).
Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_floodmax.5_false-unreach-call.3.ufo.BOUNDED-10.pals_true-termination.c, c69e3fc1b5633879ff1dd15ac986efcb8c1de7f43b8e9b2c3b89851992ed3b1d
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/c69e3fc1b5633879ff1dd15ac986efcb8c1de7f43b8e9b2c3b89851992ed3b1d.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 (c69e3fc1b5633879ff1dd15ac986efcb8c1de7f43b8e9b2c3b89851992ed3b1d, sv-benchmarks/c/seq-mthreaded/pals_floodmax.5_false-unreach-call.3.ufo.BOUNDED-10.pals_true-termination.c).
Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_floodmax.5_false-unreach-call.3.ufo.BOUNDED-10.pals_true-termination.c, c69e3fc1b5633879ff1dd15ac986efcb8c1de7f43b8e9b2c3b89851992ed3b1d
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/c69e3fc1b5633879ff1dd15ac986efcb8c1de7f43b8e9b2c3b89851992ed3b1d.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 (c69e3fc1b5633879ff1dd15ac986efcb8c1de7f43b8e9b2c3b89851992ed3b1d, sv-benchmarks/c/seq-mthreaded/pals_floodmax.5_false-unreach-call.3.ufo.BOUNDED-10.pals_true-termination.c).
Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_floodmax.5_false-unreach-call.3.ufo.BOUNDED-10.pals_true-termination.c, c69e3fc1b5633879ff1dd15ac986efcb8c1de7f43b8e9b2c3b89851992ed3b1d
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/c69e3fc1b5633879ff1dd15ac986efcb8c1de7f43b8e9b2c3b89851992ed3b1d.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 (c69e3fc1b5633879ff1dd15ac986efcb8c1de7f43b8e9b2c3b89851992ed3b1d, sv-benchmarks/c/seq-mthreaded/pals_floodmax.5_false-unreach-call.3.ufo.BOUNDED-10.pals_true-termination.c).
Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_floodmax.5_false-unreach-call.3.ufo.BOUNDED-10.pals_true-termination.c, c69e3fc1b5633879ff1dd15ac986efcb8c1de7f43b8e9b2c3b89851992ed3b1d
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/c69e3fc1b5633879ff1dd15ac986efcb8c1de7f43b8e9b2c3b89851992ed3b1d.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 (c69e3fc1b5633879ff1dd15ac986efcb8c1de7f43b8e9b2c3b89851992ed3b1d, sv-benchmarks/c/seq-mthreaded/pals_floodmax.5_false-unreach-call.3.ufo.BOUNDED-10.pals_true-termination.c).
Found 8 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_floodmax.5_false-unreach-call.3.ufo.BOUNDED-10.pals_true-termination.c, c69e3fc1b5633879ff1dd15ac986efcb8c1de7f43b8e9b2c3b89851992ed3b1d
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/c69e3fc1b5633879ff1dd15ac986efcb8c1de7f43b8e9b2c3b89851992ed3b1d.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
48037d5 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
603 |
2019-12-11T21:57:43+01:00 |
150173d |
2d010db |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
660 |
2019-12-11T20:44:46+01:00 |
13eab74 |
4ddde60 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
614 |
2019-12-03T08:01:19+01:00 |
9d85f83 |
9d85f83 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / svcomp20 |
641 |
2019-11-29T19:34:03+01:00 |
|
150173d |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco |
604 |
2019-12-01T09:06:58+01:00 |
|
0f1c914 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
316 |
2019-12-11T20:54:25+01:00 |
a46b685 |
3d9b963 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
316 |
2019-12-08T01:51:39+01:00 |
202cae0 |
0b811d4 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
316 |
2019-12-05T20:20:48+01:00 |
fa0602e |
Available Results for the Program from Witness Store SV-COMP '19
Trying to find witnesses for program (c69e3fc1b5633879ff1dd15ac986efcb8c1de7f43b8e9b2c3b89851992ed3b1d, sv-benchmarks/c/seq-mthreaded/pals_floodmax.5_false-unreach-call.3.ufo.BOUNDED-10.pals_true-termination.c).
Found 13 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_floodmax.5_false-unreach-call.3.ufo.BOUNDED-10.pals_true-termination.c, c69e3fc1b5633879ff1dd15ac986efcb8c1de7f43b8e9b2c3b89851992ed3b1d
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/c69e3fc1b5633879ff1dd15ac986efcb8c1de7f43b8e9b2c3b89851992ed3b1d.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
357a654 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
Symbiotic |
24 |
2018-12-08T13:21 CET (sv-comp) |
|
5166d86 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
SMACK 1.9.3 |
181 |
2018-12-08T00:49:01 |
|
4171687 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn b8d6131600+ |
607 |
2018-12-07T05:19:41+01:00 |
|
a71fa2a |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
660 |
2018-12-09T18:20:10+01:00 |
3dfbfd7 |
82d3579 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
615 |
2018-12-08T23:42:18+01:00 |
357a654 |
61a7ace |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
603 |
2018-12-08T09:04:46+01:00 |
4171687 |
0b00089 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
614 |
2018-12-06T09:49:02+01:00 |
06e22e2 |
06e22e2 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
641 |
2018-12-05T11:09:23+01:00 |
|
0b1e1d5 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
316 |
2018-12-10T20:36:09+01:00 |
84d6ee8 |
24f22a7 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
316 |
2018-12-08T22:11:11+01:00 |
5166d86 |
7b08db8 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
316 |
2018-12-08T04:57:05+01:00 |
1cf4d95 |
c61f7fa |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
316 |
2018-12-06T10:12:37+01:00 |
8374538 |
1487e81 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
316 |
2018-12-06T09:20:24+01:00 |
c99d140 |
Available Results for the Program from Witness Store SV-COMP '18
Trying to find witnesses for program (c69e3fc1b5633879ff1dd15ac986efcb8c1de7f43b8e9b2c3b89851992ed3b1d, sv-benchmarks/c/seq-mthreaded/pals_floodmax.5_false-unreach-call.3.ufo.BOUNDED-10.pals_true-termination.c).
Found 12 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_floodmax.5_false-unreach-call.3.ufo.BOUNDED-10.pals_true-termination.c, c69e3fc1b5633879ff1dd15ac986efcb8c1de7f43b8e9b2c3b89851992ed3b1d
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/c69e3fc1b5633879ff1dd15ac986efcb8c1de7f43b8e9b2c3b89851992ed3b1d.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
a1aa455 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
VeriAbs 1.3 |
471 |
Sun Dec 3 02:31:09 2017 |
|
229aef8 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
Symbiotic |
22 |
2017-12-02T13:47 CET (sv-comp) |
|
c6adf07 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
ESBMC 4.6.0 kind |
99 |
2017-12-02T05:22:20.872001 |
|
fa55c1a |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
ESBMC 4.6.0 incr |
103 |
2017-12-01T19:50:03.145924 |
|
f172d1e |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
ESBMC 3.1 |
186 |
2017-12-01T20:19 CET (sv-comp) |
|
ff9ca42 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
ESBMC 3.1 |
186 |
2017-11-30T20:29 CET (sv-comp) |
|
122c050 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.6.1-svn 26773 |
609 |
2017-11-30T13:22:09+01:00 |
|
4d6d281 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CBMC |
491 |
2017-11-30T17:14 CET (sv-comp) |
|
b3ffd6a |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
ESBMC 4.6.0 |
3 |
2017-12-02T19:55:34.184560 |
|
cf8bfa0 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
ESBMC 4.6.0 |
3 |
2017-12-02T08:57:00.247703 |
|
2b41c8a |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
CBMC |
1246 |
2017-12-01T17:59 CET (sv-comp) |
|
e5e23ab |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
2LS |
628 |
2017-12-01T12:11 CET (sv-comp) |
|
Available Results for the Program from Witness Store SV-COMP '17
Trying to find witnesses for program (c69e3fc1b5633879ff1dd15ac986efcb8c1de7f43b8e9b2c3b89851992ed3b1d, sv-benchmarks/c/seq-mthreaded/pals_floodmax.5_false-unreach-call.3.ufo.BOUNDED-10.pals_true-termination.c).
Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_floodmax.5_false-unreach-call.3.ufo.BOUNDED-10.pals_true-termination.c, c69e3fc1b5633879ff1dd15ac986efcb8c1de7f43b8e9b2c3b89851992ed3b1d
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/c69e3fc1b5633879ff1dd15ac986efcb8c1de7f43b8e9b2c3b89851992ed3b1d.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |