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).
Found 0 witnesses for program sv-benchmarks/c/product-lines/email_spec0_product16_false-unreach-call_true-termination.cil.c, d76a41ceb36d1c62e7aa108a59b1177aa15b100cf21cdcc8760aecd28425289d
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/d76a41ceb36d1c62e7aa108a59b1177aa15b100cf21cdcc8760aecd28425289d.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_spec0_product16_false-unreach-call_true-termination.cil.c, d76a41ceb36d1c62e7aa108a59b1177aa15b100cf21cdcc8760aecd28425289d
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/d76a41ceb36d1c62e7aa108a59b1177aa15b100cf21cdcc8760aecd28425289d.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_spec0_product16_false-unreach-call_true-termination.cil.c, d76a41ceb36d1c62e7aa108a59b1177aa15b100cf21cdcc8760aecd28425289d
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/d76a41ceb36d1c62e7aa108a59b1177aa15b100cf21cdcc8760aecd28425289d.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_spec0_product16_false-unreach-call_true-termination.cil.c, d76a41ceb36d1c62e7aa108a59b1177aa15b100cf21cdcc8760aecd28425289d
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/d76a41ceb36d1c62e7aa108a59b1177aa15b100cf21cdcc8760aecd28425289d.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_spec0_product16_false-unreach-call_true-termination.cil.c, d76a41ceb36d1c62e7aa108a59b1177aa15b100cf21cdcc8760aecd28425289d
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/d76a41ceb36d1c62e7aa108a59b1177aa15b100cf21cdcc8760aecd28425289d.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
c2200e0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 2 | 2019-12-01 11:41:31 | ||
82576ff | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 132 | 2019-12-11T22:00:45+01:00 | 825ec1b | |
7117fa1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 105 | 2019-12-11T21:09:41+01:00 | c2200e0 | |
902b7d4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 105 | 2019-12-11T20:54:51+01:00 | ae83d86 | |
6fabd48 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 105 | 2019-12-11T20:44:38+01:00 | faf67cb | |
a434df9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 117 | 2019-12-08T01:51:25+01:00 | 7919587 | |
35356a7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 121 | 2019-12-03T08:56:52+01:00 | b8bbdc6 | |
c3f3a37 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 119 | 2019-12-03T08:08:50+01:00 | 2253472 | |
2253472 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / svcomp20 | 111 | 2019-11-30T04:57:57+01:00 | ||
7919587 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.8 | 119 | 2019-12-07T13:00:24+01:00 | ||
825ec1b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco | 132 | 2019-12-01T00:25:56+01:00 | ||
8fee31f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 148 | 2019-12-05T20:21:43+01:00 | f4c9d8c | |
e55cf91 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 148 | 2019-12-05T19:34:10+01:00 | a6ad87e |
Found 18 witnesses for program sv-benchmarks/c/product-lines/email_spec0_product16_false-unreach-call_true-termination.cil.c, d76a41ceb36d1c62e7aa108a59b1177aa15b100cf21cdcc8760aecd28425289d
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/d76a41ceb36d1c62e7aa108a59b1177aa15b100cf21cdcc8760aecd28425289d.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
7ff9954 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2018-12-08T17:26 CET (sv-comp) | ||
a86fa45 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | SMACK 1.9.3 | 20 | 2018-12-08T09:22:05 | ||
cba9f3c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Pinaka | 75 | 2018-12-07T09:00 CET (sv-comp) | ||
1e82c2e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7 | 112 | 2018-12-10T18:08:14+01:00 | ||
3c048aa | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 133 | 2018-12-07T23:07:27+01:00 | ||
cef6265 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 117 | 2018-12-10T20:37:03+01:00 | 1e82c2e | |
0f906aa | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 106 | 2018-12-09T18:21:57+01:00 | e8fea8e | |
8e91d10 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 121 | 2018-12-08T23:43:43+01:00 | 7ff9954 | |
ec22856 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 79 | 2018-12-08T22:07:27+01:00 | a86fa45 | |
4ea8bad | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 133 | 2018-12-08T08:34:55+01:00 | 3c048aa | |
0251223 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 119 | 2018-12-08T05:03:26+01:00 | 4b58f66 | |
1718932 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 105 | 2018-12-07T17:45:10+01:00 | cba9f3c | |
34060ef | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 131 | 2018-12-06T10:18:21+01:00 | 57c916f | |
69c4cfc | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 119 | 2018-12-06T09:48:11+01:00 | 8adb933 | |
8adb933 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 111 | 2018-12-05T10:34:18+01:00 | ||
fefa193 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 148 | 2018-12-06T09:42:25+01:00 | f14da1e | |
0368eaf | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 148 | 2018-12-06T09:19:03+01:00 | 91c9a91 | |
4ac1c8a | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T03:23 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/product-lines/email_spec0_product16_false-unreach-call_true-termination.cil.c, d76a41ceb36d1c62e7aa108a59b1177aa15b100cf21cdcc8760aecd28425289d
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/d76a41ceb36d1c62e7aa108a59b1177aa15b100cf21cdcc8760aecd28425289d.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_spec0_product16_false-unreach-call_true-termination.cil.c, d76a41ceb36d1c62e7aa108a59b1177aa15b100cf21cdcc8760aecd28425289d
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/d76a41ceb36d1c62e7aa108a59b1177aa15b100cf21cdcc8760aecd28425289d.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |