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

• URL: http://arxiv.org/abs/2503.22228v1
• Date: Fri, 28 Mar 2025 08:21:00 GMT
• Title: MFH: A Multi-faceted Heuristic Algorithm Selection Approach for Software Verification
• Authors: Jie Su, Liansai Deng, Cheng Wen, Rong Wang, Zhi Ma, Nan Zhang, Cong Tian, Zhenhua Duan, Shengchao Qin,
• Abstract summary: We propose an automated algorithm selection approach, namely MFH, for software verification.<n>MFH embeds the code property graph (CPG) of a semantic-preserving transformed program to enhance the robustness of the prediction model.<n>We evaluate MFH on 20 verifiers and over 15,000 verification tasks.
• Score: 23.80925841520252
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: 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.

Related papers

• Calibrated Selective Classification [34.08454890436067]
  We develop a new approach to selective classification in which we propose a method for rejecting examples with "uncertain" uncertainties. We present a framework for learning selectively calibrated models, where a separate selector network is trained to improve the selective calibration error of a given base model. We demonstrate the empirical effectiveness of our approach on multiple image classification and lung cancer risk assessment tasks.
  arXiv  Detail & Related papers  (2022-08-25T13:31:09Z)
• Efficient and Differentiable Conformal Prediction with General Function Classes [96.74055810115456]
  We propose a generalization of conformal prediction to multiple learnable parameters. We show that it achieves approximate valid population coverage and near-optimal efficiency within class. Experiments show that our algorithm is able to learn valid prediction sets and improve the efficiency significantly.
  arXiv  Detail & Related papers  (2022-02-22T18:37:23Z)
• Learning Predictions for Algorithms with Predictions [49.341241064279714]
  We introduce a general design approach for algorithms that learn predictors. We apply techniques from online learning to learn against adversarial instances, tune robustness-consistency trade-offs, and obtain new statistical guarantees. We demonstrate the effectiveness of our approach at deriving learning algorithms by analyzing methods for bipartite matching, page migration, ski-rental, and job scheduling.
  arXiv  Detail & Related papers  (2022-02-18T17:25:43Z)
• Robustification of Online Graph Exploration Methods [59.50307752165016]
  We study a learning-augmented variant of the classical, notoriously hard online graph exploration problem. We propose an algorithm that naturally integrates predictions into the well-known Nearest Neighbor (NN) algorithm.
  arXiv  Detail & Related papers  (2021-12-10T10:02:31Z)
• Conformal prediction for text infilling and part-of-speech prediction [0.549690036417587]
  We propose inductive conformal prediction algorithms for the tasks of text infilling and part-of-speech prediction. We analyze the performance of the algorithms in simulations using the Brown Corpus, which contains over 57,000 sentences.
  arXiv  Detail & Related papers  (2021-11-04T02:23:05Z)
• Towards Feature-Based Performance Regression Using Trajectory Data [0.9281671380673306]
  Black-box optimization is a very active area of research, with many new algorithms being developed every year. The variety of algorithms poses a meta-problem: which algorithm to choose for a given problem at hand? Past research has shown that per-instance algorithm selection based on exploratory landscape analysis can be an efficient mean to tackle this meta-problem.
  arXiv  Detail & Related papers  (2021-02-10T10:19:13Z)
• Amortized Conditional Normalized Maximum Likelihood: Reliable Out of Distribution Uncertainty Estimation [99.92568326314667]
  We propose the amortized conditional normalized maximum likelihood (ACNML) method as a scalable general-purpose approach for uncertainty estimation. Our algorithm builds on the conditional normalized maximum likelihood (CNML) coding scheme, which has minimax optimal properties according to the minimum description length principle. We demonstrate that ACNML compares favorably to a number of prior techniques for uncertainty estimation in terms of calibration on out-of-distribution inputs.
  arXiv  Detail & Related papers  (2020-11-05T08:04:34Z)
• Adaptive Sampling for Best Policy Identification in Markov Decision Processes [79.4957965474334]
  We investigate the problem of best-policy identification in discounted Markov Decision (MDPs) when the learner has access to a generative model. The advantages of state-of-the-art algorithms are discussed and illustrated.
  arXiv  Detail & Related papers  (2020-09-28T15:22:24Z)
• Bayesian Optimization with Machine Learning Algorithms Towards Anomaly Detection [66.05992706105224]
  In this paper, an effective anomaly detection framework is proposed utilizing Bayesian Optimization technique. The performance of the considered algorithms is evaluated using the ISCX 2012 dataset. Experimental results show the effectiveness of the proposed framework in term of accuracy rate, precision, low-false alarm rate, and recall.
  arXiv  Detail & Related papers  (2020-08-05T19:29:35Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.