Algorithm selection for software verification based on adversarial LSTM

As a prevalent technique for checking the correctness of software, software verification has achieved a significant progress in the past decades, reaching a point where a large number of verification algorithms and tools are available and sophisticated enough to handle the large-scale industrial software. However, it remains a difficult task to select a suitable verification algorithm or tool for the software at hand, given the fact that the underlying algorithms are diverse and the performance tradeoffs are hard to accurately characterize. In this paper, we study the algorithm selection problem for software verification, and propose a novel algorithm selection model based on the Long Short Term Memory network (LSTM). Our solution employs word2vec to obtain the embedding representation of the code, avoiding constructing the software features manually. We also propose a novel approach to construct the adversarial code examples in order to solve the sparsity and data imbalance problem. The experimental evaluations on the latest available dataset show that our solution improves the prediction accuracy by about 7% compared with the state-of-the-art selection algorithm.