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
Secondary volumes: Selected Papers of the 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2011)
Published on: September 29, 2012
Imported on: October 14, 2011
Keywords: Computer Science - Logic in Computer Science, Computer Science - Machine 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 3180 times.
This article's PDF has been downloaded 555 times.