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.BOUNDED-10.pals_true-termination.c |
programSHA |
a54c1d4dc961e3dcb9535534ea9396e952c503514c8f9921646b70acbbe35c1f |
witnessName |
results-verified/veriabs.2018-12-10_1650.logfiles/sv-comp19_prop-reachsafety.pals_floodmax.5_false-unreach-call.4.ufo.BOUNDED-10.pals_true-termination.c.files/witness.graphml |
witnessSHA |
6a2047f931188175b3843b11477f4000336c34908ab4b36b6bfd4700cefe5bfc |
Information about the Witness from Competition Database
from https://sv-comp.sosy-lab.org/2019/results/witnessInfoByHash/6a2047f931188175b3843b11477f4000336c34908ab4b36b6bfd4700cefe5bfc.json
Key |
Value |
architecture |
32bit |
creationtime |
Mon Dec 10 16:53:06 2018 |
producer |
VeriAbs 1.3 |
programfile |
/home/benchexec/ar_abs_temp/pals_floodmax_5_false_unreach_call_4_ufo_BOUNDED_10_pals_true_termination_c.c |
programhash |
727f24e8ef6f45fcd7845df4b7c9997bc6f388f6 |
sourcecodelang |
C |
specification |
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file |
witnessFileByHash/6a2047f931188175b3843b11477f4000336c34908ab4b36b6bfd4700cefe5bfc.graphml |
witness-sha256 |
6a2047f931188175b3843b11477f4000336c34908ab4b36b6bfd4700cefe5bfc |
witness-size |
462793 |
witness-type |
violation_witness |
Available Results for the Program from Witness Store SV-COMP '24
Trying to find witnesses for program (a54c1d4dc961e3dcb9535534ea9396e952c503514c8f9921646b70acbbe35c1f, sv-benchmarks/c/seq-mthreaded/pals_floodmax.5_false-unreach-call.4.ufo.BOUNDED-10.pals_true-termination.c).
Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_floodmax.5_false-unreach-call.4.ufo.BOUNDED-10.pals_true-termination.c, a54c1d4dc961e3dcb9535534ea9396e952c503514c8f9921646b70acbbe35c1f
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/a54c1d4dc961e3dcb9535534ea9396e952c503514c8f9921646b70acbbe35c1f.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 (a54c1d4dc961e3dcb9535534ea9396e952c503514c8f9921646b70acbbe35c1f, sv-benchmarks/c/seq-mthreaded/pals_floodmax.5_false-unreach-call.4.ufo.BOUNDED-10.pals_true-termination.c).
Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_floodmax.5_false-unreach-call.4.ufo.BOUNDED-10.pals_true-termination.c, a54c1d4dc961e3dcb9535534ea9396e952c503514c8f9921646b70acbbe35c1f
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/a54c1d4dc961e3dcb9535534ea9396e952c503514c8f9921646b70acbbe35c1f.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 (a54c1d4dc961e3dcb9535534ea9396e952c503514c8f9921646b70acbbe35c1f, sv-benchmarks/c/seq-mthreaded/pals_floodmax.5_false-unreach-call.4.ufo.BOUNDED-10.pals_true-termination.c).
Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_floodmax.5_false-unreach-call.4.ufo.BOUNDED-10.pals_true-termination.c, a54c1d4dc961e3dcb9535534ea9396e952c503514c8f9921646b70acbbe35c1f
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/a54c1d4dc961e3dcb9535534ea9396e952c503514c8f9921646b70acbbe35c1f.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 (a54c1d4dc961e3dcb9535534ea9396e952c503514c8f9921646b70acbbe35c1f, sv-benchmarks/c/seq-mthreaded/pals_floodmax.5_false-unreach-call.4.ufo.BOUNDED-10.pals_true-termination.c).
Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_floodmax.5_false-unreach-call.4.ufo.BOUNDED-10.pals_true-termination.c, a54c1d4dc961e3dcb9535534ea9396e952c503514c8f9921646b70acbbe35c1f
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/a54c1d4dc961e3dcb9535534ea9396e952c503514c8f9921646b70acbbe35c1f.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 (a54c1d4dc961e3dcb9535534ea9396e952c503514c8f9921646b70acbbe35c1f, sv-benchmarks/c/seq-mthreaded/pals_floodmax.5_false-unreach-call.4.ufo.BOUNDED-10.pals_true-termination.c).
Found 9 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_floodmax.5_false-unreach-call.4.ufo.BOUNDED-10.pals_true-termination.c, a54c1d4dc961e3dcb9535534ea9396e952c503514c8f9921646b70acbbe35c1f
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/a54c1d4dc961e3dcb9535534ea9396e952c503514c8f9921646b70acbbe35c1f.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
7850412 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
590 |
2019-12-11T21:49:47+01:00 |
1dcfcda |
0380f54 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
608 |
2019-12-11T20:44:45+01:00 |
f04591b |
3d5015e |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
590 |
2019-12-03T08:10:30+01:00 |
6c52c76 |
6c52c76 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / svcomp20 |
601 |
2019-11-29T14:34:02+01:00 |
|
1dcfcda |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco |
591 |
2019-12-01T18:10:38+01:00 |
|
b3db32f |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
316 |
2019-12-11T20:55:21+01:00 |
72cea12 |
759af64 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
316 |
2019-12-08T01:52:11+01:00 |
cc69d41 |
3e23665 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
316 |
2019-12-05T20:20:40+01:00 |
1a8fb60 |
0ed1377 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
316 |
2019-12-05T19:34:21+01:00 |
860a032 |
Available Results for the Program from Witness Store SV-COMP '19
Trying to find witnesses for program (a54c1d4dc961e3dcb9535534ea9396e952c503514c8f9921646b70acbbe35c1f, sv-benchmarks/c/seq-mthreaded/pals_floodmax.5_false-unreach-call.4.ufo.BOUNDED-10.pals_true-termination.c).
Found 12 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_floodmax.5_false-unreach-call.4.ufo.BOUNDED-10.pals_true-termination.c, a54c1d4dc961e3dcb9535534ea9396e952c503514c8f9921646b70acbbe35c1f
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/a54c1d4dc961e3dcb9535534ea9396e952c503514c8f9921646b70acbbe35c1f.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
fbc475e |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
SMACK 1.9.3 |
162 |
2018-12-08T09:48:45 |
|
368ce35 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn b8d6131600+ |
594 |
2018-12-07T09:05:57+01:00 |
|
a18d282 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
608 |
2018-12-09T18:21:05+01:00 |
76ea2f5 |
00540ae |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
590 |
2018-12-08T08:23:28+01:00 |
368ce35 |
3ee4f5b |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
590 |
2018-12-06T09:49:00+01:00 |
8324aff |
8324aff |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
601 |
2018-12-05T13:39:54+01:00 |
|
ea7b5e6 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
316 |
2018-12-10T20:36:13+01:00 |
6a2047f |
4b88a06 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
316 |
2018-12-08T22:10:52+01:00 |
fbc475e |
c4a5bfe |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
316 |
2018-12-08T04:59:05+01:00 |
acf4b77 |
e3ffcbd |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
316 |
2018-12-06T10:10:52+01:00 |
3f8f71f |
6b3f372 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
316 |
2018-12-06T09:43:01+01:00 |
3bc6640 |
2b6a365 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
316 |
2018-12-06T09:09:25+01:00 |
38e825f |
Available Results for the Program from Witness Store SV-COMP '18
Trying to find witnesses for program (a54c1d4dc961e3dcb9535534ea9396e952c503514c8f9921646b70acbbe35c1f, sv-benchmarks/c/seq-mthreaded/pals_floodmax.5_false-unreach-call.4.ufo.BOUNDED-10.pals_true-termination.c).
Found 12 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_floodmax.5_false-unreach-call.4.ufo.BOUNDED-10.pals_true-termination.c, a54c1d4dc961e3dcb9535534ea9396e952c503514c8f9921646b70acbbe35c1f
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/a54c1d4dc961e3dcb9535534ea9396e952c503514c8f9921646b70acbbe35c1f.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
837e62d |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
VeriAbs 1.3 |
481 |
Sat Dec 2 20:42:05 2017 |
|
87e5e21 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
ESBMC 4.6.0 kind |
82 |
2017-12-02T02:27:15.733013 |
|
483fe81 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
ESBMC 4.6.0 incr |
87 |
2017-12-01T08:54:50.005928 |
|
7e5282c |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
ESBMC 3.1 |
191 |
2017-12-01T18:32 CET (sv-comp) |
|
4266ea0 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
ESBMC 3.1 |
184 |
2017-11-30T19:41 CET (sv-comp) |
|
038b04f |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.6.1-svn 26773 |
568 |
2017-12-01T01:28:57+01:00 |
|
81896fa |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CBMC |
484 |
2017-12-01T00:27 CET (sv-comp) |
|
16846e1 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
2LS |
388 |
2017-11-30T12:49 CET (sv-comp) |
|
3e3d188 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
ESBMC 4.6.0 |
3 |
2017-12-03T00:05:21.392601 |
|
53ed3be |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
ESBMC 4.6.0 |
3 |
2017-12-02T08:56:51.273824 |
|
8e7c0eb |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
CBMC |
1245 |
2017-12-01T17:45 CET (sv-comp) |
|
523affa |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
2LS |
628 |
2017-12-01T12:58 CET (sv-comp) |
|
Available Results for the Program from Witness Store SV-COMP '17
Trying to find witnesses for program (a54c1d4dc961e3dcb9535534ea9396e952c503514c8f9921646b70acbbe35c1f, sv-benchmarks/c/seq-mthreaded/pals_floodmax.5_false-unreach-call.4.ufo.BOUNDED-10.pals_true-termination.c).
Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_floodmax.5_false-unreach-call.4.ufo.BOUNDED-10.pals_true-termination.c, a54c1d4dc961e3dcb9535534ea9396e952c503514c8f9921646b70acbbe35c1f
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/a54c1d4dc961e3dcb9535534ea9396e952c503514c8f9921646b70acbbe35c1f.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |