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/modulus_false-no-overflow.i |
programSHA | 0b0950a1c140edc93aae34a58bc0c626e3766e3bfa56dc925d737dd984426d29 |
witnessName | results-validated/cpa-seq-validate-violation-witnesses-2ls.2018-12-06_0936.logfiles/sv-comp19_prop-nooverflow.modulus_false-no-overflow.i.files/witness.graphml |
witnessSHA | e6da45855e2ee31378b17fa49fde5fc269464948b1071d78f27eb822d2f9eadc |
Key | Value |
architecture | 32bit |
creationtime | 2018-12-06T09:40:28+01:00 |
inputwitnesshash | 589415dc7b81306122bcc31066be41373aecdb8cd9d8a912c22fe0a986223b2f |
producer | CPAchecker 1.7-svn 29852 |
program-sha256 | 0b0950a1c140edc93aae34a58bc0c626e3766e3bfa56dc925d737dd984426d29 |
programfile | ../../sv-benchmarks/c/bitvector/modulus_false-no-overflow.i |
programhash | 0b0950a1c140edc93aae34a58bc0c626e3766e3bfa56dc925d737dd984426d29 |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! overflow) ) |
witness-file | witnessFileByHash/e6da45855e2ee31378b17fa49fde5fc269464948b1071d78f27eb822d2f9eadc.graphml |
witness-sha256 | e6da45855e2ee31378b17fa49fde5fc269464948b1071d78f27eb822d2f9eadc |
witness-size | 4245 |
witness-type | violation_witness |
This witness was created for this program (cf. table above, 0b0950a1c140edc93aae34a58bc0c626e3766e3bfa56dc925d737dd984426d29).
Found 0 witnesses for program sv-benchmarks/c/bitvector/modulus_false-no-overflow.i, 0b0950a1c140edc93aae34a58bc0c626e3766e3bfa56dc925d737dd984426d29
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/0b0950a1c140edc93aae34a58bc0c626e3766e3bfa56dc925d737dd984426d29.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/bitvector/modulus_false-no-overflow.i, 0b0950a1c140edc93aae34a58bc0c626e3766e3bfa56dc925d737dd984426d29
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/0b0950a1c140edc93aae34a58bc0c626e3766e3bfa56dc925d737dd984426d29.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/bitvector/modulus_false-no-overflow.i, 0b0950a1c140edc93aae34a58bc0c626e3766e3bfa56dc925d737dd984426d29
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/0b0950a1c140edc93aae34a58bc0c626e3766e3bfa56dc925d737dd984426d29.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/bitvector/modulus_false-no-overflow.i, 0b0950a1c140edc93aae34a58bc0c626e3766e3bfa56dc925d737dd984426d29
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/0b0950a1c140edc93aae34a58bc0c626e3766e3bfa56dc925d737dd984426d29.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 11 witnesses for program sv-benchmarks/c/bitvector/modulus_false-no-overflow.i, 0b0950a1c140edc93aae34a58bc0c626e3766e3bfa56dc925d737dd984426d29
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/0b0950a1c140edc93aae34a58bc0c626e3766e3bfa56dc925d737dd984426d29.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
e444100 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Pinaka | 4 | 2019-12-03T23:59 CET (comp) | ||
d0cd0e0 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 1.9 | 4 | 2019-12-11T21:53:09+01:00 | 107db04 | |
09889b0 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 1.9 | 4 | 2019-12-11T20:44:24+01:00 | 33c7781 | |
f0b1e9a | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 1.9 | 4 | 2019-12-06T02:40:53+01:00 | 6e74f7b | |
4711f48 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 1.9 | 4 | 2019-12-05T20:20:12+01:00 | 445205c | |
b1e3e18 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 1.9 | 4 | 2019-12-05T19:33:59+01:00 | 7742d60 | |
4785355 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 1.9 | 4 | 2019-12-04T02:58:03+01:00 | e444100 | |
27f8a02 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 1.9 | 4 | 2019-12-03T08:01:15+01:00 | ab77ceb | |
ab77ceb | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 1.9 | 4 | 2019-11-29T18:25:35+01:00 | ||
107db04 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 4 | 2019-12-01T01:57:18+01:00 | ||
b3ac2dd | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 1.9 | 7 | 2019-12-11T20:54:29+01:00 | fbc21d9 |
Found 16 witnesses for program sv-benchmarks/c/bitvector/modulus_false-no-overflow.i, 0b0950a1c140edc93aae34a58bc0c626e3766e3bfa56dc925d737dd984426d29
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/0b0950a1c140edc93aae34a58bc0c626e3766e3bfa56dc925d737dd984426d29.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
d40d354 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Symbiotic | 2 | 2018-12-08T06:24 CET (sv-comp) | ||
e2a8c5e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | SMACK 1.9.3 | 4 | 2018-12-08T01:16:47 | ||
27850fd | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Pinaka | 4 | 2018-12-06T20:34 CET (sv-comp) | ||
afa8d8f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 4 | 2018-12-07T09:33:27+01:00 | ||
2f1ab85 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-09T18:16:37+01:00 | b0dc734 | |
b28092e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-08T23:43:56+01:00 | d40d354 | |
9fa6801 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-08T22:08:48+01:00 | e2a8c5e | |
28041b9 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-08T08:48:19+01:00 | afa8d8f | |
578d0d1 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-08T05:02:36+01:00 | aae5c98 | |
78d79ff | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-07T17:43:28+01:00 | 27850fd | |
563ac4a | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-06T10:19:06+01:00 | 00366f3 | |
93947bb | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-06T09:48:04+01:00 | c176eb5 | |
e6da458 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-06T09:40:28+01:00 | 589415d | |
efd883d | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-06T09:19:38+01:00 | 28ffada | |
dd2f1cc | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-06T09:13:08+01:00 | f03da54 | |
c176eb5 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-06T05:12:51+01:00 |
Found 16 witnesses for program sv-benchmarks/c/bitvector/modulus_false-no-overflow.i, 0b0950a1c140edc93aae34a58bc0c626e3766e3bfa56dc925d737dd984426d29
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/0b0950a1c140edc93aae34a58bc0c626e3766e3bfa56dc925d737dd984426d29.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
c54b549 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Symbiotic | 2 | 2017-12-03T04:13 CET (sv-comp) | ||
aca80e8 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Map2Check | 3 | 2017-12-02T01:24 CET (sv-comp) | ||
ec5801f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | ESBMC 4.6.0 kind | 4 | 2017-12-02T18:29:36.735014 | ||
ff5382a | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | ESBMC 4.6.0 incr | 4 | 2017-12-02T06:38:15.776317 | ||
9fe67da | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | ESBMC 3.1 | 4 | 2017-12-01T14:28 CET (sv-comp) | ||
7e78864 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 5 | 2017-12-03T05:16:03+01:00 | 014a1e1 | |
1625338 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 5 | 2017-12-02T20:07:41+01:00 | 2ccb31e | |
7d7ab30 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 5 | 2017-12-02T08:11:40+01:00 | 14ad9e0 | |
f543627 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 5 | 2017-12-01T12:33:17+01:00 | cb7930e | |
d47808a | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 5 | 2017-12-01T12:02:16+01:00 | 1dc0f35 | |
46324d3 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 5 | 2017-12-01T11:19:22+01:00 | c97455a | |
49d250d | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 5 | 2017-12-01T11:04:10+01:00 | ||
3ba6f88 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CBMC | 4 | 2017-12-01T12:15 CET (sv-comp) | ||
589415d | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | 2LS | 4 | 2017-12-01T10:56 CET (sv-comp) | ||
49be64e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 8 | 2017-12-02T02:13:08+01:00 | 9355210 | |
b262639 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 8 | 2017-12-01T14:47:00+01:00 | 4378dc7 |
Found 0 witnesses for program sv-benchmarks/c/bitvector/modulus_false-no-overflow.i, 0b0950a1c140edc93aae34a58bc0c626e3766e3bfa56dc925d737dd984426d29
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/0b0950a1c140edc93aae34a58bc0c626e3766e3bfa56dc925d737dd984426d29.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |