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/Problem01_label20_false-unreach-call_false-termination.c |
programSHA | 51756b95c4564bf6b2b2ff8ddf134ab8f00d7df6c058f38cad219ddefa8349c4 |
witnessName | results-validated/cpa-seq-validate-violation-witnesses-cpa-seq.2018-12-06_0944.logfiles/sv-comp19_prop-termination.Problem01_label20_false-unreach-call_false-termination.c.files/witness.graphml |
witnessSHA | 8df57ffa5ae269b219ee551afdf11144d98cd755eff856dde879e20dd3741db8 |
Key | Value |
architecture | 32bit |
creationtime | 2018-12-06T09:49:03+01:00 |
producer | CPAchecker 1.7-svn 29852 |
program-sha256 | 51756b95c4564bf6b2b2ff8ddf134ab8f00d7df6c058f38cad219ddefa8349c4 |
programfile | ../../sv-benchmarks/c/eca-rers2012/Problem01_label20_false-unreach-call_false-termination.c |
programhash | 51756b95c4564bf6b2b2ff8ddf134ab8f00d7df6c058f38cad219ddefa8349c4 |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(F end) ) |
witness-file | witnessFileByHash/8df57ffa5ae269b219ee551afdf11144d98cd755eff856dde879e20dd3741db8.graphml |
witness-sha256 | 8df57ffa5ae269b219ee551afdf11144d98cd755eff856dde879e20dd3741db8 |
witness-size | 323851 |
witness-type | violation_witness |
This witness was created for this program (cf. table above, 51756b95c4564bf6b2b2ff8ddf134ab8f00d7df6c058f38cad219ddefa8349c4).
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem01_label20_false-unreach-call_false-termination.c, 51756b95c4564bf6b2b2ff8ddf134ab8f00d7df6c058f38cad219ddefa8349c4
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/51756b95c4564bf6b2b2ff8ddf134ab8f00d7df6c058f38cad219ddefa8349c4.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/Problem01_label20_false-unreach-call_false-termination.c, 51756b95c4564bf6b2b2ff8ddf134ab8f00d7df6c058f38cad219ddefa8349c4
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/51756b95c4564bf6b2b2ff8ddf134ab8f00d7df6c058f38cad219ddefa8349c4.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/Problem01_label20_false-unreach-call_false-termination.c, 51756b95c4564bf6b2b2ff8ddf134ab8f00d7df6c058f38cad219ddefa8349c4
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/51756b95c4564bf6b2b2ff8ddf134ab8f00d7df6c058f38cad219ddefa8349c4.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/Problem01_label20_false-unreach-call_false-termination.c, 51756b95c4564bf6b2b2ff8ddf134ab8f00d7df6c058f38cad219ddefa8349c4
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/51756b95c4564bf6b2b2ff8ddf134ab8f00d7df6c058f38cad219ddefa8349c4.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 18 witnesses for program sv-benchmarks/c/eca-rers2012/Problem01_label20_false-unreach-call_false-termination.c, 51756b95c4564bf6b2b2ff8ddf134ab8f00d7df6c058f38cad219ddefa8349c4
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/51756b95c4564bf6b2b2ff8ddf134ab8f00d7df6c058f38cad219ddefa8349c4.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
fc5874d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 2 | 2019-12-01 07:01:37 | ||
55dbd58 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Pinaka | 74 | 2019-12-03T22:24 CET (comp) | ||
ade9dfa | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 212 | 2019-12-11T21:42:40+01:00 | 4c04ac4 | |
eb75d5e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 212 | 2019-12-11T21:09:18+01:00 | fc5874d | |
0c8b2d7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 212 | 2019-12-11T20:54:28+01:00 | a399bb7 | |
95901fa | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 212 | 2019-12-11T20:44:40+01:00 | da56a8d | |
1f35f3b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 214 | 2019-12-08T01:52:17+01:00 | f24a3d2 | |
2787f17 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 263 | 2019-12-04T02:58:20+01:00 | 55dbd58 | |
b75231b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 212 | 2019-12-03T08:10:35+01:00 | d55606a | |
d55606a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / svcomp20 | 210 | 2019-11-30T01:18:39+01:00 | ||
4c04ac4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco | 212 | 2019-11-30T21:17:28+01:00 | ||
7a80b01 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 287 | 2019-12-11T21:44:22+01:00 | 0e8995e | |
3e9cc85 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 287 | 2019-12-08T00:27:19+01:00 | cba2cac | |
28860a4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 287 | 2019-12-07T21:19:32+01:00 | 78ac52a | |
60b2b50 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 287 | 2019-12-05T20:22:29+01:00 | 0d86277 | |
36580f9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 287 | 2019-12-05T19:35:46+01:00 | dcd766b | |
b9fb960 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.9 | 339 | 2019-11-29T17:53:02+01:00 | ||
f8b8e88 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 339 | 2019-12-01T09:20:32+01:00 |
Found 21 witnesses for program sv-benchmarks/c/eca-rers2012/Problem01_label20_false-unreach-call_false-termination.c, 51756b95c4564bf6b2b2ff8ddf134ab8f00d7df6c058f38cad219ddefa8349c4
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/51756b95c4564bf6b2b2ff8ddf134ab8f00d7df6c058f38cad219ddefa8349c4.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
12246a7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2018-12-08T03:44 CET (sv-comp) | ||
7d296a0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | SMACK 1.9.3 | 11 | 2018-12-08T11:42:39 | ||
f6b0365 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 212 | 2018-12-08T00:11:23+01:00 | ||
94cb418 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 214 | 2018-12-10T20:34:55+01:00 | 014f286 | |
bcef71c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 213 | 2018-12-09T18:20:53+01:00 | 83c8139 | |
657e00f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 216 | 2018-12-08T23:44:34+01:00 | 12246a7 | |
6e86a27 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 212 | 2018-12-08T22:10:35+01:00 | 7d296a0 | |
ca76340 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 212 | 2018-12-08T08:29:16+01:00 | f6b0365 | |
e32e3c8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 212 | 2018-12-08T05:05:00+01:00 | cc52e1b | |
79544ad | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 212 | 2018-12-06T10:14:06+01:00 | 1d480e0 | |
4e2940a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 212 | 2018-12-06T09:48:22+01:00 | d03a021 | |
7b91a41 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 293 | 2018-12-06T09:08:16+01:00 | 96c967a | |
d03a021 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 211 | 2018-12-05T10:18:04+01:00 | ||
91ecb0b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 287 | 2018-12-09T20:53:31+01:00 | 3196919 | |
c85dd78 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 287 | 2018-12-09T20:40:19+01:00 | cdaa7cd | |
a8d1309 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 287 | 2018-12-09T20:24:51+01:00 | 65eba64 | |
0169cea | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 287 | 2018-12-06T09:41:57+01:00 | a83a03f | |
775ca64 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 339 | 2018-12-07T00:58:54+01:00 | ||
c2cadf2 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn 29852 | 336 | 2018-12-08T07:59:28+01:00 | ||
8df57ff | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn 29852 | 324 | 2018-12-06T09:49:03+01:00 | ||
56117d6 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn 29852 | 327 | 2018-12-05T23:00:51+01:00 |
Found 14 witnesses for program sv-benchmarks/c/eca-rers2012/Problem01_label20_false-unreach-call_false-termination.c, 51756b95c4564bf6b2b2ff8ddf134ab8f00d7df6c058f38cad219ddefa8349c4
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/51756b95c4564bf6b2b2ff8ddf134ab8f00d7df6c058f38cad219ddefa8349c4.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
ac3a4db | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Veriabs | 4 | 2017-12-02T20:01 CET (sv-comp) | ||
344c9c9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2017-12-02T08:20 CET (sv-comp) | ||
7686c67 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Kojak | 188 | 2017-12-02T21:24Z | ||
8d255d5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 kind | 5 | 2017-12-01T20:44:43.021062 | ||
80033ae | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 incr | 5 | 2017-12-01T09:09:54.686804 | ||
e4023b7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 16 | 2017-12-01T18:58 CET (sv-comp) | ||
d2ef0f4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 16 | 2017-11-30T19:35 CET (sv-comp) | ||
d3768da | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 121 | 2017-11-30T23:44:55+01:00 | ||
b5d6f7c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26758M | 307 | 2017-11-30T22:36:14+01:00 | ||
2fd9e25 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26725 | 115 | 2017-11-30T14:54:45+01:00 | ||
81bcf90 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CBMC | 125 | 2017-11-30T15:17 CET (sv-comp) | ||
af2f48b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Automizer | 188 | 2017-12-02T02:18Z | ||
bfdd797 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | 2LS | 96 | 2017-11-30T14:43 CET (sv-comp) | ||
c460fcd | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | 2LS | 31 | 2017-12-01T12:24 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem01_label20_false-unreach-call_false-termination.c, 51756b95c4564bf6b2b2ff8ddf134ab8f00d7df6c058f38cad219ddefa8349c4
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/51756b95c4564bf6b2b2ff8ddf134ab8f00d7df6c058f38cad219ddefa8349c4.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |