Inferring Loop Invariants for Program Verification: an Abductive Learning Perspective

Loop invariant synthesis is one of the most important tasks in program verification.This problem is fundamentally undecidable,as it involves reasoning about infinite state spaces.Current software analysis techniques rely heavily on human-defined language biases to make the search tractable.When the language bias is misaligned with the unseen problem domain, these methods are prone to failure.Hence, to generalize on unseen problems, it is natural to explore training a model to learn and infer loop invariants. However, given the lack of supervision and the significant reasoning abilities required, learning to infer invariants is challenging.In this paper, we explore the feasibility of training a model for end-to-end loop invariant inference without human-labeled data.We present Abductive Loop InVariant lEarning (ALIVE) to combine machine learning and logical abduction in a mutually beneficial way.Logical abduction explores the solution space and subsequently refines the learning model by leveraging the discovered invariants.The machine learning model offers an initial solution that serves as a strong starting point, thereby facilitating the search process.Experiments show that ALIVE significantly outperforms other machine learning methods in both accuracy and efficiency.