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_label45_false-unreach-call_false-termination.c |
programSHA | bcfba7479b0ab905c2cabbf94a226fe4f8c8b7855211192be51a674b74972d6b |
witnessName | results-verified/depthk.2017-11-30_1601.logfiles/sv-comp18.Problem02_label45_false-unreach-call_false-termination.c.files/witness.graphml |
witnessSHA | 9ecac117376caaf68e4c092c6b92d25c324f2debc06ea472ee66bda72e5cf7b3 |
Key | Value |
architecture | 32bit |
creationtime | 2017-11-30T23:07 CET (sv-comp) |
memoryModel | precise |
producer | ESBMC 3.1 |
program-sha256 | bcfba7479b0ab905c2cabbf94a226fe4f8c8b7855211192be51a674b74972d6b |
programfile | /tmp/vcloud-vcloud-master/worker/working_dir_649d137d-104c-46c3-8985-cd544a35e374/sv-benchmarks/c/eca-rers2012/Problem02_label45_false-unreach-call_false-termination.c |
programhash | eadb33136c36588f3040fbda14d62db855361eef |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/9ecac117376caaf68e4c092c6b92d25c324f2debc06ea472ee66bda72e5cf7b3.graphml |
witness-sha256 | 9ecac117376caaf68e4c092c6b92d25c324f2debc06ea472ee66bda72e5cf7b3 |
witness-size | 10571 |
witness-type | violation_witness |
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem02_label45_false-unreach-call_false-termination.c, bcfba7479b0ab905c2cabbf94a226fe4f8c8b7855211192be51a674b74972d6b
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/bcfba7479b0ab905c2cabbf94a226fe4f8c8b7855211192be51a674b74972d6b.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_label45_false-unreach-call_false-termination.c, bcfba7479b0ab905c2cabbf94a226fe4f8c8b7855211192be51a674b74972d6b
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/bcfba7479b0ab905c2cabbf94a226fe4f8c8b7855211192be51a674b74972d6b.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_label45_false-unreach-call_false-termination.c, bcfba7479b0ab905c2cabbf94a226fe4f8c8b7855211192be51a674b74972d6b
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/bcfba7479b0ab905c2cabbf94a226fe4f8c8b7855211192be51a674b74972d6b.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_label45_false-unreach-call_false-termination.c, bcfba7479b0ab905c2cabbf94a226fe4f8c8b7855211192be51a674b74972d6b
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/bcfba7479b0ab905c2cabbf94a226fe4f8c8b7855211192be51a674b74972d6b.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_label45_false-unreach-call_false-termination.c, bcfba7479b0ab905c2cabbf94a226fe4f8c8b7855211192be51a674b74972d6b
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/bcfba7479b0ab905c2cabbf94a226fe4f8c8b7855211192be51a674b74972d6b.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
69403b3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 2 | 2019-12-01 23:22:00 | ||
f3ea91c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Pinaka | 56 | 2019-12-03T23:22 CET (comp) | ||
9f68987 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 174 | 2019-12-11T21:52:23+01:00 | 4f1d23a | |
ab68c28 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 174 | 2019-12-11T21:09:25+01:00 | 69403b3 | |
3e79208 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 231 | 2019-12-11T20:54:57+01:00 | bcbbd7f | |
26df7bb | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 174 | 2019-12-11T20:44:28+01:00 | f4f5dc2 | |
b9d6963 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 175 | 2019-12-08T01:51:34+01:00 | a684466 | |
bffcf41 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 221 | 2019-12-04T02:58:09+01:00 | f3ea91c | |
1430222 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 174 | 2019-12-03T08:10:37+01:00 | d56a932 | |
d56a932 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / svcomp20 | 173 | 2019-11-29T19:47:54+01:00 | ||
4f1d23a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco | 174 | 2019-12-01T02:03:50+01:00 | ||
96f022d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 280 | 2019-12-11T21:48:51+01:00 | 6193671 | |
8664e58 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 280 | 2019-12-08T00:28:25+01:00 | 48a8d40 | |
18e8c05 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 280 | 2019-12-07T21:19:25+01:00 | 63e29cb | |
64c7bb2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 280 | 2019-12-05T20:21:32+01:00 | cfae369 | |
2e6ae19 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 280 | 2019-12-05T19:35:20+01:00 | 9a73bba | |
f964169 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | Symbiotic | 2 | 2019-12-01 11:41:03 | ||
8f10be8 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.9 | 359 | 2019-11-30T08:10:38+01:00 | ||
3610e06 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 359 | 2019-12-01T00:36:30+01:00 |
Found 23 witnesses for program sv-benchmarks/c/eca-rers2012/Problem02_label45_false-unreach-call_false-termination.c, bcfba7479b0ab905c2cabbf94a226fe4f8c8b7855211192be51a674b74972d6b
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/bcfba7479b0ab905c2cabbf94a226fe4f8c8b7855211192be51a674b74972d6b.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
45a57fa | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2018-12-07T22:17 CET (sv-comp) | ||
546045c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | SMACK 1.9.3 | 7 | 2018-12-08T05:07:37 | ||
c6d1ea1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Pinaka | 65 | 2018-12-07T14:36 CET (sv-comp) | ||
ef42f20 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 174 | 2018-12-06T12:56:20+01:00 | ||
03461a3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 175 | 2018-12-10T20:34:51+01:00 | 3225786 | |
ce8a782 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 208 | 2018-12-09T18:21:34+01:00 | 75f7657 | |
db46ef9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 175 | 2018-12-08T23:44:07+01:00 | 45a57fa | |
3604469 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 174 | 2018-12-08T22:08:40+01:00 | 546045c | |
d28e316 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 174 | 2018-12-08T08:48:07+01:00 | ef42f20 | |
5a624d2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 232 | 2018-12-08T05:02:02+01:00 | 9308eba | |
eba9074 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 221 | 2018-12-07T17:44:50+01:00 | c6d1ea1 | |
96c527d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 174 | 2018-12-06T10:19:21+01:00 | 13a835e | |
8b2ab7f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 174 | 2018-12-06T09:48:08+01:00 | 0ac5026 | |
d8d2d31 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 229 | 2018-12-06T09:15:13+01:00 | 02530d2 | |
0ac5026 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 174 | 2018-12-05T19:30:01+01:00 | ||
d1855e9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 280 | 2018-12-09T20:53:19+01:00 | 1c6567c | |
00a3320 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 280 | 2018-12-09T20:40:16+01:00 | 21d7812 | |
37885e9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 280 | 2018-12-09T20:35:48+01:00 | 319b0d3 | |
b18fce5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 280 | 2018-12-06T09:42:08+01:00 | cc5ab1a | |
193699c | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 359 | 2018-12-08T01:05:26+01:00 | ||
f714265 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn 29852 | 356 | 2018-12-08T08:25:23+01:00 | ||
0b564f5 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn 29852 | 356 | 2018-12-06T09:48:05+01:00 | ||
be36ebe | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn 29852 | 359 | 2018-12-05T05:58:20+01:00 |
Found 16 witnesses for program sv-benchmarks/c/eca-rers2012/Problem02_label45_false-unreach-call_false-termination.c, bcfba7479b0ab905c2cabbf94a226fe4f8c8b7855211192be51a674b74972d6b
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/bcfba7479b0ab905c2cabbf94a226fe4f8c8b7855211192be51a674b74972d6b.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
cab93d4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Veriabs | 3 | 2017-12-02T22:50 CET (sv-comp) | ||
f6e875f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Taipan | 140 | 2017-12-03T03:23Z | ||
811067a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2017-12-02T08:23 CET (sv-comp) | ||
2d03f6c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Kojak | 140 | 2017-12-02T02:48Z | ||
1dfa9f0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 kind | 4 | 2017-12-01T21:41:39.325433 | ||
a664a03 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 incr | 5 | 2017-12-01T08:24:33.054255 | ||
09d217b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 11 | 2017-12-01T16:53 CET (sv-comp) | ||
9ecac11 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 11 | 2017-11-30T23:07 CET (sv-comp) | ||
15eb832 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 100 | 2017-12-01T00:37:59+01:00 | ||
9f949b5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26758M | 246 | 2017-11-30T13:30:09+01:00 | ||
b8f86ca | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CBMC | 72 | 2017-11-30T21:11 CET (sv-comp) | ||
81fce28 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Automizer | 140 | 2017-12-02T16:13Z | ||
4df0a6f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | 2LS | 73 | 2017-12-01T00:02 CET (sv-comp) | ||
2722214 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 334 | 2017-12-01T15:01:55+01:00 | ||
8a956e2 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | Automizer | 15 | 2017-12-03T11:12Z | ||
5dee5f0 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | 2LS | 26 | 2017-12-01T12:56 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem02_label45_false-unreach-call_false-termination.c, bcfba7479b0ab905c2cabbf94a226fe4f8c8b7855211192be51a674b74972d6b
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/bcfba7479b0ab905c2cabbf94a226fe4f8c8b7855211192be51a674b74972d6b.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |