论文标题
使用图神经网络的软件验证算法选择算法
Algorithm Selection for Software Verification using Graph Neural Networks
论文作者
论文摘要
软件验证领域已经产生了各种算法技术，这些技术可以证明给定程序的各种属性。已经证明，在同一验证问题上，这些技术的性能最多可以变化4个数量级。即使对于验证专家，也很难确定哪种工具在给定的问题上会表现最佳。对于普通用户而言，确定其验证问题的最佳工具实际上是不可能的。 在这项工作中，我们提出了Graves，这是基于图神经网络（GNNS）的选择策略。 Graves生成了一个程序的图表表示，GNN可以从中预测验证者的分数，以表明其在程序上的性能。 我们评估了一组10个验证工具和8000多个验证问题的坟墓，发现它在验证算法选择中的最新算法提高了12％或8个百分点。此外，它能够比我们的测试集中的任何现有验证者多验证9％的问题。通过一项关于模型可解释性的定性研究，我们发现了有力的证据表明，坟墓的模型可以将其预测基于与算法技术独特特征有关的因素。
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.
