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/eca-rers2012/Problem02_label50_false-unreach-call_false-termination.c |
programSHA | 8ba94fbd0d8056071476d651633fdb5d90f00e46120ef081e3840338df422a31 |
witnessName | results-verified/depthk.2018-12-05_0936.logfiles/sv-comp19_prop-termination.Problem02_label50_false-unreach-call_false-termination.c.files/witness.graphml |
witnessSHA | 1477c8a91b8007a942579658e2561b2af42b0fe0da31d2bbcc2c2e4f9e3074f9 |
Key | Value |
architecture | 32bit |
creationtime | 2018-12-05T20:18:21.479356 |
producer | DepthK v3.0 |
programfile | /tmp/vcloud-vcloud-master/worker/working_dir_0ac8fa63-5ccb-4cb7-b87f-1f8d17a5cbff/sv-benchmarks/c/eca-rers2012/Problem02_label50_false-unreach-call_false-termination.c |
programhash | c88dc41bb0c5752717ba5895f8d33afd40276a61 |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/1477c8a91b8007a942579658e2561b2af42b0fe0da31d2bbcc2c2e4f9e3074f9.graphml |
witness-sha256 | 1477c8a91b8007a942579658e2561b2af42b0fe0da31d2bbcc2c2e4f9e3074f9 |
witness-size | 4481 |
witness-type | violation_witness |
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem02_label50_false-unreach-call_false-termination.c, 8ba94fbd0d8056071476d651633fdb5d90f00e46120ef081e3840338df422a31
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/8ba94fbd0d8056071476d651633fdb5d90f00e46120ef081e3840338df422a31.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem02_label50_false-unreach-call_false-termination.c, 8ba94fbd0d8056071476d651633fdb5d90f00e46120ef081e3840338df422a31
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/8ba94fbd0d8056071476d651633fdb5d90f00e46120ef081e3840338df422a31.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem02_label50_false-unreach-call_false-termination.c, 8ba94fbd0d8056071476d651633fdb5d90f00e46120ef081e3840338df422a31
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/8ba94fbd0d8056071476d651633fdb5d90f00e46120ef081e3840338df422a31.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem02_label50_false-unreach-call_false-termination.c, 8ba94fbd0d8056071476d651633fdb5d90f00e46120ef081e3840338df422a31
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/8ba94fbd0d8056071476d651633fdb5d90f00e46120ef081e3840338df422a31.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 19 witnesses for program sv-benchmarks/c/eca-rers2012/Problem02_label50_false-unreach-call_false-termination.c, 8ba94fbd0d8056071476d651633fdb5d90f00e46120ef081e3840338df422a31
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/8ba94fbd0d8056071476d651633fdb5d90f00e46120ef081e3840338df422a31.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
d67cfb6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 2 | 2019-12-01 05:20:16 | ||
28fe766 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Pinaka | 52 | 2019-12-04T00:39 CET (comp) | ||
aa71702 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 159 | 2019-12-11T21:48:27+01:00 | 1df7d92 | |
7f7b700 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 159 | 2019-12-11T21:09:04+01:00 | d67cfb6 | |
4d07776 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 217 | 2019-12-11T20:55:09+01:00 | 15248f8 | |
9b7c9a4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 230 | 2019-12-11T20:44:45+01:00 | ebbd8f0 | |
5b8852d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 200 | 2019-12-08T01:52:19+01:00 | 8ab8e14 | |
0fb40bc | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 201 | 2019-12-04T02:58:27+01:00 | 28fe766 | |
5dfc93a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 160 | 2019-12-03T08:10:06+01:00 | e2cc8e9 | |
e2cc8e9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / svcomp20 | 159 | 2019-11-29T17:39:39+01:00 | ||
1df7d92 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco | 160 | 2019-12-01T00:19:12+01:00 | ||
5fe2266 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 280 | 2019-12-11T22:00:57+01:00 | 9f3839b | |
f824e65 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 280 | 2019-12-08T00:27:19+01:00 | 128680e | |
2e06fe6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 280 | 2019-12-07T21:19:14+01:00 | b1b194e | |
106376c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 280 | 2019-12-05T20:21:33+01:00 | fe0595e | |
b602372 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 280 | 2019-12-05T19:35:46+01:00 | 1e187b3 | |
b85b81d | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | Symbiotic | 2 | 2019-12-02 05:08:40 | ||
07360bb | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.9 | 359 | 2019-11-30T02:02:08+01:00 | ||
ea3f93f | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 359 | 2019-12-01T01:40:24+01:00 |
Found 23 witnesses for program sv-benchmarks/c/eca-rers2012/Problem02_label50_false-unreach-call_false-termination.c, 8ba94fbd0d8056071476d651633fdb5d90f00e46120ef081e3840338df422a31
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/8ba94fbd0d8056071476d651633fdb5d90f00e46120ef081e3840338df422a31.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
8f5207c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2018-12-08T11:20 CET (sv-comp) | ||
92a9e05 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | SMACK 1.9.3 | 6 | 2018-12-08T01:34:34 | ||
53e694d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Pinaka | 61 | 2018-12-07T15:38 CET (sv-comp) | ||
b5ec9c9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 160 | 2018-12-08T01:59:27+01:00 | ||
255caae | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 200 | 2018-12-10T20:38:21+01:00 | 03162a4 | |
5d7ec79 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 159 | 2018-12-09T18:20:23+01:00 | b4d321f | |
33b25e2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 160 | 2018-12-08T23:42:53+01:00 | 8f5207c | |
f7ce28d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 159 | 2018-12-08T22:08:43+01:00 | 92a9e05 | |
670eb04 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 159 | 2018-12-08T08:05:57+01:00 | b5ec9c9 | |
8f115ae | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 159 | 2018-12-08T05:03:12+01:00 | 0044e06 | |
9605d6a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 201 | 2018-12-07T17:43:05+01:00 | 53e694d | |
f84215e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 159 | 2018-12-06T10:17:09+01:00 | 9664b9b | |
4f34257 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 160 | 2018-12-06T09:49:17+01:00 | 1ba6089 | |
001fec4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 278 | 2018-12-06T09:19:00+01:00 | eb61663 | |
1ba6089 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 159 | 2018-12-05T14:51:27+01:00 | ||
bb08463 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 280 | 2018-12-09T20:53:15+01:00 | 76978c9 | |
66f85be | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 280 | 2018-12-09T20:36:37+01:00 | 0c2d453 | |
a6b0bda | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 280 | 2018-12-09T20:34:34+01:00 | 8866747 | |
84b720c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 280 | 2018-12-06T09:43:02+01:00 | ffac3d6 | |
4c5e34b | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 359 | 2018-12-07T19:03:48+01:00 | ||
d13a51f | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn 29852 | 356 | 2018-12-08T09:05:03+01:00 | ||
1236377 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn 29852 | 356 | 2018-12-06T09:48:16+01:00 | ||
3dc61d3 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn 29852 | 359 | 2018-12-05T10:31:30+01:00 |
Found 18 witnesses for program sv-benchmarks/c/eca-rers2012/Problem02_label50_false-unreach-call_false-termination.c, 8ba94fbd0d8056071476d651633fdb5d90f00e46120ef081e3840338df422a31
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/8ba94fbd0d8056071476d651633fdb5d90f00e46120ef081e3840338df422a31.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
babdddf | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Veriabs | 3 | 2017-12-03T00:48 CET (sv-comp) | ||
fbc7fb2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Taipan | 129 | 2017-12-03T05:01Z | ||
7f4c0e5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2017-12-02T07:00 CET (sv-comp) | ||
c436361 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Kojak | 129 | 2017-12-02T06:57Z | ||
faaf4d6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 kind | 4 | 2017-12-02T01:21:30.787446 | ||
eb69d71 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 incr | 5 | 2017-12-01T11:43:00.377791 | ||
7795d9e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 10 | 2017-12-01T17:18 CET (sv-comp) | ||
9ffa7ae | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 10 | 2017-11-30T17:35 CET (sv-comp) | ||
60bf0ce | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 92 | 2017-11-30T21:26:06+01:00 | ||
4952e54 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26758M | 222 | 2017-12-01T02:06:57+01:00 | ||
e67c7c0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26725 | 90 | 2017-11-30T17:02:26+01:00 | ||
4533c2b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker (unknown version) | 160 | 2017-12-02T13:24:18+01:00 | ||
e145f22 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CBMC | 67 | 2017-11-30T14:35 CET (sv-comp) | ||
1b78982 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Automizer | 129 | 2017-12-02T07:30Z | ||
1d4ff88 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | 2LS | 67 | 2017-11-30T23:41 CET (sv-comp) | ||
c6096b6 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 334 | 2017-12-01T14:28:46+01:00 | ||
2fd8348 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | Automizer | 15 | 2017-12-03T11:17Z | ||
3968361 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | 2LS | 26 | 2017-12-01T16:56 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem02_label50_false-unreach-call_false-termination.c, 8ba94fbd0d8056071476d651633fdb5d90f00e46120ef081e3840338df422a31
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/8ba94fbd0d8056071476d651633fdb5d90f00e46120ef081e3840338df422a31.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |