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.4.ufo.UNBOUNDED.pals.c |
programSHA |
db370bff001c9f51ec91c7eb057441bb38b63191d06e394fe2da76003fd9bfe7 |
witnessName |
results-verified/veriabs.2018-12-10_1650.logfiles/sv-comp19_prop-reachsafety.pals_floodmax.5_false-unreach-call.4.ufo.UNBOUNDED.pals.c.files/witness.graphml |
witnessSHA |
e51706c47fdadfde3b2b111a3b1a523d3b7dae516549c226c417c2a2a289e17e |
Information about the Witness from Competition Database
from https://sv-comp.sosy-lab.org/2019/results/witnessInfoByHash/e51706c47fdadfde3b2b111a3b1a523d3b7dae516549c226c417c2a2a289e17e.json
Key |
Value |
architecture |
32bit |
creationtime |
Mon Dec 10 16:11:33 2018 |
producer |
VeriAbs 1.3 |
programfile |
/home/benchexec/ar_abs_temp/pals_floodmax_5_false_unreach_call_4_ufo_UNBOUNDED_pals_c.c |
programhash |
db0af4b87f56d902838b971a4e02e33e56e01163 |
sourcecodelang |
C |
specification |
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file |
witnessFileByHash/e51706c47fdadfde3b2b111a3b1a523d3b7dae516549c226c417c2a2a289e17e.graphml |
witness-sha256 |
e51706c47fdadfde3b2b111a3b1a523d3b7dae516549c226c417c2a2a289e17e |
witness-size |
437604 |
witness-type |
violation_witness |
Available Results for the Program from Witness Store SV-COMP '24
Trying to find witnesses for program (db370bff001c9f51ec91c7eb057441bb38b63191d06e394fe2da76003fd9bfe7, sv-benchmarks/c/seq-mthreaded/pals_floodmax.5_false-unreach-call.4.ufo.UNBOUNDED.pals.c).
Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_floodmax.5_false-unreach-call.4.ufo.UNBOUNDED.pals.c, db370bff001c9f51ec91c7eb057441bb38b63191d06e394fe2da76003fd9bfe7
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/db370bff001c9f51ec91c7eb057441bb38b63191d06e394fe2da76003fd9bfe7.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 (db370bff001c9f51ec91c7eb057441bb38b63191d06e394fe2da76003fd9bfe7, sv-benchmarks/c/seq-mthreaded/pals_floodmax.5_false-unreach-call.4.ufo.UNBOUNDED.pals.c).
Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_floodmax.5_false-unreach-call.4.ufo.UNBOUNDED.pals.c, db370bff001c9f51ec91c7eb057441bb38b63191d06e394fe2da76003fd9bfe7
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/db370bff001c9f51ec91c7eb057441bb38b63191d06e394fe2da76003fd9bfe7.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 (db370bff001c9f51ec91c7eb057441bb38b63191d06e394fe2da76003fd9bfe7, sv-benchmarks/c/seq-mthreaded/pals_floodmax.5_false-unreach-call.4.ufo.UNBOUNDED.pals.c).
Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_floodmax.5_false-unreach-call.4.ufo.UNBOUNDED.pals.c, db370bff001c9f51ec91c7eb057441bb38b63191d06e394fe2da76003fd9bfe7
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/db370bff001c9f51ec91c7eb057441bb38b63191d06e394fe2da76003fd9bfe7.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 (db370bff001c9f51ec91c7eb057441bb38b63191d06e394fe2da76003fd9bfe7, sv-benchmarks/c/seq-mthreaded/pals_floodmax.5_false-unreach-call.4.ufo.UNBOUNDED.pals.c).
Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_floodmax.5_false-unreach-call.4.ufo.UNBOUNDED.pals.c, db370bff001c9f51ec91c7eb057441bb38b63191d06e394fe2da76003fd9bfe7
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/db370bff001c9f51ec91c7eb057441bb38b63191d06e394fe2da76003fd9bfe7.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 (db370bff001c9f51ec91c7eb057441bb38b63191d06e394fe2da76003fd9bfe7, sv-benchmarks/c/seq-mthreaded/pals_floodmax.5_false-unreach-call.4.ufo.UNBOUNDED.pals.c).
Found 9 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_floodmax.5_false-unreach-call.4.ufo.UNBOUNDED.pals.c, db370bff001c9f51ec91c7eb057441bb38b63191d06e394fe2da76003fd9bfe7
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/db370bff001c9f51ec91c7eb057441bb38b63191d06e394fe2da76003fd9bfe7.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
98302fe |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
600 |
2019-12-11T22:00:33+01:00 |
7c4b46c |
e8edeec |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
613 |
2019-12-11T20:44:38+01:00 |
51e6c30 |
3fb41ff |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
600 |
2019-12-03T08:02:39+01:00 |
b558052 |
b558052 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / svcomp20 |
611 |
2019-11-29T20:17:01+01:00 |
|
7c4b46c |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco |
601 |
2019-12-01T00:01:12+01:00 |
|
8a96b4c |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
318 |
2019-12-11T20:55:03+01:00 |
d2156f5 |
6878bbc |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
318 |
2019-12-08T01:51:25+01:00 |
51efea5 |
af27623 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
318 |
2019-12-05T20:20:17+01:00 |
8e357d8 |
f185418 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
318 |
2019-12-05T19:34:39+01:00 |
dca51e0 |
Available Results for the Program from Witness Store SV-COMP '19
Trying to find witnesses for program (db370bff001c9f51ec91c7eb057441bb38b63191d06e394fe2da76003fd9bfe7, sv-benchmarks/c/seq-mthreaded/pals_floodmax.5_false-unreach-call.4.ufo.UNBOUNDED.pals.c).
Found 12 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_floodmax.5_false-unreach-call.4.ufo.UNBOUNDED.pals.c, db370bff001c9f51ec91c7eb057441bb38b63191d06e394fe2da76003fd9bfe7
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/db370bff001c9f51ec91c7eb057441bb38b63191d06e394fe2da76003fd9bfe7.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
186e790 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
SMACK 1.9.3 |
169 |
2018-12-08T07:13:13 |
|
85ea9bb |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn b8d6131600+ |
605 |
2018-12-07T19:06:35+01:00 |
|
e7929b4 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
616 |
2018-12-09T18:21:32+01:00 |
0b6c571 |
515a82e |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
600 |
2018-12-08T08:39:09+01:00 |
85ea9bb |
874045c |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
600 |
2018-12-06T09:48:49+01:00 |
3d7768e |
3d7768e |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
611 |
2018-12-05T22:46:00+01:00 |
|
88bb107 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
318 |
2018-12-10T20:36:16+01:00 |
e51706c |
737597d |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
318 |
2018-12-08T22:10:21+01:00 |
186e790 |
65f62e3 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
318 |
2018-12-08T05:02:15+01:00 |
05b907f |
92375ab |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
318 |
2018-12-06T10:12:26+01:00 |
bd4ba92 |
db6a2da |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
318 |
2018-12-06T09:40:42+01:00 |
968ebb1 |
abd4374 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
318 |
2018-12-06T09:16:47+01:00 |
64732a7 |
Available Results for the Program from Witness Store SV-COMP '18
Trying to find witnesses for program (db370bff001c9f51ec91c7eb057441bb38b63191d06e394fe2da76003fd9bfe7, sv-benchmarks/c/seq-mthreaded/pals_floodmax.5_false-unreach-call.4.ufo.UNBOUNDED.pals.c).
Found 7 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_floodmax.5_false-unreach-call.4.ufo.UNBOUNDED.pals.c, db370bff001c9f51ec91c7eb057441bb38b63191d06e394fe2da76003fd9bfe7
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/db370bff001c9f51ec91c7eb057441bb38b63191d06e394fe2da76003fd9bfe7.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
874ab09 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
VeriAbs 1.3 |
451 |
Sat Dec 2 18:24:00 2017 |
|
7a738f7 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
ESBMC 4.6.0 kind |
82 |
2017-12-02T04:44:46.322830 |
|
dd9ee54 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
ESBMC 4.6.0 incr |
87 |
2017-12-01T17:31:31.676889 |
|
391b28e |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
ESBMC 3.1 |
177 |
2017-12-01T07:03 CET (sv-comp) |
|
e3aacc9 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.6.1-svn 26773 |
576 |
2017-11-30T12:52:29+01:00 |
|
5090b76 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CBMC |
464 |
2017-12-01T00:04 CET (sv-comp) |
|
8d038c5 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
2LS |
377 |
2017-11-30T18:43 CET (sv-comp) |
|
Available Results for the Program from Witness Store SV-COMP '17
Trying to find witnesses for program (db370bff001c9f51ec91c7eb057441bb38b63191d06e394fe2da76003fd9bfe7, sv-benchmarks/c/seq-mthreaded/pals_floodmax.5_false-unreach-call.4.ufo.UNBOUNDED.pals.c).
Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_floodmax.5_false-unreach-call.4.ufo.UNBOUNDED.pals.c, db370bff001c9f51ec91c7eb057441bb38b63191d06e394fe2da76003fd9bfe7
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/db370bff001c9f51ec91c7eb057441bb38b63191d06e394fe2da76003fd9bfe7.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |