Predicting Rankings of Software Verification Competitions
Mike Czech, Eyke Hüllermeier, Marie-Christine Jakobs, Heike Wehrheim Department of Computer Science Paderborn University Germany
Abstract
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.
中文速览
用图结构来表示C程序——把控制流图、程序依赖图和抽象语法树融合成一个统一的带标签图——然后用Weisfeiler-Lehman图核（graph kernel）衡量两个程序之间的相似度，再结合标签排序（label ranking）算法，就能在不实际运行任何验证工具的前提下预测它们在给定程序上的排名顺序。研究者用SV-COMP 2015和2017的竞赛数据做了交叉验证实验，结果表明该方法在Spearman秩相关指标上明显优于Demyanova等人基于人工设计特征向量的方法，在几乎所有参数设置和数据集（通用安全性、终止性、内存安全性）上都取得了更高的预测精度。这项工作的价值在于：一方面帮助程序员或投资组合求解器（portfolio solver）在运行工具之前就能智能选型，另一方面所提出的图核表示完全通用，无需针对验证任务重新设计特征，可直接迁移到其他程序分析的机器学习场景中。
原文 arXiv:1703.00757;中英对照 + 大白话阅读 https://aha.fim.ai/paper/1703.00757v1