LLM2D
MFH:用于软件验证的多面向启发式算法选择方法
MFH: A Multi-faceted Heuristic Algorithm Selection Approach for Software Verification
作者: Jie Su, Liansai Deng, Cheng Wen, Rong Wang, Zhi Ma, Nan Zhang, Cong Tian, Zhenhua Duan, Shengchao Qin
发布日期: 3/31/2025
arXiv ID: oai:arXiv.org:2503.22228v1

摘要

arXiv:2503.22228v1 宣告类型: cross 摘要: 目前,有许多验证算法可用于提高软件系统的可靠性。选择合适的验证算法通常需要领域专业知识和大量的劳动力。因此,需要一个自动化的算法选择器。然而,现有的选择器要么依赖于机器学习策略,要么依靠手动设计的启发式方法,这些问题包括对高质量带有算法标签的样本的依赖以及可扩展性受限。在本文中,我们提出了一种用于软件验证的自动化算法选择方法,称为MFH。我们的方法利用验证器在产生正确结果时通常会实施某些适当算法的启发式,并且验证器支持的算法间接反映了哪些算法可能是适用的。具体而言,MFH 将语义保持转换后的程序的代码属性图(CPG)嵌入到预测模型中,以增强预测模型的鲁棒性。此外,我们的方法将选择任务分解为预测可能适用的算法和匹配最合适的验证器的子任务。另外,MFH 还引入了一个反馈循环,用于提高模型的预测准确性。我们对20个验证器和超过15,000个验证任务进行了评估。实验结果表明,MFH 的有效性,即使在训练过程中没有提供真实的算法标签,其预测准确率仍达到了91.47%。此外,引入10个新验证器时,预测准确率仅下降0.84%,表明提出的方法具有很强的可扩展性。