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_label19_true-unreach-call_false-termination.c |
programSHA | f3201e5dc6eb947acfd1bc970970110bfba79e0c6639049c3a2d0126fea4b2f4 |
witnessName | results-verified/pesco.2018-12-06_1244.logfiles/sv-comp19_prop-termination.Problem02_label19_true-unreach-call_false-termination.c.files/witness.graphml |
witnessSHA | 420962faba7998afb562c8c777ee3fb84a9101f9b31271633792113814a0ba28 |
Key | Value |
architecture | 32bit |
creationtime | 2018-12-07T14:41:47+01:00 |
producer | CPAchecker 1.7-svn b8d6131600+ |
program-sha256 | f3201e5dc6eb947acfd1bc970970110bfba79e0c6639049c3a2d0126fea4b2f4 |
programfile | ../../sv-benchmarks/c/eca-rers2012/Problem02_label19_true-unreach-call_false-termination.c |
programhash | f3201e5dc6eb947acfd1bc970970110bfba79e0c6639049c3a2d0126fea4b2f4 |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(F end) ) |
witness-file | witnessFileByHash/420962faba7998afb562c8c777ee3fb84a9101f9b31271633792113814a0ba28.graphml |
witness-sha256 | 420962faba7998afb562c8c777ee3fb84a9101f9b31271633792113814a0ba28 |
witness-size | 359160 |
witness-type | violation_witness |
This witness was created for this program (cf. table above, f3201e5dc6eb947acfd1bc970970110bfba79e0c6639049c3a2d0126fea4b2f4).
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem02_label19_true-unreach-call_false-termination.c, f3201e5dc6eb947acfd1bc970970110bfba79e0c6639049c3a2d0126fea4b2f4
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/f3201e5dc6eb947acfd1bc970970110bfba79e0c6639049c3a2d0126fea4b2f4.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_label19_true-unreach-call_false-termination.c, f3201e5dc6eb947acfd1bc970970110bfba79e0c6639049c3a2d0126fea4b2f4
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/f3201e5dc6eb947acfd1bc970970110bfba79e0c6639049c3a2d0126fea4b2f4.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_label19_true-unreach-call_false-termination.c, f3201e5dc6eb947acfd1bc970970110bfba79e0c6639049c3a2d0126fea4b2f4
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/f3201e5dc6eb947acfd1bc970970110bfba79e0c6639049c3a2d0126fea4b2f4.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_label19_true-unreach-call_false-termination.c, f3201e5dc6eb947acfd1bc970970110bfba79e0c6639049c3a2d0126fea4b2f4
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/f3201e5dc6eb947acfd1bc970970110bfba79e0c6639049c3a2d0126fea4b2f4.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_label19_true-unreach-call_false-termination.c, f3201e5dc6eb947acfd1bc970970110bfba79e0c6639049c3a2d0126fea4b2f4
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/f3201e5dc6eb947acfd1bc970970110bfba79e0c6639049c3a2d0126fea4b2f4.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
299c16e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 280 | 2019-12-11T20:31:01+01:00 | f315495 | |
7cba647 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 280 | 2019-12-11T20:08:15+01:00 | 292fd47 | |
ebd1cf0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 280 | 2019-12-11T20:02:21+01:00 | f1dcaa0 | |
38e82d4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 280 | 2019-12-08T00:47:08+01:00 | 4d3294c | |
f9f5bfe | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 280 | 2019-12-07T23:38:48+01:00 | 0342a9a | |
153d4ec | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 280 | 2019-12-07T19:46:25+01:00 | 2b83dfa | |
9215772 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 280 | 2019-12-05T19:02:56+01:00 | 784453e | |
c7d3443 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 280 | 2019-11-30T16:25:04+01:00 | 976665a | |
976665a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / svcomp20 | 280 | 2019-11-29T18:17:14+01:00 | ||
292fd47 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco | 280 | 2019-11-30T23:37:48+01:00 | ||
2cc3daf | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | Symbiotic | 2 | 2019-12-01 18:12:34 | ||
71e7fc1 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.9 | 359 | 2019-11-29T23:01:22+01:00 | ||
81d764d | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 359 | 2019-11-30T23:32:28+01:00 |
Found 17 witnesses for program sv-benchmarks/c/eca-rers2012/Problem02_label19_true-unreach-call_false-termination.c, f3201e5dc6eb947acfd1bc970970110bfba79e0c6639049c3a2d0126fea4b2f4
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/f3201e5dc6eb947acfd1bc970970110bfba79e0c6639049c3a2d0126fea4b2f4.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
42e386f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | SMACK 1.9.3 | 3 | 2018-12-08T17:13:00 | ||
d1f3f9a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 280 | 2018-12-07T10:07:30+01:00 | ||
e73106a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 280 | 2018-12-10T20:09:51+01:00 | a82adca | |
17ac4a4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 280 | 2018-12-09T20:29:46+01:00 | 7f41d6d | |
3a540ce | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 280 | 2018-12-09T20:11:38+01:00 | 49b9553 | |
64ada37 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 280 | 2018-12-09T19:41:21+01:00 | 7014577 | |
8c3a767 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 280 | 2018-12-08T21:01:39+01:00 | 42e386f | |
e7bea3c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 280 | 2018-12-08T07:02:11+01:00 | d1f3f9a | |
8c7c66f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 280 | 2018-12-08T03:56:10+01:00 | e92f570 | |
ea0eaae | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 280 | 2018-12-06T09:28:23+01:00 | edb5af5 | |
fd4dd63 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 280 | 2018-12-06T08:53:39+01:00 | b7ac619 | |
34ce605 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 280 | 2018-12-06T07:27:56+01:00 | 3f7150a | |
b7ac619 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 280 | 2018-12-06T03:18:00+01:00 | ||
420962f | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 359 | 2018-12-07T14:41:47+01:00 | ||
fd107ca | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn 29852 | 356 | 2018-12-08T08:53:19+01:00 | ||
c4cac32 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn 29852 | 356 | 2018-12-06T09:48:02+01:00 | ||
0d3ba6d | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn 29852 | 359 | 2018-12-05T15:29:55+01:00 |
Found 19 witnesses for program sv-benchmarks/c/eca-rers2012/Problem02_label19_true-unreach-call_false-termination.c, f3201e5dc6eb947acfd1bc970970110bfba79e0c6639049c3a2d0126fea4b2f4
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/f3201e5dc6eb947acfd1bc970970110bfba79e0c6639049c3a2d0126fea4b2f4.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
4845a49 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Kojak | 184 | 2017-12-02T17:04Z | ||
febff7b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.12-svcomp17 | 4 | 2017-11-02T13:16:17+05:30 | ||
4d0eaae | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 280 | 2017-12-03T04:09:52+01:00 | a112463 | |
a6ec228 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 291 | 2017-12-03T01:19:14+01:00 | cffeb3e | |
34e623a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 280 | 2017-12-03T00:08:21+01:00 | 2e673eb | |
f7650ac | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 280 | 2017-12-02T14:58:15+01:00 | a8bedd8 | |
ba3c1a3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 280 | 2017-12-01T07:02:36+01:00 | 1966317 | |
76ae208 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 280 | 2017-12-01T06:18:33+01:00 | 0bbd6db | |
5f024c1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 280 | 2017-12-01T05:51:40+01:00 | 909da20 | |
7847657 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 280 | 2017-12-01T04:25:16+01:00 | 066f42f | |
0a00431 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 280 | 2017-11-30T11:25:57+01:00 | ||
8d47c15 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26758M | 319 | 2017-11-30T20:27:13+01:00 | ||
4688c11 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26725 | 280 | 2017-11-30T12:44:33+01:00 | ||
221df89 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker (unknown version) | 411 | 2017-12-02T02:53:25+01:00 | ||
5847434 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Automizer | 161 | 2017-12-02T02:45Z | ||
6510de2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | 2LS | 811 | 2017-12-01T00:46 CET (sv-comp) | ||
4326f08 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 334 | 2017-12-01T14:15:46+01:00 | ||
36ab77f | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | Automizer | 15 | 2017-12-03T11:14Z | ||
c4ce827 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | 2LS | 26 | 2017-12-01T15:48 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem02_label19_true-unreach-call_false-termination.c, f3201e5dc6eb947acfd1bc970970110bfba79e0c6639049c3a2d0126fea4b2f4
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/f3201e5dc6eb947acfd1bc970970110bfba79e0c6639049c3a2d0126fea4b2f4.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |