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.

    https://doi.org/10.2168/LMCS-8(3:25)2012
    Source: arXiv.org:1207.7167
    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
    Licence: arXiv.org - Non-exclusive license to distribute
    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

    Classifications

    Mathematics Subject Classification 20201
    Sources:
    • [1] zbMATH Open.

    1 Document citing this article

    Share and export

    Consultation statistics

    This page has been seen 1653 times.
    This article's PDF has been downloaded 385 times.