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-call3_true-termination.i |
programSHA | f89c0269d70253696d5d265b29e4d13734f5941022888f70158ba5176897fb96 |
witnessName | results-verified/symbiotic.2017-12-01_2241.logfiles/sv-comp18.array_true-unreach-call3_true-termination.i.files/witness.graphml |
witnessSHA | 7b8bb6bb90bb9526ae96b6248169dac803d539c334c27e12cd0cbd56d2ce57dd |
Key | Value |
architecture | 32bit |
creationtime | 2017-12-02T07:53 CET (sv-comp) |
producer | Symbiotic |
program-sha256 | f89c0269d70253696d5d265b29e4d13734f5941022888f70158ba5176897fb96 |
programfile | /tmp/vcloud-vcloud-master/worker/working_dir_0a61052c-9fa3-4ed7-a642-48089f8ec06f/sv-benchmarks/c/loop-acceleration/array_true-unreach-call3_true-termination.i |
programhash | 4090a90876c90ba415ea4bea59e2b23309410708 |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/7b8bb6bb90bb9526ae96b6248169dac803d539c334c27e12cd0cbd56d2ce57dd.graphml |
witness-sha256 | 7b8bb6bb90bb9526ae96b6248169dac803d539c334c27e12cd0cbd56d2ce57dd |
witness-size | 761 |
witness-type | correctness_witness |
Found 0 witnesses for program sv-benchmarks/c/loop-acceleration/array_true-unreach-call3_true-termination.i, f89c0269d70253696d5d265b29e4d13734f5941022888f70158ba5176897fb96
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/f89c0269d70253696d5d265b29e4d13734f5941022888f70158ba5176897fb96.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-call3_true-termination.i, f89c0269d70253696d5d265b29e4d13734f5941022888f70158ba5176897fb96
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/f89c0269d70253696d5d265b29e4d13734f5941022888f70158ba5176897fb96.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-call3_true-termination.i, f89c0269d70253696d5d265b29e4d13734f5941022888f70158ba5176897fb96
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/f89c0269d70253696d5d265b29e4d13734f5941022888f70158ba5176897fb96.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-call3_true-termination.i, f89c0269d70253696d5d265b29e4d13734f5941022888f70158ba5176897fb96
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/f89c0269d70253696d5d265b29e4d13734f5941022888f70158ba5176897fb96.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 16 witnesses for program sv-benchmarks/c/loop-acceleration/array_true-unreach-call3_true-termination.i, f89c0269d70253696d5d265b29e4d13734f5941022888f70158ba5176897fb96
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/f89c0269d70253696d5d265b29e4d13734f5941022888f70158ba5176897fb96.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
2537392 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Pinaka | 3 | 2019-12-03T22:07 CET (comp) | ||
dc8bd97 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 6 | 2019-12-11T20:26:39+01:00 | 8eeba46 | |
ea98dc0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 6 | 2019-12-11T20:17:29+01:00 | 6c4394b | |
1298ca6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 6 | 2019-12-11T20:13:57+01:00 | e1ee41a | |
0a24775 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 6 | 2019-12-11T20:02:33+01:00 | ca8583f | |
5e7472d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 6 | 2019-12-08T00:58:42+01:00 | 4608dd7 | |
0cb8dd0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 6 | 2019-12-07T23:27:46+01:00 | b4e855d | |
2d42ead | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 6 | 2019-12-07T19:40:30+01:00 | 570c0c3 | |
de5a9c8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 6 | 2019-12-06T01:59:38+01:00 | faf6ccb | |
3f15bed | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 6 | 2019-12-05T19:13:12+01:00 | 6619857 | |
3b5b65f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 6 | 2019-12-05T19:03:08+01:00 | 4c1fa8c | |
4ee5299 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 6 | 2019-12-04T02:08:04+01:00 | 2537392 | |
b6bc888 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 6 | 2019-11-30T16:13:41+01:00 | 136259b | |
136259b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / svcomp20 | 35 | 2019-11-29T15:06:13+01:00 | ||
6c4394b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco | 7 | 2019-12-01T04:29:38+01:00 | ||
305c105 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2019-12-04T00:17 CET (comp) |
Found 19 witnesses for program sv-benchmarks/c/loop-acceleration/array_true-unreach-call3_true-termination.i, f89c0269d70253696d5d265b29e4d13734f5941022888f70158ba5176897fb96
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/f89c0269d70253696d5d265b29e4d13734f5941022888f70158ba5176897fb96.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
79f71c6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T09:03 CET (sv-comp) | ||
a30e45b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Pinaka | 3 | 2018-12-07T05:18 CET (sv-comp) | ||
689e65d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 35 | 2018-12-07T09:57:08+01:00 | ||
f0a7303 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-10T19:56:56+01:00 | dc8f23a | |
749c84a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-09T21:06:10+01:00 | 6424ab9 | |
260a996 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-09T20:26:51+01:00 | 8414d7a | |
9f973c3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-09T17:38:36+01:00 | 1df1a5b | |
e3eaf15 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-08T23:10:49+01:00 | 79f71c6 | |
353acef | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-08T06:29:54+01:00 | 689e65d | |
36dfd26 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-08T03:05:45+01:00 | d5d2c79 | |
4d59432 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-07T17:44:43+01:00 | 1e6a4f4 | |
682eb55 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-07T16:38:42+01:00 | a30e45b | |
7ea52c8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-06T09:28:43+01:00 | 464434a | |
3553ee3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-06T08:45:26+01:00 | 75fe30e | |
d6af4b8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-06T08:17:28+01:00 | ba09809 | |
cea2a85 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-06T08:04:48+01:00 | 59b543c | |
75fe30e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 35 | 2018-12-05T10:29:00+01:00 | ||
d352cef | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T06:31 CET (sv-comp) | ||
f2ed476 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2018-12-07T08:30 CET (sv-comp) |
Found 26 witnesses for program sv-benchmarks/c/loop-acceleration/array_true-unreach-call3_true-termination.i, f89c0269d70253696d5d265b29e4d13734f5941022888f70158ba5176897fb96
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/f89c0269d70253696d5d265b29e4d13734f5941022888f70158ba5176897fb96.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
1e6a4f4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | skink | 3 | 2017-12-01T22:14 CET (sv-comp) | ||
f555249 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Taipan | 7 | 2017-12-03T04:01Z | ||
7b8bb6b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Symbiotic | 1 | 2017-12-02T07:53 CET (sv-comp) | ||
695924e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-03T01:29:20.578319 | ||
17d57df | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T10:33:28.749274 | ||
9e3d670 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 kind | 3 | 2017-12-01T21:55:01.306616 | ||
8fcc841 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 incr | 3 | 2017-12-01T14:48:13.228347 | ||
a923d79 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.12-svcomp17 | 4 | 2017-11-02T13:16:17+05:30 | ||
003a042 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn | 4 | 2017-12-01T04:50:09+01:00 | ||
6bd904f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 6 | 2017-12-03T06:58:01+01:00 | c676cbb | |
b3785a2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 6 | 2017-12-03T04:19:46+01:00 | 18b380a | |
c25f55b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 6 | 2017-12-03T02:11:27+01:00 | 0b725bb | |
7dc57ca | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 6 | 2017-12-02T20:48:02+01:00 | 0f0bf71 | |
1253694 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 6 | 2017-12-02T08:54:29+01:00 | 1ccaf92 | |
1d79a3f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 6 | 2017-12-02T00:08:47+01:00 | b400d5d | |
21ba854 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 6 | 2017-12-01T22:27:23+01:00 | 109c3bb | |
619fcb2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 6 | 2017-12-01T08:13:52+01:00 | 06ddbce | |
40e50f4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 21 | 2017-12-01T07:08:17+01:00 | ec177fe | |
128efae | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 7 | 2017-12-01T06:23:10+01:00 | e4ae044 | |
29472a7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 6 | 2017-12-01T06:16:07+01:00 | c0a4823 | |
2b64dcd | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 35 | 2017-11-30T14:32:38+01:00 | ||
7fbbac0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CBMC | 1335 | 2017-11-30T16:52 CET (sv-comp) | ||
bb2f54a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Automizer | 7 | 2017-12-02T18:13Z | ||
ad502a3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | 2LS | 10 | 2017-11-30T13:58 CET (sv-comp) | ||
03160e2 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 1335 | 2017-12-01T13:45 CET (sv-comp) | ||
39f3471 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | 2LS | 10 | 2017-12-01T12:03 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/loop-acceleration/array_true-unreach-call3_true-termination.i, f89c0269d70253696d5d265b29e4d13734f5941022888f70158ba5176897fb96
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/f89c0269d70253696d5d265b29e4d13734f5941022888f70158ba5176897fb96.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |