Currently, many verification algorithms are available to improve the reliability of software systems. Selecting the appropriate verification algorithm typically demands domain expertise and non-trivial manpower. An automated algorithm selector is thus desired. However, existing selectors, either depend on machine-learned strategies or manually designed heuristics, encounter issues such as reliance on high-quality samples with algorithm labels and limited scalability. In this paper, an automated algorithm selection approach, namely MFH, is proposed for software verification. Our approach leverages the heuristics that verifiers producing correct results typically implement certain appropriate algorithms, and the supported algorithms by these verifiers indirectly reflect which ones are potentially applicable. Specifically, MFH embeds the code property graph (CPG) of a semantic-preserving transformed program to enhance the robustness of the prediction model. Furthermore, our approach decomposes the selection task into the sub-tasks of predicting potentially applicable algorithms and matching the most appropriate verifiers. Additionally, MFH also introduces a feedback loop on incorrect predictions to improve model prediction accuracy. We evaluate MFH on 20 verifiers and over 15,000 verification tasks. Experimental results demonstrate the effectiveness of MFH, achieving a prediction accuracy of 91.47% even without ground truth algorithm labels provided during the training phase. Moreover, the prediction accuracy decreases only by 0.84% when introducing 10 new verifiers, indicating the strong scalability of the proposed approach.

翻译：当前，众多验证算法可用于提升软件系统的可靠性。选择合适的验证算法通常需要领域专业知识与大量人力投入，因此亟需自动化的算法选择器。然而，现有选择器或依赖基于机器学习的策略，或采用人工设计的启发式方法，均面临对带算法标签的高质量样本的依赖以及可扩展性有限等问题。本文提出一种面向软件验证的自动化算法选择方法MFH。该方法基于以下启发式原则：能够输出正确结果的验证器通常实现了某些合适的算法，而这些验证器所支持的算法间接反映了哪些算法可能适用。具体而言，MFH通过嵌入经语义保持变换后程序的代码属性图（CPG）来增强预测模型的鲁棒性。此外，本方法将算法选择任务分解为预测潜在适用算法与匹配最合适验证器两个子任务。同时，MFH还引入了针对错误预测的反馈循环机制以提升模型预测精度。我们在20个验证器与超过15,000个验证任务上对MFH进行评估。实验结果表明，即使在训练阶段未提供真实算法标签的情况下，MFH仍能达到91.47%的预测准确率。此外，当引入10个新验证器时，预测准确率仅下降0.84%，证明该方法具有强大的可扩展性。