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

• A Principled Approach to Randomized Selection under Uncertainty: Applications to Peer Review and Grant Funding [68.43987626137512]
  We propose a principled framework for randomized decision-making based on interval estimates of the quality of each item.<n>We introduce MERIT, an optimization-based method that maximizes the worst-case expected number of top candidates selected.<n>We prove that MERIT satisfies desirable axiomatic properties not guaranteed by existing approaches.
  arXiv  Detail & Related papers  (2025-06-23T19:59:30Z)
• Towards Better Code Generation: Adaptive Decoding with Uncertainty Guidance [28.99265405319943]
  We introduce AdaDec, an adaptive decoding framework guided by token-level uncertainty quantified via Shannon entropy.<n>AdaDec achieves up to a 15.5% improvement in Pass@1 accuracy compared to greedy decoding, matches or outperforms traditional beam search.
  arXiv  Detail & Related papers  (2025-06-10T16:49:46Z)
• Algorithms with Calibrated Machine Learning Predictions [9.18151868060576]
  A field of algorithms with predictions incorporates machine learning advice in the design of online algorithms to improve real-world performance.<n>A central consideration is the extent to which predictions can be trusted -- while existing approaches often require users to specify an aggregate trust level, modern machine learning models can provide estimates of prediction-level uncertainty.<n>We propose calibration as a principled and practical tool to bridge this gap, demonstrating the benefits of calibrated advice through two case studies.
  arXiv  Detail & Related papers  (2025-02-05T03:41:18Z)
• 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.