Algorithm Selection for Software Verification using Graph Neural Networks

TL;DR

This paper introduces Graves, a graph neural network-based system that predicts the most effective verification algorithm for a given program, significantly improving selection accuracy and problem verification success rates.

Contribution

It presents a novel GNN-based approach for algorithm selection in software verification, outperforming existing methods in accuracy and problem coverage.

Findings

Improves verification algorithm selection accuracy by 12%.

Verifies 9% more problems than existing verifiers.

Model learns to base predictions on program features.

Abstract

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 12%, or 8 percentage points. Further, it is able to verify 9% more problems than any existing verifier on our test set. Through a qualitative study on model interpretability, we find strong evidence that the Graves' model learns to base its predictions on factors that relate to the unique features of the algorithmic techniques.