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/product-lines/email_spec11_product33_false-unreach-call_true-termination.cil.c |
programSHA | b0849ccdd25b96758e6baa1979ff203e43704a5e97b2374ea16fb14f8fcb5d1d |
witnessName | results-verified/symbiotic.2018-12-07_2142.logfiles/sv-comp19_prop-reachsafety.email_spec11_product33_false-unreach-call_true-termination.cil.c.files/witness.graphml |
witnessSHA | af05302a0e32e7245b8cce44a3c372e4ebc3e6dd38e0f7590aabe9d77a4047b3 |
Key | Value |
architecture | 32bit |
creationtime | 2018-12-08T16:16 CET (sv-comp) |
producer | Symbiotic |
program-sha256 | b0849ccdd25b96758e6baa1979ff203e43704a5e97b2374ea16fb14f8fcb5d1d |
programfile | /tmp/vcloud-vcloud-master/worker/working_dir_47a385e3-732c-48ca-b6f1-5499cdb9ae2a/sv-benchmarks/c/product-lines/email_spec11_product33_false-unreach-call_true-termination.cil.c |
programhash | b0849ccdd25b96758e6baa1979ff203e43704a5e97b2374ea16fb14f8fcb5d1d |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/af05302a0e32e7245b8cce44a3c372e4ebc3e6dd38e0f7590aabe9d77a4047b3.graphml |
witness-sha256 | af05302a0e32e7245b8cce44a3c372e4ebc3e6dd38e0f7590aabe9d77a4047b3 |
witness-size | 840 |
witness-type | violation_witness |
This witness was created for this program (cf. table above, b0849ccdd25b96758e6baa1979ff203e43704a5e97b2374ea16fb14f8fcb5d1d).
Found 0 witnesses for program sv-benchmarks/c/product-lines/email_spec11_product33_false-unreach-call_true-termination.cil.c, b0849ccdd25b96758e6baa1979ff203e43704a5e97b2374ea16fb14f8fcb5d1d
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/b0849ccdd25b96758e6baa1979ff203e43704a5e97b2374ea16fb14f8fcb5d1d.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/product-lines/email_spec11_product33_false-unreach-call_true-termination.cil.c, b0849ccdd25b96758e6baa1979ff203e43704a5e97b2374ea16fb14f8fcb5d1d
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/b0849ccdd25b96758e6baa1979ff203e43704a5e97b2374ea16fb14f8fcb5d1d.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/product-lines/email_spec11_product33_false-unreach-call_true-termination.cil.c, b0849ccdd25b96758e6baa1979ff203e43704a5e97b2374ea16fb14f8fcb5d1d
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/b0849ccdd25b96758e6baa1979ff203e43704a5e97b2374ea16fb14f8fcb5d1d.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/product-lines/email_spec11_product33_false-unreach-call_true-termination.cil.c, b0849ccdd25b96758e6baa1979ff203e43704a5e97b2374ea16fb14f8fcb5d1d
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/b0849ccdd25b96758e6baa1979ff203e43704a5e97b2374ea16fb14f8fcb5d1d.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 13 witnesses for program sv-benchmarks/c/product-lines/email_spec11_product33_false-unreach-call_true-termination.cil.c, b0849ccdd25b96758e6baa1979ff203e43704a5e97b2374ea16fb14f8fcb5d1d
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/b0849ccdd25b96758e6baa1979ff203e43704a5e97b2374ea16fb14f8fcb5d1d.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
18d456e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 2 | 2019-12-01 05:29:47 | ||
17d1eab | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 137 | 2019-12-11T21:55:56+01:00 | 54715c7 | |
011ba4a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 128 | 2019-12-11T21:09:34+01:00 | 18d456e | |
169bb3a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 156 | 2019-12-11T20:54:48+01:00 | bc7ee23 | |
e77609b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 128 | 2019-12-11T20:44:35+01:00 | 6a8505d | |
de0fff1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 126 | 2019-12-08T01:51:50+01:00 | 3b98cb5 | |
8ed94ac | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 128 | 2019-12-03T08:56:52+01:00 | b7cedd5 | |
b399d93 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 125 | 2019-12-03T08:10:07+01:00 | a4dd658 | |
a4dd658 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / svcomp20 | 118 | 2019-11-30T02:05:22+01:00 | ||
3b98cb5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.8 | 128 | 2019-12-07T14:09:00+01:00 | ||
54715c7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco | 137 | 2019-12-01T00:19:28+01:00 | ||
15f3fd3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 182 | 2019-12-05T20:20:36+01:00 | ff7cbe0 | |
edcac0b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 182 | 2019-12-05T19:34:36+01:00 | 0c390c2 |
Found 19 witnesses for program sv-benchmarks/c/product-lines/email_spec11_product33_false-unreach-call_true-termination.cil.c, b0849ccdd25b96758e6baa1979ff203e43704a5e97b2374ea16fb14f8fcb5d1d
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/b0849ccdd25b96758e6baa1979ff203e43704a5e97b2374ea16fb14f8fcb5d1d.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
af05302 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2018-12-08T16:16 CET (sv-comp) | ||
0b3d54d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | SMACK 1.9.3 | 23 | 2018-12-08T05:45:26 | ||
bdb907c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Pinaka | 89 | 2018-12-07T13:51 CET (sv-comp) | ||
1d17f08 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7 | 121 | 2018-12-10T18:03:01+01:00 | ||
dbef947 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 140 | 2018-12-08T04:37:04+01:00 | ||
41a7717 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 126 | 2018-12-10T20:35:59+01:00 | 1d17f08 | |
4c8aba4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 128 | 2018-12-09T18:21:39+01:00 | 908efa8 | |
bb30b21 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 128 | 2018-12-08T23:42:55+01:00 | af05302 | |
d515bf5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 91 | 2018-12-08T22:07:26+01:00 | 0b3d54d | |
53cd114 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 137 | 2018-12-08T07:52:08+01:00 | dbef947 | |
8a87171 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 134 | 2018-12-08T04:55:20+01:00 | 8798842 | |
60ad830 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 128 | 2018-12-07T17:42:59+01:00 | bdb907c | |
5305e5f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 137 | 2018-12-06T10:19:28+01:00 | d8cd578 | |
b993043 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 125 | 2018-12-06T09:48:06+01:00 | 4aa8e6d | |
4aa8e6d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 118 | 2018-12-06T04:04:10+01:00 | ||
0483a35 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 182 | 2018-12-06T09:42:21+01:00 | 5701435 | |
3cc6e43 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 181 | 2018-12-06T09:16:47+01:00 | 9e0b73a | |
2abc186 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 181 | 2018-12-06T09:12:18+01:00 | 4fa018c | |
5fef8b8 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T19:25 CET (sv-comp) |
Found 12 witnesses for program sv-benchmarks/c/product-lines/email_spec11_product33_false-unreach-call_true-termination.cil.c, b0849ccdd25b96758e6baa1979ff203e43704a5e97b2374ea16fb14f8fcb5d1d
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/b0849ccdd25b96758e6baa1979ff203e43704a5e97b2374ea16fb14f8fcb5d1d.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
36a94c8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2017-12-02T09:52 CET (sv-comp) | ||
a833664 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 kind | 10 | 2017-12-01T17:47:01.913391 | ||
67fe7f6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 incr | 10 | 2017-12-01T18:28:56.884418 | ||
6da4c67 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 87 | 2017-12-01T19:30 CET (sv-comp) | ||
205105e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 99 | 2017-11-30T23:05 CET (sv-comp) | ||
5e6cfee | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 110 | 2017-11-30T20:12:52+01:00 | ||
4e1951b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CBMC | 90 | 2017-12-01T02:53 CET (sv-comp) | ||
9d1fc8a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | 2LS | 82 | 2017-12-01T00:21 CET (sv-comp) | ||
4803139 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T23:46:55.084673 | ||
a8fc6e1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T15:40:30.800232 | ||
37571e4 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 472 | 2017-12-01T13:25 CET (sv-comp) | ||
e9f88f5 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | 2LS | 1186 | 2017-12-01T11:54 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/product-lines/email_spec11_product33_false-unreach-call_true-termination.cil.c, b0849ccdd25b96758e6baa1979ff203e43704a5e97b2374ea16fb14f8fcb5d1d
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/b0849ccdd25b96758e6baa1979ff203e43704a5e97b2374ea16fb14f8fcb5d1d.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |