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.2.ufo.UNBOUNDED.pals.c |
programSHA |
baedcb464f59e807c87f6d0d22b618263dc84c6324f973d5baf6bf46a2c7c253 |
witnessName |
results-verified/symbiotic.2017-12-01_2241.logfiles/sv-comp18.pals_floodmax.4_false-unreach-call.2.ufo.UNBOUNDED.pals.c.files/witness.graphml |
witnessSHA |
456f9a709a5c2b1a9e90d3d20c1052dfbae5818349a605fdbf481a19e210b456 |
Information about the Witness from Competition Database
from https://sv-comp.sosy-lab.org/2018/results/witnessInfoByHash/456f9a709a5c2b1a9e90d3d20c1052dfbae5818349a605fdbf481a19e210b456.json
Key |
Value |
architecture |
32bit |
creationtime |
2017-12-02T14:36 CET (sv-comp) |
producer |
Symbiotic |
program-sha256 |
baedcb464f59e807c87f6d0d22b618263dc84c6324f973d5baf6bf46a2c7c253 |
programfile |
/tmp/vcloud-vcloud-master/worker/working_dir_5eea5d12-a72a-46d4-93cf-48ac51a771f9/sv-benchmarks/c/seq-mthreaded/pals_floodmax.4_false-unreach-call.2.ufo.UNBOUNDED.pals.c |
programhash |
6ae2edd8acc18e48c9d76f7bf96d8f6a9040b232 |
sourcecodelang |
C |
specification |
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file |
witnessFileByHash/456f9a709a5c2b1a9e90d3d20c1052dfbae5818349a605fdbf481a19e210b456.graphml |
witness-sha256 |
456f9a709a5c2b1a9e90d3d20c1052dfbae5818349a605fdbf481a19e210b456 |
witness-size |
15448 |
witness-type |
violation_witness |
Available Results for the Program from Witness Store SV-COMP '24
Trying to find witnesses for program (baedcb464f59e807c87f6d0d22b618263dc84c6324f973d5baf6bf46a2c7c253, sv-benchmarks/c/seq-mthreaded/pals_floodmax.4_false-unreach-call.2.ufo.UNBOUNDED.pals.c).
Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_floodmax.4_false-unreach-call.2.ufo.UNBOUNDED.pals.c, baedcb464f59e807c87f6d0d22b618263dc84c6324f973d5baf6bf46a2c7c253
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/baedcb464f59e807c87f6d0d22b618263dc84c6324f973d5baf6bf46a2c7c253.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 (baedcb464f59e807c87f6d0d22b618263dc84c6324f973d5baf6bf46a2c7c253, sv-benchmarks/c/seq-mthreaded/pals_floodmax.4_false-unreach-call.2.ufo.UNBOUNDED.pals.c).
Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_floodmax.4_false-unreach-call.2.ufo.UNBOUNDED.pals.c, baedcb464f59e807c87f6d0d22b618263dc84c6324f973d5baf6bf46a2c7c253
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/baedcb464f59e807c87f6d0d22b618263dc84c6324f973d5baf6bf46a2c7c253.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 (baedcb464f59e807c87f6d0d22b618263dc84c6324f973d5baf6bf46a2c7c253, sv-benchmarks/c/seq-mthreaded/pals_floodmax.4_false-unreach-call.2.ufo.UNBOUNDED.pals.c).
Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_floodmax.4_false-unreach-call.2.ufo.UNBOUNDED.pals.c, baedcb464f59e807c87f6d0d22b618263dc84c6324f973d5baf6bf46a2c7c253
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/baedcb464f59e807c87f6d0d22b618263dc84c6324f973d5baf6bf46a2c7c253.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 (baedcb464f59e807c87f6d0d22b618263dc84c6324f973d5baf6bf46a2c7c253, sv-benchmarks/c/seq-mthreaded/pals_floodmax.4_false-unreach-call.2.ufo.UNBOUNDED.pals.c).
Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_floodmax.4_false-unreach-call.2.ufo.UNBOUNDED.pals.c, baedcb464f59e807c87f6d0d22b618263dc84c6324f973d5baf6bf46a2c7c253
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/baedcb464f59e807c87f6d0d22b618263dc84c6324f973d5baf6bf46a2c7c253.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 (baedcb464f59e807c87f6d0d22b618263dc84c6324f973d5baf6bf46a2c7c253, sv-benchmarks/c/seq-mthreaded/pals_floodmax.4_false-unreach-call.2.ufo.UNBOUNDED.pals.c).
Found 10 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_floodmax.4_false-unreach-call.2.ufo.UNBOUNDED.pals.c, baedcb464f59e807c87f6d0d22b618263dc84c6324f973d5baf6bf46a2c7c253
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/baedcb464f59e807c87f6d0d22b618263dc84c6324f973d5baf6bf46a2c7c253.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
b3dfb51 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
252 |
2019-12-11T21:59:22+01:00 |
636f743 |
6222d38 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
257 |
2019-12-11T20:44:53+01:00 |
1a2f7e8 |
324cb1b |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
244 |
2019-12-08T01:51:24+01:00 |
c80e578 |
300cfa4 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
243 |
2019-12-03T08:10:40+01:00 |
73a3740 |
73a3740 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / svcomp20 |
254 |
2019-11-29T16:31:37+01:00 |
|
c80e578 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.8 |
198 |
2019-12-07T22:24:22+01:00 |
|
636f743 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco |
253 |
2019-12-01T02:09:11+01:00 |
|
5edaebf |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
133 |
2019-12-11T20:54:24+01:00 |
b9f3bb5 |
0fa460b |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
133 |
2019-12-05T20:21:40+01:00 |
79f7742 |
2f3b965 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
133 |
2019-12-05T19:34:17+01:00 |
5f6f65a |
Available Results for the Program from Witness Store SV-COMP '19
Trying to find witnesses for program (baedcb464f59e807c87f6d0d22b618263dc84c6324f973d5baf6bf46a2c7c253, sv-benchmarks/c/seq-mthreaded/pals_floodmax.4_false-unreach-call.2.ufo.UNBOUNDED.pals.c).
Found 14 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_floodmax.4_false-unreach-call.2.ufo.UNBOUNDED.pals.c, baedcb464f59e807c87f6d0d22b618263dc84c6324f973d5baf6bf46a2c7c253
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/baedcb464f59e807c87f6d0d22b618263dc84c6324f973d5baf6bf46a2c7c253.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
f788b4e |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
Symbiotic |
17 |
2018-12-08T01:09 CET (sv-comp) |
|
bebb772 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
SMACK 1.9.3 |
70 |
2018-12-08T05:04:33 |
|
d4c49d1 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn b8d6131600+ |
253 |
2018-12-07T05:28:03+01:00 |
|
ead4b64 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
257 |
2018-12-09T18:19:54+01:00 |
4358d8d |
c2df8b3 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
241 |
2018-12-08T23:43:01+01:00 |
f788b4e |
959ca51 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
252 |
2018-12-08T07:49:55+01:00 |
d4c49d1 |
144184f |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
243 |
2018-12-06T09:48:49+01:00 |
a3ac8fc |
a3ac8fc |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
254 |
2018-12-06T03:36:42+01:00 |
|
afe80c6 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
134 |
2018-12-10T20:35:48+01:00 |
531cd3c |
24e528f |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
133 |
2018-12-08T22:10:11+01:00 |
bebb772 |
15a13b3 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
134 |
2018-12-08T05:05:58+01:00 |
60edfc8 |
a0659a0 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
134 |
2018-12-06T10:18:55+01:00 |
d53c006 |
77bf4e1 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
134 |
2018-12-06T09:42:27+01:00 |
218f76d |
634da51 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
133 |
2018-12-06T09:19:51+01:00 |
c7194aa |
Available Results for the Program from Witness Store SV-COMP '18
Trying to find witnesses for program (baedcb464f59e807c87f6d0d22b618263dc84c6324f973d5baf6bf46a2c7c253, sv-benchmarks/c/seq-mthreaded/pals_floodmax.4_false-unreach-call.2.ufo.UNBOUNDED.pals.c).
Found 8 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_floodmax.4_false-unreach-call.2.ufo.UNBOUNDED.pals.c, baedcb464f59e807c87f6d0d22b618263dc84c6324f973d5baf6bf46a2c7c253
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/baedcb464f59e807c87f6d0d22b618263dc84c6324f973d5baf6bf46a2c7c253.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
4170d90 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
VeriAbs 1.3 |
182 |
Sat Dec 2 18:35:31 2017 |
|
456f9a7 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
Symbiotic |
15 |
2017-12-02T14:36 CET (sv-comp) |
|
450edd9 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
ESBMC 4.6.0 kind |
36 |
2017-12-01T14:51:22.517248 |
|
e694958 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
ESBMC 4.6.0 incr |
38 |
2017-12-01T14:44:32.012263 |
|
3a8a93d |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
ESBMC 3.1 |
77 |
2017-12-01T07:30 CET (sv-comp) |
|
16af03a |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.6.1-svn 26773 |
241 |
2017-11-30T16:35:27+01:00 |
|
919b91d |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CBMC |
197 |
2017-12-01T00:28 CET (sv-comp) |
|
2d3b896 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
2LS |
143 |
2017-11-30T15:49 CET (sv-comp) |
|
Available Results for the Program from Witness Store SV-COMP '17
Trying to find witnesses for program (baedcb464f59e807c87f6d0d22b618263dc84c6324f973d5baf6bf46a2c7c253, sv-benchmarks/c/seq-mthreaded/pals_floodmax.4_false-unreach-call.2.ufo.UNBOUNDED.pals.c).
Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_floodmax.4_false-unreach-call.2.ufo.UNBOUNDED.pals.c, baedcb464f59e807c87f6d0d22b618263dc84c6324f973d5baf6bf46a2c7c253
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/baedcb464f59e807c87f6d0d22b618263dc84c6324f973d5baf6bf46a2c7c253.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |