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/recursive-simple/id_i20_o20_false-unreach-call_true-termination.c |
programSHA | 21a977dc01fbb676ffbd104991f6d1e698de7db9cfedad64decaf2424e4fc66b |
witnessName | results-verified/depthk.2018-12-05_0936.logfiles/sv-comp19_prop-reachsafety.id_i20_o20_false-unreach-call_true-termination.c.files/witness.graphml |
witnessSHA | 0203a90290e9cdc0fdf23aa29e2115425374879b25faae12a6bbb203581af2d4 |
Key | Value |
architecture | 32bit |
creationtime | 2018-12-05T15:45:27.869855 |
producer | DepthK v3.0 |
programfile | /tmp/vcloud-vcloud-master/worker/working_dir_c035c4f4-8475-44d1-991e-591bc86e9c7d/sv-benchmarks/c/recursive-simple/id_i20_o20_false-unreach-call_true-termination.c |
programhash | 7d05936c4bb1bb97a4b24ebc11d02c0e844c743b |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/0203a90290e9cdc0fdf23aa29e2115425374879b25faae12a6bbb203581af2d4.graphml |
witness-sha256 | 0203a90290e9cdc0fdf23aa29e2115425374879b25faae12a6bbb203581af2d4 |
witness-size | 3688 |
witness-type | violation_witness |
Found 0 witnesses for program sv-benchmarks/c/recursive-simple/id_i20_o20_false-unreach-call_true-termination.c, 21a977dc01fbb676ffbd104991f6d1e698de7db9cfedad64decaf2424e4fc66b
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/21a977dc01fbb676ffbd104991f6d1e698de7db9cfedad64decaf2424e4fc66b.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/recursive-simple/id_i20_o20_false-unreach-call_true-termination.c, 21a977dc01fbb676ffbd104991f6d1e698de7db9cfedad64decaf2424e4fc66b
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/21a977dc01fbb676ffbd104991f6d1e698de7db9cfedad64decaf2424e4fc66b.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/recursive-simple/id_i20_o20_false-unreach-call_true-termination.c, 21a977dc01fbb676ffbd104991f6d1e698de7db9cfedad64decaf2424e4fc66b
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/21a977dc01fbb676ffbd104991f6d1e698de7db9cfedad64decaf2424e4fc66b.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/recursive-simple/id_i20_o20_false-unreach-call_true-termination.c, 21a977dc01fbb676ffbd104991f6d1e698de7db9cfedad64decaf2424e4fc66b
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/21a977dc01fbb676ffbd104991f6d1e698de7db9cfedad64decaf2424e4fc66b.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 18 witnesses for program sv-benchmarks/c/recursive-simple/id_i20_o20_false-unreach-call_true-termination.c, 21a977dc01fbb676ffbd104991f6d1e698de7db9cfedad64decaf2424e4fc66b
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/21a977dc01fbb676ffbd104991f6d1e698de7db9cfedad64decaf2424e4fc66b.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
6855ac2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2019-12-02 00:02:06 | ||
ffd281f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Pinaka | 13 | 2019-12-03T23:49 CET (comp) | ||
b7e6f30 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 27 | 2019-12-11T21:49:16+01:00 | bc062dd | |
8f9653d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 27 | 2019-12-11T21:40:56+01:00 | c88de69 | |
dce008a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 27 | 2019-12-11T21:09:02+01:00 | 6855ac2 | |
0ad6de8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 26 | 2019-12-11T20:55:19+01:00 | 7efa299 | |
3aca6bf | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 27 | 2019-12-11T20:44:26+01:00 | dfa0a8c | |
93ef2b2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 27 | 2019-12-08T00:27:24+01:00 | 7375bb9 | |
cc1659d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 27 | 2019-12-07T21:16:34+01:00 | 0f209da | |
14b00c6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 26 | 2019-12-06T02:43:11+01:00 | 553ba19 | |
52e61cd | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 27 | 2019-12-04T02:58:28+01:00 | ffd281f | |
cc8b1a3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 26 | 2019-12-03T08:57:12+01:00 | 0da2f68 | |
72aae60 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 27 | 2019-12-03T08:10:10+01:00 | dc08479 | |
dc08479 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / svcomp20 | 26 | 2019-11-30T13:23:23+01:00 | ||
c88de69 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco | 26 | 2019-12-01T07:35:06+01:00 | ||
0b96429 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 5 | 2019-12-08T01:52:20+01:00 | 3ec2881 | |
49f8115 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 5 | 2019-12-05T20:20:14+01:00 | ab97f32 | |
9d4b760 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2019-12-04T00:12 CET (comp) |
Found 26 witnesses for program sv-benchmarks/c/recursive-simple/id_i20_o20_false-unreach-call_true-termination.c, 21a977dc01fbb676ffbd104991f6d1e698de7db9cfedad64decaf2424e4fc66b
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/21a977dc01fbb676ffbd104991f6d1e698de7db9cfedad64decaf2424e4fc66b.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
1c93fc0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2018-12-08T03:53 CET (sv-comp) | ||
9cc2bdc | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | SMACK 1.9.3 | 4 | 2018-12-08T04:31:28 | ||
bd81da4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Pinaka | 14 | 2018-12-06T21:06 CET (sv-comp) | ||
e159bac | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 26 | 2018-12-06T20:24:14+01:00 | ||
8f02c97 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 26 | 2018-12-10T10:48:54+01:00 | 0e176e5 | |
92c4d29 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 27 | 2018-12-09T21:23:40+01:00 | 2a32cad | |
66d3f49 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 27 | 2018-12-09T20:53:13+01:00 | 9d366e5 | |
cd85550 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 27 | 2018-12-09T20:39:43+01:00 | 8368b19 | |
f09dadb | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 27 | 2018-12-09T20:30:20+01:00 | 022b8f2 | |
4bfeaf0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 27 | 2018-12-09T17:59:13+01:00 | 38a0181 | |
b6888d2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 26 | 2018-12-08T23:43:03+01:00 | 1c93fc0 | |
7f9677f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 26 | 2018-12-08T22:07:26+01:00 | 9cc2bdc | |
854721e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 27 | 2018-12-08T08:09:52+01:00 | e159bac | |
dc0f4e3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 26 | 2018-12-08T04:57:37+01:00 | 20f2438 | |
06ce3ee | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 26 | 2018-12-08T04:36:58+01:00 | 0e176e5 | |
7d2fade | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 26 | 2018-12-07T18:19:14+01:00 | 66ba1c1 | |
56329d6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 27 | 2018-12-07T17:45:40+01:00 | bd81da4 | |
6587214 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 26 | 2018-12-07T01:06:31+01:00 | 2781c40 | |
8dc8260 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 26 | 2018-12-06T10:20:12+01:00 | 0203a90 | |
037bd94 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 27 | 2018-12-06T09:48:57+01:00 | 64c2eb9 | |
11451b3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 27 | 2018-12-06T09:16:49+01:00 | 03b13ca | |
64c2eb9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 26 | 2018-12-06T07:23:56+01:00 | ||
a6821f7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-10T20:36:03+01:00 | 3e87a19 | |
765a1e8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-06T09:18:47+01:00 | 5795185 | |
e8533e7 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T09:08 CET (sv-comp) | ||
84922d2 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2018-12-07T11:13 CET (sv-comp) |
Found 20 witnesses for program sv-benchmarks/c/recursive-simple/id_i20_o20_false-unreach-call_true-termination.c, 21a977dc01fbb676ffbd104991f6d1e698de7db9cfedad64decaf2424e4fc66b
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/21a977dc01fbb676ffbd104991f6d1e698de7db9cfedad64decaf2424e4fc66b.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
4056d83 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | skink | 3 | 2017-12-01T22:26 CET (sv-comp) | ||
ae30f6d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | VeriAbs 1.3 | 16 | Sat Dec 2 20:12:26 2017 | ||
2a32cad | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | VIAP | 20 | 2017-12-03T03:48 CET (sv-comp) | ||
0348016 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Taipan | 21 | 2017-12-02T18:41Z | ||
5b558c2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2017-12-02T11:01 CET (sv-comp) | ||
c242f90 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Map2Check | 3 | 2017-12-01T21:15 CET (sv-comp) | ||
d919de4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Kojak | 21 | 2017-12-02T14:05Z | ||
b38715e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 kind | 4 | 2017-12-02T04:08:27.399540 | ||
8e4ee58 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 incr | 4 | 2017-12-01T19:26:15.673167 | ||
f33fb91 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 8 | 2017-12-01T16:05 CET (sv-comp) | ||
016276a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 8 | 2017-12-01T04:13 CET (sv-comp) | ||
6dd39ff | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 26 | 2017-11-30T16:07:42+01:00 | ||
6ac09cb | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26758M | 9 | 2017-11-30T14:44:43+01:00 | ||
4e76738 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26725 | 5 | 2017-12-01T00:18:17+01:00 | ||
b8d01b5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker (unknown version) | 6 | 2017-12-02T03:42:41+01:00 | ||
eedb775 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CBMC | 17 | 2017-11-30T22:57 CET (sv-comp) | ||
679f72a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Automizer | 21 | 2017-12-02T18:49Z | ||
e99537e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-03T01:27:22.746920 | ||
ba5872f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T09:00:56.045420 | ||
02a84e9 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 15 | 2017-12-01T19:14 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/recursive-simple/id_i20_o20_false-unreach-call_true-termination.c, 21a977dc01fbb676ffbd104991f6d1e698de7db9cfedad64decaf2424e4fc66b
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/21a977dc01fbb676ffbd104991f6d1e698de7db9cfedad64decaf2424e4fc66b.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |