Assertion Generation Through Active Learning

Abstract

Program assertions are useful for many program analysis tasks. They are however often missing in practice. Many approaches have been developed to generate assertions automatically. Existing methods are either based on generalizing from a set of test cases (e.g., Daikon), or based on some forms of symbolic execution. In this work, we develop a novel approach for generating likely assertions automatically based on active learning. Our targets are complex Java programs which are challenging for symbolic execution. Our key idea is to generate candidate assertions based on test cases and then apply active learning techniques to iteratively improve them. We evaluate our approach using two sets of programs, i.e., 425 methods from three popular Java projects from GitHub and 10 programs from the SVComp repository. We evaluate the ‘correctness’ of the assertions either by comparing them with existing assertion-like checking conditions, or by comparing them with the documentation, or by verifying them.