# MFH: A Multi-faceted Heuristic Algorithm Selection Approach for Software Verification

arXiv: https://arxiv.org/abs/2503.22228 · HTML: https://mlsanity.com/paper/2503.22228/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 13 of its 46 references that are in the map.
- First posted on arXiv 28 Mar 2025.

## Builds on (most cited first, 13 of 13)

- [Attention Is All You Need](https://mlsanity.com/paper/1706.03762/) (2017)
- [Graph Attention Networks](https://mlsanity.com/paper/1710.10903/) (2017)
- [Inductive Representation Learning on Large Graphs](https://mlsanity.com/paper/1706.02216/) (2017)
- [DeepWalk: Online Learning of Social Representations](https://mlsanity.com/paper/1403.6652/) (2014)
- [Graph-to-Sequence Learning using Gated Graph Neural Networks](https://mlsanity.com/paper/1806.09835/) (2018)
- [Neural population geometry: An approach for understanding biological and artificial neural networks](https://mlsanity.com/paper/2104.07059/) (2021)
- [Macro Graph Neural Networks for Online Billion-Scale Recommender Systems](https://mlsanity.com/paper/2401.14939/) (2024)
- [Deep Learning Enabled Semantic Communications with Speech Recognition and Synthesis](https://mlsanity.com/paper/2205.04603/) (2022)
- [ReGVD: Revisiting Graph Neural Networks for Vulnerability Detection](https://mlsanity.com/paper/2110.07317/) (2021)
- [CBMC: The C Bounded Model Checker](https://mlsanity.com/paper/2302.02384/) (2023)
- [ESBMC v7.4: Harnessing the Power of Intervals](https://mlsanity.com/paper/2312.14746/) (2023)
- [Deductive Verification of Unmodified Linux Kernel Library Functions](https://mlsanity.com/paper/1809.00626/) (2018)
- [An experimental Study using ACSL and Frama-C to formulate and verify Low-Level Requirements from a DO-178C compliant Avionics Project](https://mlsanity.com/paper/1508.03894/) (2015)

## Abstract (arXiv)

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.