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 | ../../../comp/sv-benchmarks/c/reducercommutativity/rangesum40_false-unreach-call.i |
programSHA | 8a2694cc92f116b1d40f63dcd703d0139bba1f3bd0b7e28d69fa3d9cfe58ded3 |
witnessName | results-verified/symbiotic.2017-12-01_2241.logfiles/sv-comp18.rangesum40_false-unreach-call.i.files/witness.graphml |
witnessSHA | df63c3f9a65d8b9bc00fd13c7dddbd54c176df4c07168cbfbded5750e97b6afc |
Key | Value |
architecture | 32bit |
creationtime | 2017-12-02T00:58 CET (sv-comp) |
producer | Symbiotic |
program-sha256 | 8a2694cc92f116b1d40f63dcd703d0139bba1f3bd0b7e28d69fa3d9cfe58ded3 |
programfile | /tmp/vcloud-vcloud-master/worker/working_dir_2e0249d5-f71a-4565-9260-15550dc93b82/sv-benchmarks/c/reducercommutativity/rangesum40_false-unreach-call.i |
programhash | 3bc22eacddab290eba000ecad4885815ce9878ac |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/df63c3f9a65d8b9bc00fd13c7dddbd54c176df4c07168cbfbded5750e97b6afc.graphml |
witness-sha256 | df63c3f9a65d8b9bc00fd13c7dddbd54c176df4c07168cbfbded5750e97b6afc |
witness-size | 790 |
witness-type | violation_witness |
Found 0 witnesses for program ../../../comp/sv-benchmarks/c/reducercommutativity/rangesum40_false-unreach-call.i, 8a2694cc92f116b1d40f63dcd703d0139bba1f3bd0b7e28d69fa3d9cfe58ded3
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/8a2694cc92f116b1d40f63dcd703d0139bba1f3bd0b7e28d69fa3d9cfe58ded3.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program ../../../comp/sv-benchmarks/c/reducercommutativity/rangesum40_false-unreach-call.i, 8a2694cc92f116b1d40f63dcd703d0139bba1f3bd0b7e28d69fa3d9cfe58ded3
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/8a2694cc92f116b1d40f63dcd703d0139bba1f3bd0b7e28d69fa3d9cfe58ded3.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program ../../../comp/sv-benchmarks/c/reducercommutativity/rangesum40_false-unreach-call.i, 8a2694cc92f116b1d40f63dcd703d0139bba1f3bd0b7e28d69fa3d9cfe58ded3
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/8a2694cc92f116b1d40f63dcd703d0139bba1f3bd0b7e28d69fa3d9cfe58ded3.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program ../../../comp/sv-benchmarks/c/reducercommutativity/rangesum40_false-unreach-call.i, 8a2694cc92f116b1d40f63dcd703d0139bba1f3bd0b7e28d69fa3d9cfe58ded3
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/8a2694cc92f116b1d40f63dcd703d0139bba1f3bd0b7e28d69fa3d9cfe58ded3.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 11 witnesses for program ../../../comp/sv-benchmarks/c/reducercommutativity/rangesum40_false-unreach-call.i, 8a2694cc92f116b1d40f63dcd703d0139bba1f3bd0b7e28d69fa3d9cfe58ded3
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/8a2694cc92f116b1d40f63dcd703d0139bba1f3bd0b7e28d69fa3d9cfe58ded3.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
cc2444f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Pinaka | 158 | 2019-12-03T22:20 CET (comp) | ||
0b3a86c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 331 | 2019-12-11T21:40:29+01:00 | 4db0443 | |
4db0443 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco | 318 | 2019-11-30T22:49:39+01:00 | ||
cee3de7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 12 | 2019-12-11T20:54:32+01:00 | 6322df4 | |
2d4e2e6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 13 | 2019-12-11T20:45:54+01:00 | 70a4819 | |
cc033d8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 13 | 2019-12-08T01:52:15+01:00 | bfa9930 | |
0eaa696 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 10 | 2019-12-05T20:20:46+01:00 | b7470f3 | |
137d400 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 13 | 2019-12-04T02:58:38+01:00 | cc2444f | |
b4ef691 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 13 | 2019-12-03T08:58:49+01:00 | ea18acc | |
bf4981a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 10 | 2019-12-03T08:10:29+01:00 | cfcd21f | |
cfcd21f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / svcomp20 | 20 | 2019-11-30T07:44:20+01:00 |
Found 17 witnesses for program ../../../comp/sv-benchmarks/c/reducercommutativity/rangesum40_false-unreach-call.i, 8a2694cc92f116b1d40f63dcd703d0139bba1f3bd0b7e28d69fa3d9cfe58ded3
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/8a2694cc92f116b1d40f63dcd703d0139bba1f3bd0b7e28d69fa3d9cfe58ded3.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
9cb3a93 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2018-12-08T08:12 CET (sv-comp) | ||
961c8aa | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | SMACK 1.9.3 | 4 | 2018-12-08T16:34:03 | ||
ae95d86 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Pinaka | 167 | 2018-12-07T15:49 CET (sv-comp) | ||
8b49806 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 318 | 2018-12-08T04:03:29+01:00 | ||
87c942a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 330 | 2018-12-08T08:59:41+01:00 | 8b49806 | |
12b9e99 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 332 | 2018-12-07T17:45:23+01:00 | ae95d86 | |
30677f9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-10T20:35:35+01:00 | 90d76a3 | |
f15c87b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-09T18:01:15+01:00 | 89e4c33 | |
da26621 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-08T23:45:34+01:00 | 9cb3a93 | |
2e96ef1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-08T22:09:05+01:00 | 961c8aa | |
b184818 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 12 | 2018-12-08T05:05:21+01:00 | c2c5f1c | |
d4dd392 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-08T03:51:31+01:00 | c596398 | |
16d737a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 10 | 2018-12-06T10:20:42+01:00 | c503777 | |
3af5517 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 11 | 2018-12-06T09:49:34+01:00 | d71566f | |
e6332e4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 10 | 2018-12-06T09:19:17+01:00 | baf36bd | |
3458555 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 10 | 2018-12-06T09:01:43+01:00 | d4a2894 | |
d71566f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 20 | 2018-12-05T16:24:27+01:00 |
Found 10 witnesses for program ../../../comp/sv-benchmarks/c/reducercommutativity/rangesum40_false-unreach-call.i, 8a2694cc92f116b1d40f63dcd703d0139bba1f3bd0b7e28d69fa3d9cfe58ded3
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/8a2694cc92f116b1d40f63dcd703d0139bba1f3bd0b7e28d69fa3d9cfe58ded3.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
6bccddb | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | skink | 3 | 2017-12-01T23:53 CET (sv-comp) | ||
1a2e911 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | VIAP | 4 | 2017-12-03T03:51 CET (sv-comp) | ||
df63c3f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2017-12-02T00:58 CET (sv-comp) | ||
fc70bc3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Map2Check | 13 | 2017-12-01T20:58 CET (sv-comp) | ||
b36740c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 kind | 33 | 2017-12-01T17:51:42.231102 | ||
f8b9f39 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 incr | 33 | 2017-12-01T10:02:10.325335 | ||
3eb870a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn | 284 | 2017-12-02T21:25:39+01:00 | ||
c065c99 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26758M | 364 | 2017-11-30T21:09:40+01:00 | ||
e34e110 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker (unknown version) | 166 | 2017-12-02T10:21:14+01:00 | ||
664de07 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CBMC | 204 | 2017-11-30T22:06 CET (sv-comp) |
Found 0 witnesses for program ../../../comp/sv-benchmarks/c/reducercommutativity/rangesum40_false-unreach-call.i, 8a2694cc92f116b1d40f63dcd703d0139bba1f3bd0b7e28d69fa3d9cfe58ded3
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/8a2694cc92f116b1d40f63dcd703d0139bba1f3bd0b7e28d69fa3d9cfe58ded3.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |