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]. Experiments excerpted from Linux, SPEC2000, and Tar source codes are reported. © 2011 Springer-Verlag.
Mendeley helps you to discover research relevant for your work.
CITATION STYLE
Jung, Y., Lee, W., Wang, B. Y., & Yi, K. (2011). Predicate generation for learning-based quantifier-free loop invariant inference. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6605 LNCS, pp. 205–219). https://doi.org/10.1007/978-3-642-19835-9_17