.png){kind=icon}
.png){kind=icon}
Return
Interpretable Configuration Optimization for Static Program Verification via Rule-Based and Counterfactual Reasoning
.png){kind=icon}
PRE
AI
DOI：10.1007/978-3-032-15981-6_1.png)
.png){kind=icon}
Original request for help.png){kind=icon}
Share.png){kind=icon}
Save
Abstract
En 中文
Static program verification tools are essential for ensuring software correctness and reliability without executing the code. However, their effectiveness relies heavily on precise configuration, which must be tailored to specific project requirements, coding standards, and quality objectives. Selecting appropriate configurations is challenging due to the unique properties of each codebase and the need for an in-depth understanding of the analysis techniques. Current methods often default to standard settings or rely on random exploration, leading to sub-optimal results. In this paper, we introduce ConfigTuneX, a novel rule-based machine learning approach that optimizes configuration settings in static program verification tools through composite FOLD-SE rules. These rules simultaneously address two critical challenges: (1) reducing inconclusive outcomes by distinguishing unresolved cases from resolved outcomes, and (2) improving verification accuracy by separating correct outcomes from incorrect ones. The extracted rules are transformed into stratified answer set program (ASP) compatible with the s(CASP) solver, which systematically generates counterfactual configurations to avoid undesired outcomes. This targeted reasoning narrows the search space to the most promising configurations, reducing computational overhead while enhancing both interpretability and effectiveness. Experimental results show that ConfigTuneX with composite FOLD-SE rules consistently outperforms the state-of-the-art baseline across verification tools. On Jayhorn, CBMC, and Symbiotic, ConfigTuneX improves success rates by 76.34%, 10.73%, and 3.17%, respectively, and achieves a 76.4% success rate on JBMC where the baseline fails completely. ConfigTuneX also reduces runtime by 76.42%, 14.66%, and 48.83% on Jayhorn, CBMC, and Symbiotic, while JBMC shows a 73.69% increase due to the additional computation required for newly verified cases.
Keywords:
Static program verification
Configuration optimization
Rule-based machine learning
Counterfactual reasoning
Interpretable AI
Journal
P
IF:
0
Papers:
12
Citations:
0