# SMT-Based Refutation of Spurious Bug Reports in the Clang Static Analyzer

arXiv: https://arxiv.org/abs/1810.12041 · HTML: https://mlsanity.com/paper/1810.12041/

## Key facts

- Cited by 5 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 29 Oct 2018.

## Built on by (most cited first, 5 of 5)

- [A New Era in Software Security: Towards Self-Healing Software via Large Language Models and Formal Verification](https://mlsanity.com/paper/2305.14752/) (2023)
- [The FormAI Dataset: Generative AI in Software Security Through the Lens of Formal Verification](https://mlsanity.com/paper/2307.02192/) (2023)
- [How secure is AI-generated Code: A Large-Scale Comparison of Large Language Models](https://mlsanity.com/paper/2404.18353/) (2024)
- [PromSec: Prompt Optimization for Secure Generation of Functional Source Code with Large Language Models (LLMs)](https://mlsanity.com/paper/2409.12699/) (2024)
- [Can Language Models Pretend Solvers? Logic Code Simulation with LLMs](https://mlsanity.com/paper/2403.16097/) (2024)

## Abstract (arXiv)

We describe and evaluate a bug refutation extension for the Clang Static Analyzer (CSA) that addresses the limitations of the existing built-in constraint solver. In particular, we complement CSA's existing heuristics that remove spurious bug reports. We encode the path constraints produced by CSA as Satisfiability Modulo Theories (SMT) problems, use SMT solvers to precisely check them for satisfiability, and remove bug reports whose associated path constraints are unsatisfiable. Our refutation extension refutes spurious bug reports in 8 out of 12 widely used open-source applications; on average, it refutes ca. 7% of all bug reports, and never refutes any true bug report. It incurs only negligible performance overheads, and on average adds 1.2% to the runtime of the full Clang/LLVM toolchain. A demonstration is available at tt https://www.youtube.com/watch?v=ylW5iRYNsGA.