Predicate Generation for Learning-Based Quantifier-Free Loop Invariant Inference
We address the predicate generation problem in the context of loop invariant inference. Motivated by the interpolation-based abstraction refinement technique, we apply the interpolation theorem to synthesize predicates implicitly implied by program texts. Our technique is able to improve the effecti...
| Main Authors: | , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2012-09-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/1035/pdf |
| _version_ | 1797268737918763008 |
|---|---|
| author | Wonchan Lee Yungbum Jung Bow-yaw Wang Kwangkuen Yi |
| author_facet | Wonchan Lee Yungbum Jung Bow-yaw Wang Kwangkuen Yi |
| author_sort | Wonchan Lee |
| collection | DOAJ |
| description | We address the predicate generation problem in the context of loop invariant
inference. Motivated by the interpolation-based abstraction refinement
technique, we apply the interpolation theorem to synthesize predicates
implicitly implied by program texts. Our technique is able to improve the
effectiveness and efficiency of the learning-based loop invariant inference
algorithm in [14]. We report experiment results of examples from Linux,
SPEC2000, and Tar utility. |
| first_indexed | 2024-04-25T01:37:15Z |
| format | Article |
| id | doaj.art-fd647e56179c46e9b793c87c1be51234 |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:37:15Z |
| publishDate | 2012-09-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-fd647e56179c46e9b793c87c1be512342024-03-08T09:28:00ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742012-09-01Volume 8, Issue 310.2168/LMCS-8(3:25)20121035Predicate Generation for Learning-Based Quantifier-Free Loop Invariant InferenceWonchan LeeYungbum JungBow-yaw WangKwangkuen YiWe address the predicate generation problem in the context of loop invariant inference. Motivated by the interpolation-based abstraction refinement technique, we apply the interpolation theorem to synthesize predicates implicitly implied by program texts. Our technique is able to improve the effectiveness and efficiency of the learning-based loop invariant inference algorithm in [14]. We report experiment results of examples from Linux, SPEC2000, and Tar utility.https://lmcs.episciences.org/1035/pdfcomputer science - logic in computer sciencecomputer science - learningf.3.1 |
| spellingShingle | Wonchan Lee Yungbum Jung Bow-yaw Wang Kwangkuen Yi Predicate Generation for Learning-Based Quantifier-Free Loop Invariant Inference Logical Methods in Computer Science computer science - logic in computer science computer science - learning f.3.1 |
| title | Predicate Generation for Learning-Based Quantifier-Free Loop Invariant Inference |
| title_full | Predicate Generation for Learning-Based Quantifier-Free Loop Invariant Inference |
| title_fullStr | Predicate Generation for Learning-Based Quantifier-Free Loop Invariant Inference |
| title_full_unstemmed | Predicate Generation for Learning-Based Quantifier-Free Loop Invariant Inference |
| title_short | Predicate Generation for Learning-Based Quantifier-Free Loop Invariant Inference |
| title_sort | predicate generation for learning based quantifier free loop invariant inference |
| topic | computer science - logic in computer science computer science - learning f.3.1 |
| url | https://lmcs.episciences.org/1035/pdf |
| work_keys_str_mv | AT wonchanlee predicategenerationforlearningbasedquantifierfreeloopinvariantinference AT yungbumjung predicategenerationforlearningbasedquantifierfreeloopinvariantinference AT bowyawwang predicategenerationforlearningbasedquantifierfreeloopinvariantinference AT kwangkuenyi predicategenerationforlearningbasedquantifierfreeloopinvariantinference |