arXiv subjects

William Klieber

Publications and source records attributed to William Klieber.

3 recordsLinked to original sources

arXiv2026

Solving QBF with Counterexample Guided Refinement

We propose two novel approaches for using Counterexample-Guided Abstraction Refinement (CEGAR) in Quantified Boolean Formula (QBF) solvers. The first approach develops a recursive algorithm whose search is driven by CEGAR (rather than by DPLL). The second approach employs CEGAR as an additional learning technique in an existing DPLL-based QBF solver. Experimental evaluation of the implemented prototypes shows that the CEGAR-driven solver outperforms existing solvers on a number of families in the QBF-LIB and that the DPLL solver benefits from the additional type of learning. Thus this article opens two promising avenues in QBF: CEGAR-driven solvers as an alternative to existing approaches and a novel type of learning in DPLL.

cs.LO↗

arXiv2026

Using LLMs to Adjudicate Static-Analysis Alerts with Error Reduction Techniques

Static analysis is widely used for finding security weaknesses in source code before deployment, but it often produces far more alerts than analysts can review. We study how well large language models (LLMs) can adjudicate (classify as a real bug or a false alarm) static-analysis alerts. We use two mistake-mitigation methods: (1) a consistency check (CC) that runs the LLM multiple times and checks that the verdicts are consistent with each other, and (2) an LLM reasoning evaluation (LRE) step that runs the LLM multiple times and then asks the LLM to choose a verdict after evaluating the reasoning provided by each run. We evaluated several LLMs on three test suites: Juliet, FormAI, and SV-COMP. Across all three suites, the mid-tier reasoning LLMs that we tested (o4-mini, gpt-oss-120b, gpt-oss-20b) reach high recall (percent of real bugs that the tool correctly flags as needing repair / manual attention) and specificity (percent of actually false alerts that the tool correctly dismisses as false alarms). With mistake mitigation, they reach at least 98% recall and at least 94.8% specificity on every suite (with CC alone on Juliet and SV-COMP, and with LRE+CC on FormAI). We probe Juliet memorization and show that o4-mini can often reconstruct sanitized test cases' original identities, so we base our generalization claims primarily on FormAI, scored against our own unpublished manual adjudications. We also report results of using the LLM to synthesize a program that dynamically triggers the flaw as independent evidence; a validity check rejected every trigger driver aimed at a false alarm, so a valid trigger proved to be strong evidence of a real flaw.

cs.SE↗

arXiv2025

Automated Code Repair for C/C++ Static Analysis Alerts

(Note: This work is a preprint.) Static analysis (SA) tools produce many diagnostic alerts indicating that source code in C or C++ may be defective and potentially vulnerable to security exploits. Many of these alerts are false positives. Identifying the true-positive alerts and repairing the defects in the associated code are huge efforts that automated program repair (APR) tools can help with. Our experience showed us that APR can reduce the number of SA alerts significantly and reduce the manual effort of analysts to review code. This engineering experience paper details the application of design, development, and performance testing to an APR tool we built that repairs C/C++ code associated with 3 categories of alerts produced by multiple SA tools. Its repairs are simple and local. Furthermore, our findings convinced the maintainers of the CERT Coding Standards to re-assess and update the metrics used to assess when violations of guidelines are detectable or repairable. We discuss engineering design choices made to support goals of trustworthiness and acceptability to developers. Our APR tool repaired 8718 out of 9234 alerts produced by one SA tool on one codebase. It can repair 3 flaw categories. For 2 flaw categories, 2 SA tools, and 2 codebases, our tool repaired or dismissed as false positives over 80% of alerts, on average. Tests showed repairs did not appreciably degrade the performance of the code or cause new alerts to appear (with the possible exception of sqlite3.c). This paper describes unique contributions that include a new empirical analysis of SA data, our selection method for flaw categories to repair, publication of our APR tool, and a dataset of SA alerts from open-source SA tools run on open-source codebases. It discusses positive and negative results and lessons learned.

cs.SE↗