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_label35_true-unreach-call_false-termination.c |
programSHA | 5168fcf0a20c38c01d513f5bdf8afc888a4b7c7ef433970b5482deca87fef687 |
witnessName | results-verified/uautomizer.2017-12-03_1212.logfiles/sv-comp18.Problem02_label35_true-unreach-call_false-termination.c.files/witness.graphml |
witnessSHA | 10d9ce551025f065d25aea268f3d5e6c0472b8254fd1a02e6719504f46c65b41 |
Key | Value |
architecture | 32bit |
creationtime | 2017-12-03T11:14Z |
producer | Automizer |
program-sha256 | 5168fcf0a20c38c01d513f5bdf8afc888a4b7c7ef433970b5482deca87fef687 |
programfile | /tmp/vcloud-vcloud-master/worker/working_dir_920be461-f7dc-4395-ae2f-acb32ef3c6d4/sv-benchmarks/c/eca-rers2012/Problem02_label35_true-unreach-call_false-termination.c |
programhash | f6b5db140f0af5d4dbaefce619ea0ad631629d04 |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(F end) ) |
witness-file | witnessFileByHash/10d9ce551025f065d25aea268f3d5e6c0472b8254fd1a02e6719504f46c65b41.graphml |
witness-sha256 | 10d9ce551025f065d25aea268f3d5e6c0472b8254fd1a02e6719504f46c65b41 |
witness-size | 15163 |
witness-type | violation_witness |
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem02_label35_true-unreach-call_false-termination.c, 5168fcf0a20c38c01d513f5bdf8afc888a4b7c7ef433970b5482deca87fef687
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/5168fcf0a20c38c01d513f5bdf8afc888a4b7c7ef433970b5482deca87fef687.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_label35_true-unreach-call_false-termination.c, 5168fcf0a20c38c01d513f5bdf8afc888a4b7c7ef433970b5482deca87fef687
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/5168fcf0a20c38c01d513f5bdf8afc888a4b7c7ef433970b5482deca87fef687.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_label35_true-unreach-call_false-termination.c, 5168fcf0a20c38c01d513f5bdf8afc888a4b7c7ef433970b5482deca87fef687
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/5168fcf0a20c38c01d513f5bdf8afc888a4b7c7ef433970b5482deca87fef687.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_label35_true-unreach-call_false-termination.c, 5168fcf0a20c38c01d513f5bdf8afc888a4b7c7ef433970b5482deca87fef687
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/5168fcf0a20c38c01d513f5bdf8afc888a4b7c7ef433970b5482deca87fef687.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 13 witnesses for program sv-benchmarks/c/eca-rers2012/Problem02_label35_true-unreach-call_false-termination.c, 5168fcf0a20c38c01d513f5bdf8afc888a4b7c7ef433970b5482deca87fef687
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/5168fcf0a20c38c01d513f5bdf8afc888a4b7c7ef433970b5482deca87fef687.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
d298808 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 280 | 2019-12-11T20:31:05+01:00 | 520e79d | |
5a6aed8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 280 | 2019-12-11T20:15:22+01:00 | 4e4b782 | |
9d179de | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 280 | 2019-12-11T20:02:39+01:00 | a3a0782 | |
8a0fac7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 280 | 2019-12-08T00:59:35+01:00 | c30d9a0 | |
3263e86 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 280 | 2019-12-07T23:31:24+01:00 | 9d71b23 | |
2067658 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 280 | 2019-12-07T19:45:43+01:00 | d4dd333 | |
427ef14 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 280 | 2019-12-05T19:02:56+01:00 | 6c85140 | |
335b6b4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 280 | 2019-11-30T16:11:23+01:00 | 068cb92 | |
068cb92 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / svcomp20 | 280 | 2019-11-30T06:26:58+01:00 | ||
4e4b782 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco | 280 | 2019-12-01T13:04:17+01:00 | ||
0570456 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | Symbiotic | 2 | 2019-12-01 01:25:39 | ||
52113fa | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.9 | 359 | 2019-11-29T16:34:05+01:00 | ||
70114a1 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 359 | 2019-12-01T01:28:32+01:00 |
Found 17 witnesses for program sv-benchmarks/c/eca-rers2012/Problem02_label35_true-unreach-call_false-termination.c, 5168fcf0a20c38c01d513f5bdf8afc888a4b7c7ef433970b5482deca87fef687
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/5168fcf0a20c38c01d513f5bdf8afc888a4b7c7ef433970b5482deca87fef687.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
3b44968 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | SMACK 1.9.3 | 3 | 2018-12-08T01:37:54 | ||
5dd6ed4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 280 | 2018-12-07T10:21:21+01:00 | ||
6bb4ba1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 280 | 2018-12-10T20:16:57+01:00 | 1fe8998 | |
88ecece | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 280 | 2018-12-09T20:32:52+01:00 | 9a9f950 | |
821d83b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 280 | 2018-12-09T20:04:01+01:00 | 7cb3928 | |
1163f28 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 280 | 2018-12-09T19:53:28+01:00 | 934acc2 | |
ba5d337 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 280 | 2018-12-08T21:34:40+01:00 | 3b44968 | |
e2d0731 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 280 | 2018-12-08T05:40:11+01:00 | 5dd6ed4 | |
af44fd1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 280 | 2018-12-08T03:02:50+01:00 | 4cd1072 | |
5123e83 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 280 | 2018-12-06T09:28:20+01:00 | 43a391b | |
69db030 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 280 | 2018-12-06T09:00:16+01:00 | d1cc172 | |
045dc92 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 280 | 2018-12-06T08:22:50+01:00 | 6ca474a | |
d1cc172 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 280 | 2018-12-05T05:56:37+01:00 | ||
c936c4d | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 359 | 2018-12-06T13:29:48+01:00 | ||
f229773 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn 29852 | 356 | 2018-12-08T09:02:22+01:00 | ||
b6da9c8 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn 29852 | 356 | 2018-12-06T09:49:13+01:00 | ||
9380104 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn 29852 | 359 | 2018-12-06T05:24:04+01:00 |
Found 19 witnesses for program sv-benchmarks/c/eca-rers2012/Problem02_label35_true-unreach-call_false-termination.c, 5168fcf0a20c38c01d513f5bdf8afc888a4b7c7ef433970b5482deca87fef687
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/5168fcf0a20c38c01d513f5bdf8afc888a4b7c7ef433970b5482deca87fef687.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
596642c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Kojak | 180 | 2017-12-02T13:33Z | ||
4c9fd88 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.12-svcomp17 | 4 | 2017-11-02T13:16:17+05:30 | ||
7a6840f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 280 | 2017-12-03T04:05:34+01:00 | e48a3c4 | |
c5c61bd | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 287 | 2017-12-03T02:02:15+01:00 | afac18c | |
39a58e9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 280 | 2017-12-02T23:51:17+01:00 | 26a207a | |
3dda2de | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 280 | 2017-12-02T14:56:55+01:00 | cadcf32 | |
1e13dc6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 280 | 2017-12-01T07:12:49+01:00 | c7ac5f1 | |
3ab869c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 280 | 2017-12-01T06:33:33+01:00 | 4496d81 | |
9f3c8cc | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 280 | 2017-12-01T05:31:45+01:00 | 04a6c57 | |
0523c60 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 280 | 2017-12-01T04:46:33+01:00 | ab03db3 | |
8c1043d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 280 | 2017-11-30T18:17:07+01:00 | ||
4e8e8ff | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26758M | 319 | 2017-11-30T15:09:29+01:00 | ||
86b7d1e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26725 | 280 | 2017-12-01T03:03:19+01:00 | ||
9f7ce4d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker (unknown version) | 447 | 2017-12-01T23:03:53+01:00 | ||
e7661cc | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Automizer | 161 | 2017-12-02T18:59Z | ||
bc9fd4a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | 2LS | 811 | 2017-11-30T13:33 CET (sv-comp) | ||
89fc908 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 334 | 2017-12-01T15:50:01+01:00 | ||
10d9ce5 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | Automizer | 15 | 2017-12-03T11:14Z | ||
e8d6b98 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | 2LS | 26 | 2017-12-01T11:43 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem02_label35_true-unreach-call_false-termination.c, 5168fcf0a20c38c01d513f5bdf8afc888a4b7c7ef433970b5482deca87fef687
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/5168fcf0a20c38c01d513f5bdf8afc888a4b7c7ef433970b5482deca87fef687.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |