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/loop-acceleration/array_true-unreach-call2_true-termination.i |
programSHA | 41ef36c9196e37909032d0af0542413f965f9b97cd349d0c1d36b1634eb171bd |
witnessName | results-validated/cpa-seq-validate-correctness-witnesses-pinaka.2018-12-07_1617.logfiles/sv-comp19_prop-reachsafety.array_true-unreach-call2_true-termination.i.files/witness.graphml |
witnessSHA | 3d0afe0804bb6ef7becd02a6dafacf4fcc1cf65d6e6b1f59b1124f7e9fda13c4 |
Key | Value |
architecture | 32bit |
creationtime | 2018-12-07T16:41:50+01:00 |
inputwitnesshash | d2caccdc1c05a913ba70cb4599e0170734108b3dcfc0d25f90c84db13b6c3fe7 |
producer | CPAchecker 1.7-svn 29852 |
program-sha256 | 41ef36c9196e37909032d0af0542413f965f9b97cd349d0c1d36b1634eb171bd |
programfile | ../../sv-benchmarks/c/loop-acceleration/array_true-unreach-call2_true-termination.i |
programhash | 41ef36c9196e37909032d0af0542413f965f9b97cd349d0c1d36b1634eb171bd |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/3d0afe0804bb6ef7becd02a6dafacf4fcc1cf65d6e6b1f59b1124f7e9fda13c4.graphml |
witness-sha256 | 3d0afe0804bb6ef7becd02a6dafacf4fcc1cf65d6e6b1f59b1124f7e9fda13c4 |
witness-size | 5037 |
witness-type | correctness_witness |
This witness was created for this program (cf. table above, 41ef36c9196e37909032d0af0542413f965f9b97cd349d0c1d36b1634eb171bd).
Found 0 witnesses for program sv-benchmarks/c/loop-acceleration/array_true-unreach-call2_true-termination.i, 41ef36c9196e37909032d0af0542413f965f9b97cd349d0c1d36b1634eb171bd
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/41ef36c9196e37909032d0af0542413f965f9b97cd349d0c1d36b1634eb171bd.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/loop-acceleration/array_true-unreach-call2_true-termination.i, 41ef36c9196e37909032d0af0542413f965f9b97cd349d0c1d36b1634eb171bd
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/41ef36c9196e37909032d0af0542413f965f9b97cd349d0c1d36b1634eb171bd.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/loop-acceleration/array_true-unreach-call2_true-termination.i, 41ef36c9196e37909032d0af0542413f965f9b97cd349d0c1d36b1634eb171bd
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/41ef36c9196e37909032d0af0542413f965f9b97cd349d0c1d36b1634eb171bd.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/loop-acceleration/array_true-unreach-call2_true-termination.i, 41ef36c9196e37909032d0af0542413f965f9b97cd349d0c1d36b1634eb171bd
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/41ef36c9196e37909032d0af0542413f965f9b97cd349d0c1d36b1634eb171bd.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 9 witnesses for program sv-benchmarks/c/loop-acceleration/array_true-unreach-call2_true-termination.i, 41ef36c9196e37909032d0af0542413f965f9b97cd349d0c1d36b1634eb171bd
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/41ef36c9196e37909032d0af0542413f965f9b97cd349d0c1d36b1634eb171bd.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
f262557 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Pinaka | 3 | 2019-12-03T22:50 CET (comp) | ||
2894e44 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 5 | 2019-12-11T20:29:31+01:00 | e4c5440 | |
302251c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 5 | 2019-12-11T20:02:56+01:00 | af122ff | |
774cb4a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 5 | 2019-12-08T00:52:04+01:00 | 086462a | |
2e4dc23 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 5 | 2019-12-06T01:41:10+01:00 | 6a16a18 | |
da47342 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 5 | 2019-12-05T19:13:59+01:00 | f69cb88 | |
6aca7e4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 5 | 2019-12-04T02:07:59+01:00 | f262557 | |
5388b18 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 5 | 2019-11-30T19:51:59+01:00 | 73d7f4c | |
e4a17c4 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2019-12-04T00:03 CET (comp) |
Found 15 witnesses for program sv-benchmarks/c/loop-acceleration/array_true-unreach-call2_true-termination.i, 41ef36c9196e37909032d0af0542413f965f9b97cd349d0c1d36b1634eb171bd
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/41ef36c9196e37909032d0af0542413f965f9b97cd349d0c1d36b1634eb171bd.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
068777d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T00:32 CET (sv-comp) | ||
f257e40 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | SMACK 1.9.3 | 3 | 2018-12-08T05:51:14 | ||
d2caccd | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Pinaka | 3 | 2018-12-07T12:54 CET (sv-comp) | ||
ce145ee | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-10T20:23:06+01:00 | 343f9dc | |
a9e3a39 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-09T21:21:04+01:00 | 31e0f4c | |
d48e8e4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-08T23:18:13+01:00 | 068777d | |
1d2e6b3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-08T21:50:27+01:00 | f257e40 | |
3bdcd74 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-08T04:35:20+01:00 | 50e6f56 | |
361cc32 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-07T18:00:00+01:00 | 7ab8a11 | |
3d0afe0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-07T16:41:50+01:00 | d2caccd | |
436a8ac | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-06T08:20:03+01:00 | 3ca2970 | |
4f2a6cf | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-06T07:41:26+01:00 | 1ac58f3 | |
366b63c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 35 | 2018-12-06T02:28:09+01:00 | ||
afc1903 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T06:37 CET (sv-comp) | ||
95e7db0 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2018-12-07T01:03 CET (sv-comp) |
Found 18 witnesses for program sv-benchmarks/c/loop-acceleration/array_true-unreach-call2_true-termination.i, 41ef36c9196e37909032d0af0542413f965f9b97cd349d0c1d36b1634eb171bd
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/41ef36c9196e37909032d0af0542413f965f9b97cd349d0c1d36b1634eb171bd.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
7ab8a11 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | skink | 3 | 2017-12-01T22:26 CET (sv-comp) | ||
b67ab43 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Symbiotic | 1 | 2017-12-02T00:10 CET (sv-comp) | ||
210457c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Map2Check | 4 | 2017-12-01T20:12 CET (sv-comp) | ||
f6866d2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-03T02:22:48.313535 | ||
82647cc | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T14:31:39.893681 | ||
0f1fb25 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 kind | 3 | 2017-12-01T12:09:22.176037 | ||
e5d7b7a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 incr | 3 | 2017-12-01T08:21:00.026473 | ||
6ee1d89 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.12-svcomp17 | 4 | 2017-11-02T13:16:17+05:30 | ||
d03cdca | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 5 | 2017-12-03T04:32:59+01:00 | 7b73a71 | |
b8055a1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 5 | 2017-12-02T20:42:55+01:00 | 995c701 | |
79c48c1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 5 | 2017-12-02T07:38:29+01:00 | cb118b2 | |
8b5a2e8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 5 | 2017-12-02T00:23:46+01:00 | 0513701 | |
ed7b12e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 5 | 2017-12-01T22:36:48+01:00 | bc505ed | |
9298b71 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 5 | 2017-12-01T22:34:47+01:00 | 238a48f | |
b6899ab | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 5 | 2017-12-01T05:04:02+01:00 | 9ff3c91 | |
376f89f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CBMC | 2133 | 2017-11-30T21:31 CET (sv-comp) | ||
a593a6e | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 2132 | 2017-12-01T17:12 CET (sv-comp) | ||
4d1db22 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | 2LS | 9 | 2017-12-01T12:55 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/loop-acceleration/array_true-unreach-call2_true-termination.i, 41ef36c9196e37909032d0af0542413f965f9b97cd349d0c1d36b1634eb171bd
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/41ef36c9196e37909032d0af0542413f965f9b97cd349d0c1d36b1634eb171bd.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |