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).
Key | Value |
programName | sv-benchmarks/c/ldv-regression/test24_true-unreach-call_true-termination.c |
programSHA | cc1815e5cb3973c51d39901b33005464c8969226287e77dd46669f2fab66e3ba |
witnessName | results-verified/ukojak.2018-12-08_1104.logfiles/sv-comp19_prop-reachsafety.test24_true-unreach-call_true-termination.c.files/witness.graphml |
witnessSHA | 098819592858d3bdcccccdf6e162f60be64dee49aa17748025dc0d6a9a866a0d |
Key | Value |
architecture | 32bit |
creationtime | 2018-12-09T09:09Z |
producer | Kojak |
programfile | /tmp/vcloud-vcloud-master/worker/working_dir_cebe2097-15e7-4e7f-836c-27219097abbe/sv-benchmarks/c/ldv-regression/test24_true-unreach-call_true-termination.c |
programhash | 043660dc5a969bbd34b12cbb93ba3e467b4f8613 |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/098819592858d3bdcccccdf6e162f60be64dee49aa17748025dc0d6a9a866a0d.graphml |
witness-sha256 | 098819592858d3bdcccccdf6e162f60be64dee49aa17748025dc0d6a9a866a0d |
witness-size | 10467 |
witness-type | correctness_witness |
Found 0 witnesses for program sv-benchmarks/c/ldv-regression/test24_true-unreach-call_true-termination.c, cc1815e5cb3973c51d39901b33005464c8969226287e77dd46669f2fab66e3ba
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/cc1815e5cb3973c51d39901b33005464c8969226287e77dd46669f2fab66e3ba.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/ldv-regression/test24_true-unreach-call_true-termination.c, cc1815e5cb3973c51d39901b33005464c8969226287e77dd46669f2fab66e3ba
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/cc1815e5cb3973c51d39901b33005464c8969226287e77dd46669f2fab66e3ba.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/ldv-regression/test24_true-unreach-call_true-termination.c, cc1815e5cb3973c51d39901b33005464c8969226287e77dd46669f2fab66e3ba
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/cc1815e5cb3973c51d39901b33005464c8969226287e77dd46669f2fab66e3ba.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/ldv-regression/test24_true-unreach-call_true-termination.c, cc1815e5cb3973c51d39901b33005464c8969226287e77dd46669f2fab66e3ba
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/cc1815e5cb3973c51d39901b33005464c8969226287e77dd46669f2fab66e3ba.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 18 witnesses for program sv-benchmarks/c/ldv-regression/test24_true-unreach-call_true-termination.c, cc1815e5cb3973c51d39901b33005464c8969226287e77dd46669f2fab66e3ba
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/cc1815e5cb3973c51d39901b33005464c8969226287e77dd46669f2fab66e3ba.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
7c463fd | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Pinaka | 3 | 2019-12-03T22:19 CET (comp) | ||
dfc0dae | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 6 | 2019-12-11T20:29:57+01:00 | 427e1d0 | |
6e1703d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 6 | 2019-12-11T20:17:32+01:00 | db5abad | |
6c5d1ea | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 6 | 2019-12-11T20:07:10+01:00 | 0f3a88b | |
5dd7ce3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 6 | 2019-12-11T20:02:22+01:00 | 317c27f | |
ab31aa1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 6 | 2019-12-08T00:36:23+01:00 | 760201c | |
c6efa1b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 6 | 2019-12-07T23:46:49+01:00 | 293f20a | |
e2e053c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 6 | 2019-12-07T23:44:39+01:00 | aa4ba99 | |
a82083b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 6 | 2019-12-07T19:40:56+01:00 | 0cbe70e | |
d3ffdf4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 6 | 2019-12-06T01:42:20+01:00 | c053bb0 | |
750dd6c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 6 | 2019-12-05T19:12:50+01:00 | 590a95a | |
5bec5ba | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 6 | 2019-12-04T02:07:58+01:00 | 7c463fd | |
70cf3d2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 6 | 2019-11-30T19:54:48+01:00 | b534533 | |
0779667 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 6 | 2019-11-30T17:23:32+01:00 | 37315ad | |
37315ad | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / svcomp20 | 6 | 2019-11-30T00:47:00+01:00 | ||
760201c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.8 | 6 | 2019-12-07T13:17:58+01:00 | ||
0f3a88b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco | 6 | 2019-11-30T22:26:33+01:00 | ||
fd66f7c | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2019-12-03T22:59 CET (comp) |
Found 20 witnesses for program sv-benchmarks/c/ldv-regression/test24_true-unreach-call_true-termination.c, cc1815e5cb3973c51d39901b33005464c8969226287e77dd46669f2fab66e3ba
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/cc1815e5cb3973c51d39901b33005464c8969226287e77dd46669f2fab66e3ba.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
7e98bf7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T19:40 CET (sv-comp) | ||
6970766 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | SMACK 1.9.3 | 3 | 2018-12-08T20:02:59 | ||
d0f28f3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 6 | 2018-12-07T09:36:23+01:00 | ||
90be448 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-10T20:05:43+01:00 | 0d1e70c | |
04f6b45 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-09T20:34:09+01:00 | 88a8008 | |
620a37e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-09T19:48:55+01:00 | 0988195 | |
6610ed0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-09T17:22:53+01:00 | b2859c4 | |
4da3123 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-08T23:18:00+01:00 | 7e98bf7 | |
30b0d8a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-08T21:35:40+01:00 | 6970766 | |
5c123be | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-08T06:00:42+01:00 | d0f28f3 | |
086db51 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-08T02:40:43+01:00 | cffc4cf | |
baa161e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-08T02:25:13+01:00 | 970c8ee | |
83e4c0a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-07T17:44:57+01:00 | 1c993ad | |
054b8e7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-07T08:52:43+01:00 | 1f1bfe9 | |
0313337 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-06T09:28:32+01:00 | a469493 | |
559d751 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-06T08:56:16+01:00 | c1d2cc5 | |
bf8e852 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-06T08:20:43+01:00 | 24ea2c2 | |
a60c3f4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-06T07:29:47+01:00 | 9d0891f | |
c1d2cc5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-06T07:16:35+01:00 | ||
e52f648 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T05:35 CET (sv-comp) |
Found 29 witnesses for program sv-benchmarks/c/ldv-regression/test24_true-unreach-call_true-termination.c, cc1815e5cb3973c51d39901b33005464c8969226287e77dd46669f2fab66e3ba
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/cc1815e5cb3973c51d39901b33005464c8969226287e77dd46669f2fab66e3ba.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
7b5542b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26758M | 12 | 2017-11-30T22:52:13+01:00 | ||
760a687 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | skink | 3 | 2017-12-01T22:14 CET (sv-comp) | ||
7010814 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Taipan | 9 | 2017-12-03T02:54Z | ||
d30d8ce | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Symbiotic | 1 | 2017-12-02T18:33 CET (sv-comp) | ||
9b973d3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Kojak | 11 | 2017-12-02T07:37Z | ||
74c8a4d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-03T01:12:52.299433 | ||
1732117 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T12:33:22.253674 | ||
8b4a8b6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 kind | 3 | 2017-12-01T21:36:13.195995 | ||
5c2ca7d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 incr | 3 | 2017-12-01T15:39:29.152347 | ||
4fe4bed | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 3.1 | 7 | 2017-12-01T19:39 CET (sv-comp) | ||
eb8f82d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn | 6 | 2017-12-02T23:42:53+01:00 | ||
ea1b357 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn | 4 | 2017-12-01T03:23:22+01:00 | ||
74172e2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 6 | 2017-12-03T06:59:52+01:00 | 286232a | |
0ea7dc7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 7 | 2017-12-03T04:08:30+01:00 | 99af053 | |
dbc5741 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 6 | 2017-12-03T01:49:01+01:00 | 11be26b | |
cf38ecf | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 6 | 2017-12-03T01:05:01+01:00 | 8a4285b | |
2bb5a28 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 6 | 2017-12-02T20:36:21+01:00 | 6d72bd2 | |
06c0f91 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 6 | 2017-12-02T14:20:09+01:00 | fbd9243 | |
eefa4cb | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 6 | 2017-12-02T08:32:30+01:00 | 8da582a | |
d72b9b4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 6 | 2017-12-02T00:13:50+01:00 | 8459e0a | |
852ebb4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 6 | 2017-12-01T22:21:41+01:00 | d4c75c7 | |
5572af4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 6 | 2017-12-01T08:13:58+01:00 | d8b6185 | |
5ce7a29 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 6 | 2017-12-01T05:11:33+01:00 | bb69bae | |
1b52a0e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 6 | 2017-12-01T04:41:49+01:00 | 48132b2 | |
1ff90e1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 6 | 2017-12-01T02:09:17+01:00 | ||
8a1c08a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker (unknown version) | 6 | 2017-12-02T01:14:31+01:00 | ||
a78242f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CBMC | 13 | 2017-11-30T13:54 CET (sv-comp) | ||
ec4a039 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Automizer | 9 | 2017-12-02T19:01Z | ||
29f616c | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 12 | 2017-12-01T15:07 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/ldv-regression/test24_true-unreach-call_true-termination.c, cc1815e5cb3973c51d39901b33005464c8969226287e77dd46669f2fab66e3ba
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/cc1815e5cb3973c51d39901b33005464c8969226287e77dd46669f2fab66e3ba.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |