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

lmcs:1035 - Logical Methods in Computer Science, September 29, 2012, Volume 8, Issue 3
Predicate Generation for Learning-Based Quantifier-Free Loop Invariant Inference

Authors: Lee, Wonchan and Jung, Yungbum and Wang, Bow-yaw and Yi, Kwangkuen

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.


Source : oai:arXiv.org:1207.7167
DOI : 10.2168/LMCS-8(3:25)2012
Volume: Volume 8, Issue 3
Published on: September 29, 2012
Submitted on: October 14, 2011
Keywords: Computer Science - Logic in Computer Science,Computer Science - Learning,F.3.1


Share

Consultation statistics

This page has been seen 125 times.
This article's PDF has been downloaded 97 times.