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/bitvector/byte_add_1_true-unreach-call_true-no-overflow_true-termination.i |
programSHA | 9534af200f13816f4bbb1218022ee782061159f6f882fcb7a0fc9ce8ef190944 |
witnessName | results-verified/ukojak.2018-12-08_1104.logfiles/sv-comp19_prop-reachsafety.byte_add_1_true-unreach-call_true-no-overflow_true-termination.i.files/witness.graphml |
witnessSHA | fadc9be07f652571824ea8271b92361d96ef0399f7bb001e589e6132123a5cb1 |
Key | Value |
architecture | 32bit |
creationtime | 2018-12-09T07:42Z |
producer | Kojak |
programfile | /tmp/vcloud-vcloud-master/worker/working_dir_44ea21a2-7118-4808-b137-e1528f672400/sv-benchmarks/c/bitvector/byte_add_1_true-unreach-call_true-no-overflow_true-termination.i |
programhash | 6e973c5cecb5d30af2cf4ea74d1b0b1563334ffe |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/fadc9be07f652571824ea8271b92361d96ef0399f7bb001e589e6132123a5cb1.graphml |
witness-sha256 | fadc9be07f652571824ea8271b92361d96ef0399f7bb001e589e6132123a5cb1 |
witness-size | 162118 |
witness-type | correctness_witness |
Found 0 witnesses for program sv-benchmarks/c/bitvector/byte_add_1_true-unreach-call_true-no-overflow_true-termination.i, 9534af200f13816f4bbb1218022ee782061159f6f882fcb7a0fc9ce8ef190944
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/9534af200f13816f4bbb1218022ee782061159f6f882fcb7a0fc9ce8ef190944.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/bitvector/byte_add_1_true-unreach-call_true-no-overflow_true-termination.i, 9534af200f13816f4bbb1218022ee782061159f6f882fcb7a0fc9ce8ef190944
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/9534af200f13816f4bbb1218022ee782061159f6f882fcb7a0fc9ce8ef190944.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/bitvector/byte_add_1_true-unreach-call_true-no-overflow_true-termination.i, 9534af200f13816f4bbb1218022ee782061159f6f882fcb7a0fc9ce8ef190944
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/9534af200f13816f4bbb1218022ee782061159f6f882fcb7a0fc9ce8ef190944.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/bitvector/byte_add_1_true-unreach-call_true-no-overflow_true-termination.i, 9534af200f13816f4bbb1218022ee782061159f6f882fcb7a0fc9ce8ef190944
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/9534af200f13816f4bbb1218022ee782061159f6f882fcb7a0fc9ce8ef190944.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 18 witnesses for program sv-benchmarks/c/bitvector/byte_add_1_true-unreach-call_true-no-overflow_true-termination.i, 9534af200f13816f4bbb1218022ee782061159f6f882fcb7a0fc9ce8ef190944
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/9534af200f13816f4bbb1218022ee782061159f6f882fcb7a0fc9ce8ef190944.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
969123c | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Pinaka | 3 | 2019-12-03T23:11 CET (comp) | ||
0540a3c | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 1.9 | 20 | 2019-11-30T08:16:24+01:00 | ||
79ed83a | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 20 | 2019-12-01T02:10:15+01:00 | ||
d7038cb | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Pinaka | 3 | 2019-12-04T00:58 CET (comp) | ||
bd2c167 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 19 | 2019-12-11T20:28:26+01:00 | 10ef2ac | |
83fb5bb | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 19 | 2019-12-11T20:13:00+01:00 | b5af3a2 | |
904b552 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 19 | 2019-12-11T20:03:14+01:00 | 5a1b2cd | |
0b158e8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 19 | 2019-12-08T00:36:29+01:00 | 6937e86 | |
41e17c4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 19 | 2019-12-06T02:11:14+01:00 | 7dc6c71 | |
7d08813 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 19 | 2019-12-05T19:13:38+01:00 | 4a579fc | |
e5b382b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 19 | 2019-12-05T19:03:08+01:00 | b5479fd | |
130f0da | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 19 | 2019-12-04T02:08:03+01:00 | d7038cb | |
fea97eb | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 19 | 2019-11-30T19:51:21+01:00 | 13d25ba | |
dea236a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 19 | 2019-11-30T17:05:31+01:00 | 963977d | |
963977d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / svcomp20 | 19 | 2019-11-30T00:21:51+01:00 | ||
6937e86 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.8 | 27 | 2019-12-07T13:26:13+01:00 | ||
b5af3a2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco | 19 | 2019-12-01T00:27:22+01:00 | ||
61f746b | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2019-12-03T22:56 CET (comp) |
Found 26 witnesses for program sv-benchmarks/c/bitvector/byte_add_1_true-unreach-call_true-no-overflow_true-termination.i, 9534af200f13816f4bbb1218022ee782061159f6f882fcb7a0fc9ce8ef190944
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/9534af200f13816f4bbb1218022ee782061159f6f882fcb7a0fc9ce8ef190944.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
084600f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T03:17 CET (sv-comp) | ||
a8f4c2e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | SMACK 1.9.3 | 3 | 2018-12-07T20:56:38 | ||
bcdc1ea | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Pinaka | 3 | 2018-12-06T22:50 CET (sv-comp) | ||
d38e9fb | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 20 | 2018-12-07T02:50:13+01:00 | ||
0d8a7f6 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 20 | 2018-12-05T21:10:24+01:00 | ||
7bc6982 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T12:39 CET (sv-comp) | ||
2716e54 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | SMACK 1.9.3 | 3 | 2018-12-08T09:04:03 | ||
6004aad | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Pinaka | 3 | 2018-12-07T03:29 CET (sv-comp) | ||
35d0674 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7 | 27 | 2018-12-10T17:30:12+01:00 | ||
4ade45a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 24 | 2018-12-07T08:59:42+01:00 | ||
e464b03 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 26 | 2018-12-10T20:10:38+01:00 | 35d0674 | |
7000a32 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 20 | 2018-12-09T19:48:32+01:00 | fadc9be | |
932cb89 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 20 | 2018-12-08T23:10:03+01:00 | 7bc6982 | |
273db25 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 20 | 2018-12-08T21:37:14+01:00 | 2716e54 | |
e86a9e4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 20 | 2018-12-08T05:09:56+01:00 | 4ade45a | |
0941e52 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 20 | 2018-12-08T04:19:37+01:00 | c5d77c0 | |
3e0c8f3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 20 | 2018-12-08T02:09:05+01:00 | 9b506e9 | |
56383df | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 20 | 2018-12-07T16:38:56+01:00 | 6004aad | |
807c1ae | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 20 | 2018-12-06T09:28:57+01:00 | c0e4952 | |
a0e4a62 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 20 | 2018-12-06T09:08:57+01:00 | 7c1d37a | |
f78c86f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 20 | 2018-12-06T08:29:43+01:00 | 24ae525 | |
b7d3583 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 20 | 2018-12-06T07:58:49+01:00 | 8c6d9ee | |
0e16686 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 20 | 2018-12-06T07:12:16+01:00 | d5ad1bc | |
7c1d37a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 19 | 2018-12-05T16:53:59+01:00 | ||
a5848cb | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T11:37 CET (sv-comp) | ||
bd7b113 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2018-12-07T06:10 CET (sv-comp) |
Found 36 witnesses for program sv-benchmarks/c/bitvector/byte_add_1_true-unreach-call_true-no-overflow_true-termination.i, 9534af200f13816f4bbb1218022ee782061159f6f882fcb7a0fc9ce8ef190944
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/9534af200f13816f4bbb1218022ee782061159f6f882fcb7a0fc9ce8ef190944.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
91d1d66 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Taipan | 39 | 2017-12-03T07:44Z | ||
be535ca | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Symbiotic | 1 | 2017-12-03T04:12 CET (sv-comp) | ||
f2aafa6 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Map2Check | 9 | 2017-12-02T01:30 CET (sv-comp) | ||
00b6993 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Kojak | 40 | 2017-12-03T10:38Z | ||
abe8ad6 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | ESBMC 4.6.0 kind | 3 | 2017-12-02T18:17:39.299294 | ||
5d04cde | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | ESBMC 4.6.0 incr | 3 | 2017-12-02T06:09:45.209463 | ||
45fcf91 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | ESBMC 3.1 | 23 | 2017-12-01T13:16 CET (sv-comp) | ||
a550afb | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 19 | 2017-12-01T11:46:11+01:00 | ||
9b4e5d4 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CBMC | 69 | 2017-12-01T11:38 CET (sv-comp) | ||
ac2c304 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Automizer | 39 | 2017-12-03T10:28Z | ||
3767297 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | 2LS | 43 | 2017-12-01T10:43 CET (sv-comp) | ||
7c58ff5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker (unknown version) | 31 | 2017-12-01T22:36:00+01:00 | ||
a6f7901 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Symbiotic | 1 | 2017-12-02T04:03 CET (sv-comp) | ||
a8d1f16 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Map2Check | 9 | 2017-12-01T20:50 CET (sv-comp) | ||
e86f5b5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Kojak | 172 | 2017-12-02T06:39Z | ||
60264a4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-03T02:05:05.412020 | ||
97d3b22 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T14:00:35.168512 | ||
2a625b8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 kind | 3 | 2017-12-01T21:06:49.918966 | ||
af20299 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 incr | 3 | 2017-12-01T10:41:34.803928 | ||
1d5b9ed | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 3.1 | 28 | 2017-12-01T21:23 CET (sv-comp) | ||
d36396d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn | 22 | 2017-12-03T01:01:01+01:00 | ||
9a9f418 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn | 4 | 2017-12-01T04:18:44+01:00 | ||
d87a2f1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 23 | 2017-12-03T04:26:41+01:00 | 6caa401 | |
67544f2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 19 | 2017-12-03T02:21:52+01:00 | 1557ef8 | |
9cfdaf4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 19 | 2017-12-02T20:30:39+01:00 | 6409e8b | |
2194734 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 19 | 2017-12-02T08:36:34+01:00 | 1963c46 | |
4be62dc | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 19 | 2017-12-01T22:26:35+01:00 | d24e568 | |
ec5c6b4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 19 | 2017-12-01T22:05:02+01:00 | b85a7d4 | |
e3147ca | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 19 | 2017-12-01T08:13:31+01:00 | 8c36319 | |
dbb9064 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 19 | 2017-12-01T05:46:18+01:00 | 58aa97f | |
b0277a9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 19 | 2017-12-01T05:26:59+01:00 | f7153b0 | |
1e4a994 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 19 | 2017-12-01T05:15:39+01:00 | a4d8415 | |
00af9de | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 19 | 2017-11-30T15:45:40+01:00 | ||
b0c9b36 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CBMC | 63 | 2017-12-01T01:54 CET (sv-comp) | ||
361c468 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | 2LS | 121 | 2017-11-30T12:36 CET (sv-comp) | ||
e843eda | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 63 | 2017-12-01T15:28 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/bitvector/byte_add_1_true-unreach-call_true-no-overflow_true-termination.i, 9534af200f13816f4bbb1218022ee782061159f6f882fcb7a0fc9ce8ef190944
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/9534af200f13816f4bbb1218022ee782061159f6f882fcb7a0fc9ce8ef190944.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |