Predicting Rankings of Software Verification Competitions
This work addresses the need for pre-runtime performance estimation in software verification competitions, which is useful for applications like portfolio solvers, but it is incremental as it builds on existing label ranking techniques with domain-specific adaptations.
The paper tackles the problem of predicting rankings of software verification tools on specific tasks before execution, using a machine learning approach with label ranking algorithms and custom kernels for code similarity. The method achieves high predictive accuracy and outperforms a recent feature-based approach on SV-COMP data.
Software verification competitions, such as the annual SV-COMP, evaluate software verification tools with respect to their effectivity and efficiency. Typically, the outcome of a competition is a (possibly category-specific) ranking of the tools. For many applications, such as building portfolio solvers, it would be desirable to have an idea of the (relative) performance of verification tools on a given verification task beforehand, i.e., prior to actually running all tools on the task. In this paper, we present a machine learning approach to predicting rankings of tools on verification tasks. The method builds upon so-called label ranking algorithms, which we complement with appropriate kernels providing a similarity measure for verification tasks. Our kernels employ a graph representation for software source code that mixes elements of control flow and program dependence graphs with abstract syntax trees. Using data sets from SV-COMP, we demonstrate our rank prediction technique to generalize well and achieve a rather high predictive accuracy. In particular, our method outperforms a recently proposed feature-based approach of Demyanova et al. (when applied to rank predictions).