Algorithm Selection for Software Verification Using Graph Neural Networks

doi:10.1145/3637225

Algorithm Selection for Software Verification Using Graph Neural Networks

2024-03-14

0

OA

AI

DOI：10.1145/3637225

原文求助

摘要

En 中文

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 8,000 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.

Keyword:

Algorithm selection

graph neural networks

Algorithm Selection for Software Verification Using Graph Neural Networks

摘要

期刊

机构