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_label44_false-unreach-call_false-termination.c |
programSHA | a5330d743ce0709e95121dad266db295edf58fa3750f286cdfc9738ce4648a96 |
witnessName | results-validated/cpa-seq-validate-violation-witnesses-pesco.2018-12-08_0739.logfiles/sv-comp19_prop-reachsafety.Problem02_label44_false-unreach-call_false-termination.c.files/witness.graphml |
witnessSHA | 7ac29f05d6e0968975ebbc817d9a454de1d6d7e15fc269283f5e7f2e0041ccc2 |
Key | Value |
architecture | 32bit |
creationtime | 2018-12-08T08:12:54+01:00 |
inputwitnesshash | a5e65b4b838de917259885ba37bfb1eea7355746c4f4409c90ae873cd857f5cb |
producer | CPAchecker 1.7-svn 29852 |
program-sha256 | a5330d743ce0709e95121dad266db295edf58fa3750f286cdfc9738ce4648a96 |
programfile | ../../sv-benchmarks/c/eca-rers2012/Problem02_label44_false-unreach-call_false-termination.c |
programhash | a5330d743ce0709e95121dad266db295edf58fa3750f286cdfc9738ce4648a96 |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/7ac29f05d6e0968975ebbc817d9a454de1d6d7e15fc269283f5e7f2e0041ccc2.graphml |
witness-sha256 | 7ac29f05d6e0968975ebbc817d9a454de1d6d7e15fc269283f5e7f2e0041ccc2 |
witness-size | 121643 |
witness-type | violation_witness |
This witness was created for this program (cf. table above, a5330d743ce0709e95121dad266db295edf58fa3750f286cdfc9738ce4648a96).
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem02_label44_false-unreach-call_false-termination.c, a5330d743ce0709e95121dad266db295edf58fa3750f286cdfc9738ce4648a96
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/a5330d743ce0709e95121dad266db295edf58fa3750f286cdfc9738ce4648a96.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_label44_false-unreach-call_false-termination.c, a5330d743ce0709e95121dad266db295edf58fa3750f286cdfc9738ce4648a96
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/a5330d743ce0709e95121dad266db295edf58fa3750f286cdfc9738ce4648a96.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_label44_false-unreach-call_false-termination.c, a5330d743ce0709e95121dad266db295edf58fa3750f286cdfc9738ce4648a96
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/a5330d743ce0709e95121dad266db295edf58fa3750f286cdfc9738ce4648a96.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_label44_false-unreach-call_false-termination.c, a5330d743ce0709e95121dad266db295edf58fa3750f286cdfc9738ce4648a96
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/a5330d743ce0709e95121dad266db295edf58fa3750f286cdfc9738ce4648a96.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_label44_false-unreach-call_false-termination.c, a5330d743ce0709e95121dad266db295edf58fa3750f286cdfc9738ce4648a96
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/a5330d743ce0709e95121dad266db295edf58fa3750f286cdfc9738ce4648a96.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
69b88cf | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2019-12-01 21:10:01 | ||
f6d8755 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Pinaka | 41 | 2019-12-04T00:55 CET (comp) | ||
38e034d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 122 | 2019-12-11T21:58:46+01:00 | 38100be | |
efe3b6c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 122 | 2019-12-11T21:09:44+01:00 | 69b88cf | |
1d818c2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 122 | 2019-12-11T20:54:55+01:00 | 271e3fa | |
a402a55 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 122 | 2019-12-11T20:44:26+01:00 | 2f41064 | |
4ad9152 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 122 | 2019-12-08T01:51:36+01:00 | d933cb0 | |
97ad575 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 152 | 2019-12-04T02:58:03+01:00 | f6d8755 | |
89bcb48 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 122 | 2019-12-03T08:03:30+01:00 | 08b5926 | |
08b5926 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / svcomp20 | 121 | 2019-11-30T00:15:52+01:00 | ||
38100be | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco | 122 | 2019-12-01T09:21:22+01:00 | ||
1fc78c5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 280 | 2019-12-11T21:44:02+01:00 | 60ae2be | |
40061b2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 280 | 2019-12-08T00:37:24+01:00 | ada092c | |
adbec83 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 280 | 2019-12-07T21:15:27+01:00 | 27a7973 | |
88094a8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 280 | 2019-12-05T20:21:44+01:00 | b411547 | |
7c676e0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 280 | 2019-12-05T19:35:18+01:00 | 38adc37 | |
9845683 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | Symbiotic | 2 | 2019-12-02 00:19:13 | ||
22f3de0 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.9 | 359 | 2019-11-29T15:28:12+01:00 | ||
918c9d7 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 359 | 2019-12-01T00:13:51+01:00 |
Found 23 witnesses for program sv-benchmarks/c/eca-rers2012/Problem02_label44_false-unreach-call_false-termination.c, a5330d743ce0709e95121dad266db295edf58fa3750f286cdfc9738ce4648a96
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/a5330d743ce0709e95121dad266db295edf58fa3750f286cdfc9738ce4648a96.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
f59fd5b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2018-12-08T09:51 CET (sv-comp) | ||
7cad77d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | SMACK 1.9.3 | 6 | 2018-12-08T03:30:23 | ||
5f87f87 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Pinaka | 47 | 2018-12-07T06:05 CET (sv-comp) | ||
a5e65b4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 122 | 2018-12-07T05:18:36+01:00 | ||
dcea823 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 122 | 2018-12-10T20:37:36+01:00 | 61ef255 | |
eaf86d1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 122 | 2018-12-09T17:52:59+01:00 | 192a8bc | |
73c08ae | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 122 | 2018-12-08T23:44:08+01:00 | f59fd5b | |
b7d6931 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 122 | 2018-12-08T22:09:03+01:00 | 7cad77d | |
7ac29f0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 122 | 2018-12-08T08:12:54+01:00 | a5e65b4 | |
4f2cabf | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 122 | 2018-12-08T05:06:28+01:00 | d432074 | |
2dfa16e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 152 | 2018-12-07T17:43:24+01:00 | 5f87f87 | |
2e61e28 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 122 | 2018-12-06T10:09:56+01:00 | 688343f | |
c6e0153 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 122 | 2018-12-06T09:49:03+01:00 | 6768bfc | |
b5e5dbe | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 380 | 2018-12-06T09:18:49+01:00 | de159ef | |
6768bfc | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 121 | 2018-12-05T06:07:26+01:00 | ||
aadd022 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 280 | 2018-12-09T20:53:17+01:00 | 579373f | |
1baade2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 280 | 2018-12-09T20:37:25+01:00 | 287ca03 | |
fb4450a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 280 | 2018-12-09T20:33:17+01:00 | eeac21b | |
f4f7172 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 280 | 2018-12-06T09:43:41+01:00 | d892c73 | |
809076f | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 359 | 2018-12-07T15:56:28+01:00 | ||
0d64d44 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn 29852 | 356 | 2018-12-08T08:14:25+01:00 | ||
b936d0f | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn 29852 | 356 | 2018-12-06T09:48:10+01:00 | ||
9f7a6ac | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn 29852 | 359 | 2018-12-05T14:00:15+01:00 |
Found 18 witnesses for program sv-benchmarks/c/eca-rers2012/Problem02_label44_false-unreach-call_false-termination.c, a5330d743ce0709e95121dad266db295edf58fa3750f286cdfc9738ce4648a96
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/a5330d743ce0709e95121dad266db295edf58fa3750f286cdfc9738ce4648a96.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
21e7bea | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Veriabs | 3 | 2017-12-03T01:27 CET (sv-comp) | ||
61d422f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Taipan | 100 | 2017-12-03T04:29Z | ||
2743384 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2017-12-02T09:39 CET (sv-comp) | ||
0ef12c1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Kojak | 100 | 2017-12-02T01:48Z | ||
7493d39 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 kind | 4 | 2017-12-01T21:55:14.201896 | ||
d588fd3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 incr | 4 | 2017-12-01T09:23:16.701284 | ||
4cb03c8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 9 | 2017-12-01T20:48 CET (sv-comp) | ||
d0f688e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 9 | 2017-11-30T21:48 CET (sv-comp) | ||
06a69b8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 70 | 2017-11-30T17:21:46+01:00 | ||
41bfe73 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26758M | 168 | 2017-11-30T17:53:42+01:00 | ||
ee73865 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26725 | 82 | 2017-11-30T18:04:20+01:00 | ||
48cf9f9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker (unknown version) | 103 | 2017-12-02T13:06:47+01:00 | ||
abe26ac | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CBMC | 85 | 2017-11-30T13:22 CET (sv-comp) | ||
9c08cd3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Automizer | 100 | 2017-12-02T07:32Z | ||
88a43ae | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | 2LS | 52 | 2017-11-30T12:29 CET (sv-comp) | ||
d3385f6 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 334 | 2017-12-01T14:38:49+01:00 | ||
defc998 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | Automizer | 15 | 2017-12-03T11:12Z | ||
60e2e7e | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | 2LS | 26 | 2017-12-01T12:42 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem02_label44_false-unreach-call_false-termination.c, a5330d743ce0709e95121dad266db295edf58fa3750f286cdfc9738ce4648a96
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/a5330d743ce0709e95121dad266db295edf58fa3750f286cdfc9738ce4648a96.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |