Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2411.12749 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866909396238336000 |
|---|---|
| author | Su, Yuheng Yang, Qiusong Ci, Yiwei |
| author_facet | Su, Yuheng Yang, Qiusong Ci, Yiwei |
| contents | The IC3 algorithm, also known as PDR, has made a significant impact in the field of safety model checking in recent years due to its high efficiency, scalability, and completeness. The most crucial component of IC3 is inductive generalization, which involves dropping variables one by one and is often the most time-consuming step. In this paper, we propose a novel approach to predict a possible minimal lemma before dropping variables by utilizing the counterexample to propagation (CTP). By leveraging this approach, we can avoid dropping variables if predict successfully. The comprehensive evaluation demonstrates a commendable success rate in lemma prediction and a significant performance improvement achieved by our proposed method. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2411_12749 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Predicting Lemmas in Generalization of IC3 Su, Yuheng Yang, Qiusong Ci, Yiwei Software Engineering The IC3 algorithm, also known as PDR, has made a significant impact in the field of safety model checking in recent years due to its high efficiency, scalability, and completeness. The most crucial component of IC3 is inductive generalization, which involves dropping variables one by one and is often the most time-consuming step. In this paper, we propose a novel approach to predict a possible minimal lemma before dropping variables by utilizing the counterexample to propagation (CTP). By leveraging this approach, we can avoid dropping variables if predict successfully. The comprehensive evaluation demonstrates a commendable success rate in lemma prediction and a significant performance improvement achieved by our proposed method. |
| title | Predicting Lemmas in Generalization of IC3 |
| topic | Software Engineering |
| url | https://arxiv.org/abs/2411.12749 |