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.6_false-unreach-call.2.ufo.BOUNDED-12.pals_true-termination.c |
programSHA |
73c46a3f89411959188ac7ee26077027a0eeca3e2f382125e516f68989a4d768 |
witnessName |
results-verified/cbmc.2017-11-30_1120.logfiles/sv-comp18.pals_lcr-var-start-time.6_false-unreach-call.2.ufo.BOUNDED-12.pals_true-termination.c.files/witness.graphml |
witnessSHA |
f43bc720acf8f69edf68ff2fe2347c4e132136c5f50d49deb10bee834fa5ca91 |
Information about the Witness from Competition Database
from https://sv-comp.sosy-lab.org/2018/results/witnessInfoByHash/f43bc720acf8f69edf68ff2fe2347c4e132136c5f50d49deb10bee834fa5ca91.json
Key |
Value |
architecture |
32bit |
creationtime |
2017-11-30T11:46 CET (sv-comp) |
producer |
CBMC |
program-sha256 |
73c46a3f89411959188ac7ee26077027a0eeca3e2f382125e516f68989a4d768 |
programfile |
../../sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.6_false-unreach-call.2.ufo.BOUNDED-12.pals_true-termination.c |
programhash |
c9907cb75ed84c11388be65b346c48a42942e3a6 |
sourcecodelang |
C |
specification |
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file |
witnessFileByHash/f43bc720acf8f69edf68ff2fe2347c4e132136c5f50d49deb10bee834fa5ca91.graphml |
witness-sha256 |
f43bc720acf8f69edf68ff2fe2347c4e132136c5f50d49deb10bee834fa5ca91 |
witness-size |
299160 |
witness-type |
violation_witness |
Available Results for the Program from Witness Store SV-COMP '24
Trying to find witnesses for program (73c46a3f89411959188ac7ee26077027a0eeca3e2f382125e516f68989a4d768, sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.6_false-unreach-call.2.ufo.BOUNDED-12.pals_true-termination.c).
Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.6_false-unreach-call.2.ufo.BOUNDED-12.pals_true-termination.c, 73c46a3f89411959188ac7ee26077027a0eeca3e2f382125e516f68989a4d768
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/73c46a3f89411959188ac7ee26077027a0eeca3e2f382125e516f68989a4d768.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 (73c46a3f89411959188ac7ee26077027a0eeca3e2f382125e516f68989a4d768, sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.6_false-unreach-call.2.ufo.BOUNDED-12.pals_true-termination.c).
Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.6_false-unreach-call.2.ufo.BOUNDED-12.pals_true-termination.c, 73c46a3f89411959188ac7ee26077027a0eeca3e2f382125e516f68989a4d768
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/73c46a3f89411959188ac7ee26077027a0eeca3e2f382125e516f68989a4d768.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 (73c46a3f89411959188ac7ee26077027a0eeca3e2f382125e516f68989a4d768, sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.6_false-unreach-call.2.ufo.BOUNDED-12.pals_true-termination.c).
Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.6_false-unreach-call.2.ufo.BOUNDED-12.pals_true-termination.c, 73c46a3f89411959188ac7ee26077027a0eeca3e2f382125e516f68989a4d768
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/73c46a3f89411959188ac7ee26077027a0eeca3e2f382125e516f68989a4d768.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 (73c46a3f89411959188ac7ee26077027a0eeca3e2f382125e516f68989a4d768, sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.6_false-unreach-call.2.ufo.BOUNDED-12.pals_true-termination.c).
Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.6_false-unreach-call.2.ufo.BOUNDED-12.pals_true-termination.c, 73c46a3f89411959188ac7ee26077027a0eeca3e2f382125e516f68989a4d768
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/73c46a3f89411959188ac7ee26077027a0eeca3e2f382125e516f68989a4d768.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 (73c46a3f89411959188ac7ee26077027a0eeca3e2f382125e516f68989a4d768, sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.6_false-unreach-call.2.ufo.BOUNDED-12.pals_true-termination.c).
Found 11 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.6_false-unreach-call.2.ufo.BOUNDED-12.pals_true-termination.c, 73c46a3f89411959188ac7ee26077027a0eeca3e2f382125e516f68989a4d768
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/73c46a3f89411959188ac7ee26077027a0eeca3e2f382125e516f68989a4d768.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
71352b4 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
Pinaka |
251 |
2019-12-03T23:19 CET (comp) |
|
46c4960 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
379 |
2019-12-11T21:50:37+01:00 |
e35fb8d |
891c80f |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
362 |
2019-12-11T20:44:28+01:00 |
0dea433 |
8da4ff0 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
379 |
2019-12-03T08:09:33+01:00 |
1888a82 |
1888a82 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / svcomp20 |
388 |
2019-11-30T14:55:42+01:00 |
|
e35fb8d |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco |
380 |
2019-11-30T23:39:19+01:00 |
|
ab36bcf |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
61 |
2019-12-11T20:54:50+01:00 |
20de75f |
4d88006 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
62 |
2019-12-08T01:52:26+01:00 |
72ae1b3 |
29cf7ea |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
61 |
2019-12-05T20:20:51+01:00 |
10a4c69 |
4622bfa |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
62 |
2019-12-05T19:34:28+01:00 |
aabc2f4 |
fd04ef8 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
62 |
2019-12-04T02:58:05+01:00 |
71352b4 |
Available Results for the Program from Witness Store SV-COMP '19
Trying to find witnesses for program (73c46a3f89411959188ac7ee26077027a0eeca3e2f382125e516f68989a4d768, sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.6_false-unreach-call.2.ufo.BOUNDED-12.pals_true-termination.c).
Found 15 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.6_false-unreach-call.2.ufo.BOUNDED-12.pals_true-termination.c, 73c46a3f89411959188ac7ee26077027a0eeca3e2f382125e516f68989a4d768
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/73c46a3f89411959188ac7ee26077027a0eeca3e2f382125e516f68989a4d768.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
4f7012d |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
Symbiotic |
14 |
2018-12-08T02:58 CET (sv-comp) |
|
dbeec78 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
SMACK 1.9.3 |
103 |
2018-12-08T05:39:53 |
|
23c03ca |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn b8d6131600+ |
384 |
2018-12-06T22:38:21+01:00 |
|
3ce4eac |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
362 |
2018-12-09T18:20:59+01:00 |
3a68e9a |
be1de4f |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
362 |
2018-12-08T23:43:34+01:00 |
4f7012d |
0646e38 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
379 |
2018-12-08T09:00:20+01:00 |
23c03ca |
f70c3b3 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
379 |
2018-12-06T09:48:56+01:00 |
5bf02f4 |
5bf02f4 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
388 |
2018-12-06T06:57:38+01:00 |
|
b010f81 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
62 |
2018-12-10T20:35:56+01:00 |
148975f |
6db3013 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
61 |
2018-12-08T22:07:26+01:00 |
dbeec78 |
4114595 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
62 |
2018-12-08T05:02:23+01:00 |
5067988 |
ea2f02a |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
62 |
2018-12-06T10:19:11+01:00 |
a40f4d3 |
b32ce2d |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
62 |
2018-12-06T09:42:20+01:00 |
ef7fb6b |
5752bea |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
61 |
2018-12-06T09:17:37+01:00 |
d3abed7 |
c9dd745 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
Symbiotic |
1 |
2018-12-08T10:02 CET (sv-comp) |
|
Available Results for the Program from Witness Store SV-COMP '18
Trying to find witnesses for program (73c46a3f89411959188ac7ee26077027a0eeca3e2f382125e516f68989a4d768, sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.6_false-unreach-call.2.ufo.BOUNDED-12.pals_true-termination.c).
Found 14 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.6_false-unreach-call.2.ufo.BOUNDED-12.pals_true-termination.c, 73c46a3f89411959188ac7ee26077027a0eeca3e2f382125e516f68989a4d768
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/73c46a3f89411959188ac7ee26077027a0eeca3e2f382125e516f68989a4d768.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
6749de6 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
VeriAbs 1.3 |
269 |
Sun Dec 3 00:05:51 2017 |
|
e8f3aae |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
Symbiotic |
14 |
2017-12-02T02:11 CET (sv-comp) |
|
c49f11f |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
ESBMC 4.6.0 kind |
42 |
2017-12-01T16:08:21.812886 |
|
b25c0be |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
ESBMC 4.6.0 incr |
42 |
2017-12-01T09:22:23.539968 |
|
cf0c926 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
ESBMC 3.1 |
124 |
2017-12-01T19:55 CET (sv-comp) |
|
0e02b16 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
ESBMC 3.1 |
119 |
2017-12-01T03:48 CET (sv-comp) |
|
034d097 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.6.1-svn 26773 |
376 |
2017-11-30T15:54:24+01:00 |
|
5bffcca |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker (unknown version) |
232 |
2017-12-02T05:13:22+01:00 |
|
f43bc72 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CBMC |
299 |
2017-11-30T11:46 CET (sv-comp) |
|
49d877e |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
2LS |
245 |
2017-11-30T12:44 CET (sv-comp) |
|
afb798c |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
ESBMC 4.6.0 |
3 |
2017-12-02T21:49:10.424528 |
|
5aa5880 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
ESBMC 4.6.0 |
3 |
2017-12-02T12:29:45.566118 |
|
74210b8 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
CBMC |
564 |
2017-12-01T13:10 CET (sv-comp) |
|
561c01a |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
2LS |
112 |
2017-12-01T15:35 CET (sv-comp) |
|
Available Results for the Program from Witness Store SV-COMP '17
Trying to find witnesses for program (73c46a3f89411959188ac7ee26077027a0eeca3e2f382125e516f68989a4d768, sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.6_false-unreach-call.2.ufo.BOUNDED-12.pals_true-termination.c).
Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.6_false-unreach-call.2.ufo.BOUNDED-12.pals_true-termination.c, 73c46a3f89411959188ac7ee26077027a0eeca3e2f382125e516f68989a4d768
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/73c46a3f89411959188ac7ee26077027a0eeca3e2f382125e516f68989a4d768.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |