Algorithm Selection for Software Verification using Graph Attention Networks

The field of software verification has produced a wide array of algorithmic techniques that can prove a variety of properties of a given program. It has been demonstrated that the performance of these techniques can vary up to 4 orders of magnitude on the same verification problem. Even for verification experts, it is difficult to decide which tool will perform best on a given problem. For general users, deciding the best tool for their verification problem is effectively impossible. In this work, we present Graves, a selection strategy based on graph neural networks (GNNs). Graves generates a graph representation of a program from which a GNN predicts a score for a verifier that indicates its performance on the program. We evaluate Graves on a set of 10 verification tools and over 8000 verification problems and find that it improves the state-of-the-art in verification algorithm selection by 11\%. We conjecture this is in part due to Graves' use of GNNs with attention mechanisms. Through a qualitative study on model interpretability, we find strong evidence that the Graves' GNN-based model learns to base its predictions on factors that relate to the unique features of the algorithmic techniques.