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.3.ufo.UNBOUNDED.pals.c |
programSHA |
a6deb70f34ef1eb656156b2c82e446dc52cd556c844bcda83f636233dab208db |
witnessName |
results-verified/esbmc-kind.2018-12-06_1103.logfiles/sv-comp19_prop-reachsafety.pals_floodmax.4_false-unreach-call.3.ufo.UNBOUNDED.pals.c.files/witness.graphml |
witnessSHA |
1081650e98ef7fc2160585d62ca1f3f22edac1ab963718ef34ebaddc0b32fb28 |
Information about the Witness from Competition Database
from https://sv-comp.sosy-lab.org/2019/results/witnessInfoByHash/1081650e98ef7fc2160585d62ca1f3f22edac1ab963718ef34ebaddc0b32fb28.json
Key |
Value |
architecture |
32bit |
creationtime |
2018-12-07T08:28:19.658269 |
producer |
ESBMC 6.0.0 kind |
programfile |
../../sv-benchmarks/c/seq-mthreaded/pals_floodmax.4_false-unreach-call.3.ufo.UNBOUNDED.pals.c |
programhash |
66be30329ce5a875d8d31bd46efe6f26bf4e8225 |
sourcecodelang |
C |
specification |
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file |
witnessFileByHash/1081650e98ef7fc2160585d62ca1f3f22edac1ab963718ef34ebaddc0b32fb28.graphml |
witness-sha256 |
1081650e98ef7fc2160585d62ca1f3f22edac1ab963718ef34ebaddc0b32fb28 |
witness-size |
47531 |
witness-type |
violation_witness |
Available Results for the Program from Witness Store SV-COMP '24
Trying to find witnesses for program (a6deb70f34ef1eb656156b2c82e446dc52cd556c844bcda83f636233dab208db, sv-benchmarks/c/seq-mthreaded/pals_floodmax.4_false-unreach-call.3.ufo.UNBOUNDED.pals.c).
Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_floodmax.4_false-unreach-call.3.ufo.UNBOUNDED.pals.c, a6deb70f34ef1eb656156b2c82e446dc52cd556c844bcda83f636233dab208db
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/a6deb70f34ef1eb656156b2c82e446dc52cd556c844bcda83f636233dab208db.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 (a6deb70f34ef1eb656156b2c82e446dc52cd556c844bcda83f636233dab208db, sv-benchmarks/c/seq-mthreaded/pals_floodmax.4_false-unreach-call.3.ufo.UNBOUNDED.pals.c).
Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_floodmax.4_false-unreach-call.3.ufo.UNBOUNDED.pals.c, a6deb70f34ef1eb656156b2c82e446dc52cd556c844bcda83f636233dab208db
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/a6deb70f34ef1eb656156b2c82e446dc52cd556c844bcda83f636233dab208db.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 (a6deb70f34ef1eb656156b2c82e446dc52cd556c844bcda83f636233dab208db, sv-benchmarks/c/seq-mthreaded/pals_floodmax.4_false-unreach-call.3.ufo.UNBOUNDED.pals.c).
Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_floodmax.4_false-unreach-call.3.ufo.UNBOUNDED.pals.c, a6deb70f34ef1eb656156b2c82e446dc52cd556c844bcda83f636233dab208db
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/a6deb70f34ef1eb656156b2c82e446dc52cd556c844bcda83f636233dab208db.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 (a6deb70f34ef1eb656156b2c82e446dc52cd556c844bcda83f636233dab208db, sv-benchmarks/c/seq-mthreaded/pals_floodmax.4_false-unreach-call.3.ufo.UNBOUNDED.pals.c).
Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_floodmax.4_false-unreach-call.3.ufo.UNBOUNDED.pals.c, a6deb70f34ef1eb656156b2c82e446dc52cd556c844bcda83f636233dab208db
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/a6deb70f34ef1eb656156b2c82e446dc52cd556c844bcda83f636233dab208db.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 (a6deb70f34ef1eb656156b2c82e446dc52cd556c844bcda83f636233dab208db, sv-benchmarks/c/seq-mthreaded/pals_floodmax.4_false-unreach-call.3.ufo.UNBOUNDED.pals.c).
Found 10 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_floodmax.4_false-unreach-call.3.ufo.UNBOUNDED.pals.c, a6deb70f34ef1eb656156b2c82e446dc52cd556c844bcda83f636233dab208db
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/a6deb70f34ef1eb656156b2c82e446dc52cd556c844bcda83f636233dab208db.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
e595020 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
323 |
2019-12-11T21:55:59+01:00 |
5cf1204 |
e0e17db |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
344 |
2019-12-11T20:44:31+01:00 |
b6f0235 |
f28e185 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
338 |
2019-12-08T01:51:44+01:00 |
8ef0e95 |
8a688d7 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
319 |
2019-12-03T08:09:08+01:00 |
a1aaf29 |
a1aaf29 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / svcomp20 |
332 |
2019-11-30T09:15:47+01:00 |
|
8ef0e95 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.8 |
269 |
2019-12-07T22:24:52+01:00 |
|
5cf1204 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco |
324 |
2019-12-01T18:24:53+01:00 |
|
55118d5 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
133 |
2019-12-11T20:54:38+01:00 |
fd2d344 |
6e2421a |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
133 |
2019-12-05T20:20:16+01:00 |
923a1ed |
e777833 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
133 |
2019-12-05T19:34:56+01:00 |
bd5c284 |
Available Results for the Program from Witness Store SV-COMP '19
Trying to find witnesses for program (a6deb70f34ef1eb656156b2c82e446dc52cd556c844bcda83f636233dab208db, sv-benchmarks/c/seq-mthreaded/pals_floodmax.4_false-unreach-call.3.ufo.UNBOUNDED.pals.c).
Found 14 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_floodmax.4_false-unreach-call.3.ufo.UNBOUNDED.pals.c, a6deb70f34ef1eb656156b2c82e446dc52cd556c844bcda83f636233dab208db
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/a6deb70f34ef1eb656156b2c82e446dc52cd556c844bcda83f636233dab208db.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
4778448 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
Symbiotic |
17 |
2018-12-08T06:45 CET (sv-comp) |
|
1c7a610 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
SMACK 1.9.3 |
89 |
2018-12-07T21:38:50 |
|
82d019b |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn b8d6131600+ |
326 |
2018-12-07T04:04:33+01:00 |
|
e1b2526 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
344 |
2018-12-09T18:21:57+01:00 |
c06a67e |
d92f391 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
320 |
2018-12-08T23:44:34+01:00 |
4778448 |
b7b3397 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
323 |
2018-12-08T08:41:04+01:00 |
82d019b |
4b6b67c |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
319 |
2018-12-06T09:48:13+01:00 |
c38579d |
c38579d |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
332 |
2018-12-05T22:59:15+01:00 |
|
c617d9d |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
134 |
2018-12-10T20:35:04+01:00 |
70f86eb |
21cd816 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
133 |
2018-12-08T22:10:08+01:00 |
1c7a610 |
0889ec8 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
134 |
2018-12-08T04:52:45+01:00 |
1081650 |
2ce0d6c |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
134 |
2018-12-06T10:16:16+01:00 |
9d0db2a |
5cb9c48 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
134 |
2018-12-06T09:42:54+01:00 |
3fc9aba |
3109407 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
133 |
2018-12-06T09:19:08+01:00 |
e55f58f |
Available Results for the Program from Witness Store SV-COMP '18
Trying to find witnesses for program (a6deb70f34ef1eb656156b2c82e446dc52cd556c844bcda83f636233dab208db, sv-benchmarks/c/seq-mthreaded/pals_floodmax.4_false-unreach-call.3.ufo.UNBOUNDED.pals.c).
Found 8 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_floodmax.4_false-unreach-call.3.ufo.UNBOUNDED.pals.c, a6deb70f34ef1eb656156b2c82e446dc52cd556c844bcda83f636233dab208db
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/a6deb70f34ef1eb656156b2c82e446dc52cd556c844bcda83f636233dab208db.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
3f51af9 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
VeriAbs 1.3 |
230 |
Sat Dec 2 22:10:51 2017 |
|
c4bf969 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
Symbiotic |
15 |
2017-12-02T07:48 CET (sv-comp) |
|
aceb350 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
ESBMC 4.6.0 kind |
45 |
2017-12-01T21:27:39.748912 |
|
ae0e8e1 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
ESBMC 4.6.0 incr |
48 |
2017-12-01T13:24:17.252180 |
|
aae7b93 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
ESBMC 3.1 |
96 |
2017-12-01T06:12 CET (sv-comp) |
|
f6e81ee |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.6.1-svn 26773 |
315 |
2017-11-30T11:27:32+01:00 |
|
c7de019 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CBMC |
248 |
2017-11-30T15:24 CET (sv-comp) |
|
7dd550d |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
2LS |
187 |
2017-11-30T16:33 CET (sv-comp) |
|
Available Results for the Program from Witness Store SV-COMP '17
Trying to find witnesses for program (a6deb70f34ef1eb656156b2c82e446dc52cd556c844bcda83f636233dab208db, sv-benchmarks/c/seq-mthreaded/pals_floodmax.4_false-unreach-call.3.ufo.UNBOUNDED.pals.c).
Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_floodmax.4_false-unreach-call.3.ufo.UNBOUNDED.pals.c, a6deb70f34ef1eb656156b2c82e446dc52cd556c844bcda83f636233dab208db
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/a6deb70f34ef1eb656156b2c82e446dc52cd556c844bcda83f636233dab208db.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |