Wonchan Lee ; Yungbum Jung ; Bow-yaw Wang ; Kwangkuen Yi - Predicate Generation for Learning-Based Quantifier-Free Loop Invariant Inference

lmcs:1035 - Logical Methods in Computer Science, September 29, 2012, Volume 8, Issue 3 - https://doi.org/10.2168/LMCS-8(3:25)2012
Predicate Generation for Learning-Based Quantifier-Free Loop Invariant InferenceArticle

Authors: 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.


    Volume: Volume 8, Issue 3
    Published on: September 29, 2012
    Imported on: October 14, 2011
    Keywords: Computer Science - Logic in Computer Science,Computer Science - Learning,F.3.1
    Funding:
      Source : OpenAIRE Graph
    • Collaborative Research: Next-Generation Model Checking and Abstract Interpretation with a Focus on Embedded Control and Systems Biology; Funder: National Science Foundation; Code: 0926181

    1 Document citing this article

    Consultation statistics

    This page has been seen 1212 times.
    This article's PDF has been downloaded 347 times.