POPL 2026
Sun 11 - Sat 17 January 2026 Rennes, France
Mon 12 Jan 2026 16:30 - 17:00 at Salle 12 - PADL M4 Chair(s): Nada Amin, Joaquín Arias

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 all 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.

Mon 12 Jan

Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

16:00 - 17:30
PADL M4PADL at Salle 12
Chair(s): Nada Amin Harvard University, Joaquín Arias Universidad Rey Juan Carlos
16:00
30m
Talk
Declarative Debugging for Modern Networks
PADL
Anduo Wang Temple University, USA, Matthew Caesar UIUC
16:30
30m
Talk
Interpretable Configuration Optimization for Static Program Verification via Rule-Based and Counterfactual Reasoning
PADL
Jaeseong Lee The University of Texas at Dallas, Sopam Dasgupta The University of Texas at Dallas, Gopal Gupta The University of Texas at Dallas, Shiyi Wei University of Texas at Dallas
17:00
30m
Talk
REGAL: Extracting implicit rules in text using LLMs with logic program feedback
PADL
Abhiramon Rajasekharan The University of Texas at Dallas, Gopal Gupta The University of Texas at Dallas