Predicate Generation for Learning-Based Quantifier-Free Loop Invariant Inference

TL;DR

This paper presents a novel predicate generation method using interpolation for improving learning-based loop invariant inference, demonstrating enhanced effectiveness and efficiency on real-world program examples.

Contribution

It introduces an interpolation-based predicate synthesis approach that advances loop invariant inference techniques beyond prior methods.

Findings

Improved inference efficiency on Linux, SPEC2000, and Tar utility examples.

Enhanced effectiveness of loop invariant inference.

Successful application of interpolation in predicate generation.

Abstract

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.