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/loops/invert_string_true-unreach-call_true-termination.i |
programSHA | 7d1e1085960ce45c0ce267f697714b70bddb591dd05a4bcb4b118a4ce9db6861 |
witnessName | results-verified/veriabs.2018-12-10_1650.logfiles/sv-comp19_prop-reachsafety.invert_string_true-unreach-call_true-termination.i.files/witness.graphml |
witnessSHA | 035260f9656091c7e642cd38f8a3284df4ee26e72d10875bfa3e972cfe3a6fdf |
Key | Value |
architecture | 32bit |
creationtime | 2018-12-10T17:49:36+01:00 |
producer | CPAchecker 1.7 |
program-sha256 | 7d1e1085960ce45c0ce267f697714b70bddb591dd05a4bcb4b118a4ce9db6861 |
programfile | /home/benchexec/ar_abs_temp/invert_string_true_unreach_call_true_termination.c |
programhash | 7d1e1085960ce45c0ce267f697714b70bddb591dd05a4bcb4b118a4ce9db6861 |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/035260f9656091c7e642cd38f8a3284df4ee26e72d10875bfa3e972cfe3a6fdf.graphml |
witness-sha256 | 035260f9656091c7e642cd38f8a3284df4ee26e72d10875bfa3e972cfe3a6fdf |
witness-size | 7930 |
witness-type | correctness_witness |
This witness was created for this program (cf. table above, 7d1e1085960ce45c0ce267f697714b70bddb591dd05a4bcb4b118a4ce9db6861).
Found 0 witnesses for program sv-benchmarks/c/loops/invert_string_true-unreach-call_true-termination.i, 7d1e1085960ce45c0ce267f697714b70bddb591dd05a4bcb4b118a4ce9db6861
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/7d1e1085960ce45c0ce267f697714b70bddb591dd05a4bcb4b118a4ce9db6861.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/loops/invert_string_true-unreach-call_true-termination.i, 7d1e1085960ce45c0ce267f697714b70bddb591dd05a4bcb4b118a4ce9db6861
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/7d1e1085960ce45c0ce267f697714b70bddb591dd05a4bcb4b118a4ce9db6861.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/loops/invert_string_true-unreach-call_true-termination.i, 7d1e1085960ce45c0ce267f697714b70bddb591dd05a4bcb4b118a4ce9db6861
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/7d1e1085960ce45c0ce267f697714b70bddb591dd05a4bcb4b118a4ce9db6861.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/loops/invert_string_true-unreach-call_true-termination.i, 7d1e1085960ce45c0ce267f697714b70bddb591dd05a4bcb4b118a4ce9db6861
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/7d1e1085960ce45c0ce267f697714b70bddb591dd05a4bcb4b118a4ce9db6861.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/loops/invert_string_true-unreach-call_true-termination.i, 7d1e1085960ce45c0ce267f697714b70bddb591dd05a4bcb4b118a4ce9db6861
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/7d1e1085960ce45c0ce267f697714b70bddb591dd05a4bcb4b118a4ce9db6861.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 24 witnesses for program sv-benchmarks/c/loops/invert_string_true-unreach-call_true-termination.i, 7d1e1085960ce45c0ce267f697714b70bddb591dd05a4bcb4b118a4ce9db6861
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/7d1e1085960ce45c0ce267f697714b70bddb591dd05a4bcb4b118a4ce9db6861.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
a177881 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T16:30 CET (sv-comp) | ||
d3f57ba | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | SMACK 1.9.3 | 3 | 2018-12-08T02:19:30 | ||
543dd9e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Pinaka | 3 | 2018-12-07T01:15 CET (sv-comp) | ||
035260f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7 | 8 | 2018-12-10T17:49:36+01:00 | ||
1fa23dd | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 9 | 2018-12-07T10:34:37+01:00 | ||
650afe2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-10T20:09:55+01:00 | 035260f | |
6e8d1ce | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-09T21:06:38+01:00 | 7ebf521 | |
97fb492 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-09T20:06:47+01:00 | d1cdf05 | |
c6b05b2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-09T19:49:26+01:00 | fa267e9 | |
b8733e0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-08T23:15:41+01:00 | a177881 | |
5e282aa | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-08T21:46:37+01:00 | d3f57ba | |
3f7b933 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-08T06:00:58+01:00 | 1fa23dd | |
98b56ff | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-08T04:03:25+01:00 | 9422bfe | |
9980eed | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-08T02:33:57+01:00 | 19e7e05 | |
721e8d7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-07T17:45:19+01:00 | 6797ee6 | |
5a80c97 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-07T16:39:38+01:00 | 543dd9e | |
6446b7a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-06T09:29:12+01:00 | 8b38a9c | |
e69eed7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-06T08:56:04+01:00 | af9af57 | |
f0b8785 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-06T08:17:22+01:00 | 0e0a3a5 | |
5060c36 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-06T07:53:26+01:00 | bb22cdf | |
e6aff01 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-06T07:13:23+01:00 | 63c776c | |
af9af57 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-05T22:33:24+01:00 | ||
e3731cb | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T06:39 CET (sv-comp) | ||
05e834c | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2018-12-07T04:00 CET (sv-comp) |
Found 35 witnesses for program sv-benchmarks/c/loops/invert_string_true-unreach-call_true-termination.i, 7d1e1085960ce45c0ce267f697714b70bddb591dd05a4bcb4b118a4ce9db6861
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/7d1e1085960ce45c0ce267f697714b70bddb591dd05a4bcb4b118a4ce9db6861.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
ef04229 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26758M | 29 | 2017-12-01T03:47:17+01:00 | ||
96d6a22 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26725 | 15 | 2017-12-01T02:30:39+01:00 | ||
6797ee6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | skink | 3 | 2017-12-01T22:11 CET (sv-comp) | ||
1688888 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Taipan | 11 | 2017-12-02T23:16Z | ||
29ad765 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Symbiotic | 1 | 2017-12-02T13:20 CET (sv-comp) | ||
32937d2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Map2Check | 4 | 2017-12-01T21:22 CET (sv-comp) | ||
994c27e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Kojak | 19 | 2017-12-02T12:50Z | ||
7cdfc15 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T23:24:42.324181 | ||
a23b835 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T10:11:19.725351 | ||
23f51e9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 kind | 3 | 2017-12-01T14:39:22.572148 | ||
b71de2c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 incr | 3 | 2017-12-01T08:05:26.133934 | ||
efa701c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 3.1 | 10 | 2017-12-01T16:32 CET (sv-comp) | ||
84361d3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn | 9 | 2017-12-02T21:36:38+01:00 | ||
a959d3c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn | 4 | 2017-12-01T05:42:53+01:00 | ||
086b7d2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 7 | 2017-12-03T07:02:54+01:00 | b773eb7 | |
4f56c75 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 7 | 2017-12-03T04:23:47+01:00 | d0b9598 | |
28398de | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 9 | 2017-12-03T01:33:29+01:00 | 5df9d7c | |
6889fcd | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 8 | 2017-12-03T00:48:04+01:00 | 816b789 | |
46a6f56 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 7 | 2017-12-02T20:47:21+01:00 | 0167bbd | |
23e9626 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 7 | 2017-12-02T15:13:56+01:00 | eaad0e9 | |
374eb47 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 7 | 2017-12-02T08:19:18+01:00 | 1a15f48 | |
d14b1c9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 7 | 2017-12-02T00:06:47+01:00 | c719998 | |
ce9e42a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 7 | 2017-12-01T22:26:23+01:00 | 1955fc1 | |
054c69d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 7 | 2017-12-01T22:08:40+01:00 | f42677e | |
88ec782 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 7 | 2017-12-01T08:12:45+01:00 | ffadc85 | |
1ab7b8b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 7 | 2017-12-01T06:41:21+01:00 | e1e8635 | |
feba057 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 7 | 2017-12-01T06:17:24+01:00 | 31c7807 | |
6307242 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 7 | 2017-12-01T05:01:18+01:00 | 09de94b | |
902b848 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 7 | 2017-12-01T03:28:02+01:00 | ||
6e4eb6e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker (unknown version) | 8 | 2017-12-02T09:44:56+01:00 | ||
e407130 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CBMC | 22 | 2017-11-30T15:46 CET (sv-comp) | ||
c8e101f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Automizer | 11 | 2017-12-02T09:50Z | ||
60343c9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | 2LS | 41 | 2017-11-30T21:51 CET (sv-comp) | ||
56f957b | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 21 | 2017-12-01T16:10 CET (sv-comp) | ||
0ad01b1 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | 2LS | 15 | 2017-12-01T11:50 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/loops/invert_string_true-unreach-call_true-termination.i, 7d1e1085960ce45c0ce267f697714b70bddb591dd05a4bcb4b118a4ce9db6861
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/7d1e1085960ce45c0ce267f697714b70bddb591dd05a4bcb4b118a4ce9db6861.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |