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_lcr-var-start-time.5_false-unreach-call.2.ufo.UNBOUNDED.pals.c |
programSHA |
1a670b4fbeabf1f11baa9f4cc2bb55de60afce7eda87c258973d4f43d63c6636 |
witnessName |
results-verified/verifuzz.2018-12-09_0247.logfiles/sv-comp19_prop-reachsafety.pals_lcr-var-start-time.5_false-unreach-call.2.ufo.UNBOUNDED.pals.c.files/witness.graphml |
witnessSHA |
56888c5c7283dd0b7319af342e09a2b9b27c80c66e96566d29fce6f601e74be0 |
Information about the Witness from Competition Database
from https://sv-comp.sosy-lab.org/2019/results/witnessInfoByHash/56888c5c7283dd0b7319af342e09a2b9b27c80c66e96566d29fce6f601e74be0.json
Key |
Value |
architecture |
32bit |
creationtime |
2018-12-09T14:44 CET (sv-comp) |
memorymodel |
precise |
producer |
verifuzz |
programfile |
/home/benchexec/VERIFUZZ_TEMP_DIR/OUT/pals_lcr-var-start-time.5_false-unreach-call.2.ufo.UNBOUNDED.pals.c |
programhash |
f28d54ed211f46bb4a2be31b557c08c9d019f036 |
sourcecodelang |
C |
specification |
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file |
witnessFileByHash/56888c5c7283dd0b7319af342e09a2b9b27c80c66e96566d29fce6f601e74be0.graphml |
witness-sha256 |
56888c5c7283dd0b7319af342e09a2b9b27c80c66e96566d29fce6f601e74be0 |
witness-size |
8315 |
witness-type |
violation_witness |
Available Results for the Program from Witness Store SV-COMP '24
Trying to find witnesses for program (1a670b4fbeabf1f11baa9f4cc2bb55de60afce7eda87c258973d4f43d63c6636, sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.5_false-unreach-call.2.ufo.UNBOUNDED.pals.c).
Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.5_false-unreach-call.2.ufo.UNBOUNDED.pals.c, 1a670b4fbeabf1f11baa9f4cc2bb55de60afce7eda87c258973d4f43d63c6636
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/1a670b4fbeabf1f11baa9f4cc2bb55de60afce7eda87c258973d4f43d63c6636.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 (1a670b4fbeabf1f11baa9f4cc2bb55de60afce7eda87c258973d4f43d63c6636, sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.5_false-unreach-call.2.ufo.UNBOUNDED.pals.c).
Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.5_false-unreach-call.2.ufo.UNBOUNDED.pals.c, 1a670b4fbeabf1f11baa9f4cc2bb55de60afce7eda87c258973d4f43d63c6636
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/1a670b4fbeabf1f11baa9f4cc2bb55de60afce7eda87c258973d4f43d63c6636.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 (1a670b4fbeabf1f11baa9f4cc2bb55de60afce7eda87c258973d4f43d63c6636, sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.5_false-unreach-call.2.ufo.UNBOUNDED.pals.c).
Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.5_false-unreach-call.2.ufo.UNBOUNDED.pals.c, 1a670b4fbeabf1f11baa9f4cc2bb55de60afce7eda87c258973d4f43d63c6636
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/1a670b4fbeabf1f11baa9f4cc2bb55de60afce7eda87c258973d4f43d63c6636.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 (1a670b4fbeabf1f11baa9f4cc2bb55de60afce7eda87c258973d4f43d63c6636, sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.5_false-unreach-call.2.ufo.UNBOUNDED.pals.c).
Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.5_false-unreach-call.2.ufo.UNBOUNDED.pals.c, 1a670b4fbeabf1f11baa9f4cc2bb55de60afce7eda87c258973d4f43d63c6636
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/1a670b4fbeabf1f11baa9f4cc2bb55de60afce7eda87c258973d4f43d63c6636.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 (1a670b4fbeabf1f11baa9f4cc2bb55de60afce7eda87c258973d4f43d63c6636, sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.5_false-unreach-call.2.ufo.UNBOUNDED.pals.c).
Found 11 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.5_false-unreach-call.2.ufo.UNBOUNDED.pals.c, 1a670b4fbeabf1f11baa9f4cc2bb55de60afce7eda87c258973d4f43d63c6636
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/1a670b4fbeabf1f11baa9f4cc2bb55de60afce7eda87c258973d4f43d63c6636.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
7d1c267 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
Pinaka |
181 |
2019-12-03T22:54 CET (comp) |
|
549b206 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
274 |
2019-12-11T21:59:22+01:00 |
969a8e5 |
4680084 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
258 |
2019-12-11T20:44:27+01:00 |
a2c97f2 |
4621a74 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
274 |
2019-12-03T08:10:32+01:00 |
06041c0 |
06041c0 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / svcomp20 |
281 |
2019-11-29T14:45:12+01:00 |
|
969a8e5 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco |
276 |
2019-12-01T01:57:05+01:00 |
|
7471712 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
52 |
2019-12-11T20:55:21+01:00 |
c98ceb5 |
1209151 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
52 |
2019-12-08T01:52:18+01:00 |
fc1b193 |
0bbc75d |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
51 |
2019-12-05T20:21:07+01:00 |
98e2c19 |
12f32b5 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
52 |
2019-12-05T19:34:57+01:00 |
3549874 |
f5abc00 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
53 |
2019-12-04T02:58:30+01:00 |
7d1c267 |
Available Results for the Program from Witness Store SV-COMP '19
Trying to find witnesses for program (1a670b4fbeabf1f11baa9f4cc2bb55de60afce7eda87c258973d4f43d63c6636, sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.5_false-unreach-call.2.ufo.UNBOUNDED.pals.c).
Found 14 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.5_false-unreach-call.2.ufo.UNBOUNDED.pals.c, 1a670b4fbeabf1f11baa9f4cc2bb55de60afce7eda87c258973d4f43d63c6636
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/1a670b4fbeabf1f11baa9f4cc2bb55de60afce7eda87c258973d4f43d63c6636.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
c15f538 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
Symbiotic |
12 |
2018-12-08T03:11 CET (sv-comp) |
|
d4ebf95 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
SMACK 1.9.3 |
65 |
2018-12-08T06:27:11 |
|
774f578 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn b8d6131600+ |
278 |
2018-12-06T23:55:05+01:00 |
|
8e51c6a |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
258 |
2018-12-09T18:21:07+01:00 |
56888c5 |
17be90a |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
258 |
2018-12-08T23:43:30+01:00 |
c15f538 |
9b9e160 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
275 |
2018-12-08T08:28:19+01:00 |
774f578 |
6b70ae8 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
275 |
2018-12-06T09:48:28+01:00 |
10b88fd |
10b88fd |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
281 |
2018-12-06T00:50:27+01:00 |
|
9f655d7 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
52 |
2018-12-10T20:37:02+01:00 |
c4ff9c3 |
d90a4c9 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
52 |
2018-12-08T22:10:31+01:00 |
d4ebf95 |
e386687 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
52 |
2018-12-08T05:06:08+01:00 |
84063be |
97474c4 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
52 |
2018-12-06T10:20:14+01:00 |
b91e134 |
802746f |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
52 |
2018-12-06T09:42:49+01:00 |
fac6b34 |
da173b5 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
51 |
2018-12-06T09:09:52+01:00 |
6846948 |
Available Results for the Program from Witness Store SV-COMP '18
Trying to find witnesses for program (1a670b4fbeabf1f11baa9f4cc2bb55de60afce7eda87c258973d4f43d63c6636, sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.5_false-unreach-call.2.ufo.UNBOUNDED.pals.c).
Found 8 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.5_false-unreach-call.2.ufo.UNBOUNDED.pals.c, 1a670b4fbeabf1f11baa9f4cc2bb55de60afce7eda87c258973d4f43d63c6636
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/1a670b4fbeabf1f11baa9f4cc2bb55de60afce7eda87c258973d4f43d63c6636.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
931b1d8 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
VeriAbs 1.3 |
194 |
Sat Dec 2 21:27:44 2017 |
|
bd68ed1 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
Symbiotic |
12 |
2017-12-02T03:23 CET (sv-comp) |
|
e66c047 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
ESBMC 4.6.0 kind |
31 |
2017-12-02T01:58:51.946594 |
|
f513927 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
ESBMC 4.6.0 incr |
32 |
2017-12-01T10:39:50.639902 |
|
1c12155 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
ESBMC 3.1 |
86 |
2017-11-30T16:44 CET (sv-comp) |
|
cdc0e78 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.6.1-svn 26773 |
271 |
2017-11-30T17:46:49+01:00 |
|
fe8ba75 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CBMC |
199 |
2017-11-30T17:26 CET (sv-comp) |
|
e4ec2e8 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
2LS |
168 |
2017-12-01T01:29 CET (sv-comp) |
|
Available Results for the Program from Witness Store SV-COMP '17
Trying to find witnesses for program (1a670b4fbeabf1f11baa9f4cc2bb55de60afce7eda87c258973d4f43d63c6636, sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.5_false-unreach-call.2.ufo.UNBOUNDED.pals.c).
Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.5_false-unreach-call.2.ufo.UNBOUNDED.pals.c, 1a670b4fbeabf1f11baa9f4cc2bb55de60afce7eda87c258973d4f43d63c6636
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/1a670b4fbeabf1f11baa9f4cc2bb55de60afce7eda87c258973d4f43d63c6636.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |