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

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.