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/jain_7_true-unreach-call_true-no-overflow_false-termination.i |
programSHA | 6a8bacdce81a8dd1ae9373269e3e34cade980c80920d4898b38a14df93e5bced |
witnessName | results-verified/cpa-seq.2018-12-05_0546.logfiles/sv-comp19_prop-reachsafety.jain_7_true-unreach-call_true-no-overflow_false-termination.i.files/witness.graphml |
witnessSHA | 0a91de5d6e828fcc9d02c70065dc092e0096e2bbb91cac777c606014e1a77782 |
Key | Value |
architecture | 32bit |
creationtime | 2018-12-05T12:37:10+01:00 |
producer | CPAchecker 1.7-svn 29852 |
program-sha256 | 6a8bacdce81a8dd1ae9373269e3e34cade980c80920d4898b38a14df93e5bced |
programfile | ../../sv-benchmarks/c/bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i |
programhash | 6a8bacdce81a8dd1ae9373269e3e34cade980c80920d4898b38a14df93e5bced |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/0a91de5d6e828fcc9d02c70065dc092e0096e2bbb91cac777c606014e1a77782.graphml |
witness-sha256 | 0a91de5d6e828fcc9d02c70065dc092e0096e2bbb91cac777c606014e1a77782 |
witness-size | 4247 |
witness-type | correctness_witness |
This witness was created for this program (cf. table above, 6a8bacdce81a8dd1ae9373269e3e34cade980c80920d4898b38a14df93e5bced).
Found 0 witnesses for program sv-benchmarks/c/bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i, 6a8bacdce81a8dd1ae9373269e3e34cade980c80920d4898b38a14df93e5bced
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/6a8bacdce81a8dd1ae9373269e3e34cade980c80920d4898b38a14df93e5bced.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i, 6a8bacdce81a8dd1ae9373269e3e34cade980c80920d4898b38a14df93e5bced
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/6a8bacdce81a8dd1ae9373269e3e34cade980c80920d4898b38a14df93e5bced.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i, 6a8bacdce81a8dd1ae9373269e3e34cade980c80920d4898b38a14df93e5bced
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/6a8bacdce81a8dd1ae9373269e3e34cade980c80920d4898b38a14df93e5bced.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i, 6a8bacdce81a8dd1ae9373269e3e34cade980c80920d4898b38a14df93e5bced
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/6a8bacdce81a8dd1ae9373269e3e34cade980c80920d4898b38a14df93e5bced.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i, 6a8bacdce81a8dd1ae9373269e3e34cade980c80920d4898b38a14df93e5bced
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/6a8bacdce81a8dd1ae9373269e3e34cade980c80920d4898b38a14df93e5bced.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 12 witnesses for program sv-benchmarks/c/bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i, 6a8bacdce81a8dd1ae9373269e3e34cade980c80920d4898b38a14df93e5bced
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/6a8bacdce81a8dd1ae9373269e3e34cade980c80920d4898b38a14df93e5bced.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
eb45f44 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T02:52 CET (sv-comp) | ||
fefd47c | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | SMACK 1.9.3 | 3 | 2018-12-08T08:58:53 | ||
e5e05b6 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 4 | 2018-12-08T01:27:43+01:00 | ||
a4827fe | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-05T11:22:23+01:00 | ||
8ecb51c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | SMACK 1.9.3 | 3 | 2018-12-08T02:23:32 | ||
89f2cbc | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 4 | 2018-12-07T01:23:02+01:00 | ||
ef89523 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-09T20:28:51+01:00 | 569cd22 | |
8e0113b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-09T20:17:08+01:00 | f4a613a | |
199359b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-09T19:55:46+01:00 | bb61b09 | |
0a91de5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-05T12:37:10+01:00 | ||
f8221e5 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 6 | 2018-12-06T13:10:55+01:00 | ||
dd76551 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-05T14:36:57+01:00 |
Found 21 witnesses for program sv-benchmarks/c/bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i, 6a8bacdce81a8dd1ae9373269e3e34cade980c80920d4898b38a14df93e5bced
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/6a8bacdce81a8dd1ae9373269e3e34cade980c80920d4898b38a14df93e5bced.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
84d368d | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Map2Check | 3 | 2017-12-02T00:58 CET (sv-comp) | ||
d28f9ef | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Taipan | 6 | 2017-12-03T07:44Z | ||
aad4e63 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Symbiotic | 1 | 2017-12-03T04:33 CET (sv-comp) | ||
0bab836 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Kojak | 6 | 2017-12-03T10:25Z | ||
ba6005f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | ESBMC 4.6.0 kind | 3 | 2017-12-02T18:23:50.911976 | ||
64af8cf | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | ESBMC 3.1 | 6 | 2017-12-01T13:25 CET (sv-comp) | ||
c24cd19 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 4 | 2017-12-01T11:15:15+01:00 | ||
6f289c9 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Automizer | 6 | 2017-12-03T10:24Z | ||
ec05237 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | 2LS | 12 | 2017-12-01T10:28 CET (sv-comp) | ||
023bd82 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | skink | 3 | 2017-12-01T22:43 CET (sv-comp) | ||
5997358 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Taipan | 6 | 2017-12-03T05:08Z | ||
6c6d74a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 4 | 2017-12-03T07:18:01+01:00 | 3ba4b37 | |
714a5f8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 4 | 2017-12-03T00:29:39+01:00 | 79f4f26 | |
9c1048d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 4 | 2017-12-02T00:29:27+01:00 | a0f39c3 | |
fabfa94 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 4 | 2017-11-30T15:13:55+01:00 | ||
8cd3dcc | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26758M | 11 | 2017-12-01T03:53:44+01:00 | ||
a990127 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26725 | 4 | 2017-11-30T23:47:00+01:00 | ||
044996b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Automizer | 6 | 2017-12-02T20:28Z | ||
8ffcc4c | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 6 | 2017-12-01T18:28:52+01:00 | ||
520a2cd | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | Automizer | 7 | 2017-12-03T11:14Z | ||
ecf3c43 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | 2LS | 8 | 2017-12-01T14:36 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i, 6a8bacdce81a8dd1ae9373269e3e34cade980c80920d4898b38a14df93e5bced
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/6a8bacdce81a8dd1ae9373269e3e34cade980c80920d4898b38a14df93e5bced.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |