Predicate Generation for Learning-Based Quantifier-Free Loop Invariant
InferenceArticle
Authors: Wonchan Lee ; Yungbum Jung ; Bow-yaw Wang ; Kwangkuen Yi
NULL##NULL##NULL##NULL
Wonchan Lee;Yungbum Jung;Bow-yaw Wang;Kwangkuen Yi
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.
Collaborative Research: Next-Generation Model Checking and Abstract Interpretation with a Focus on Embedded Control and Systems Biology; Funder: National Science Foundation; Code: 0926181
Bibliographic References
1 Document citing this article
Shang-Wei Lin;Jun Sun;Hao Xiao;Yang Liu;David Sanan;et al., Singapore Management University Institutional Knowledge (InK) (Singapore Management University), FiB: Squeezing loop invariants by interpolation between forward/backward predicate transformers, 2017, Urbana, IL, 10.1109/ase.2017.8115690, https://ink.library.smu.edu.sg/sis_research/4713.