POPL 2025 (series) / TPSA 2025 (series) / Theory and Practice of Static Analysis 2025 /
Scalable Bug Detection for Internally Unsafe Libraries: A Logical Approach to Type Refutation
Recent work has shown promising advances in techniques for scalable bug detection by leveraging \emph{under-approximate} (UX) reasoning. This work presents a UX approach to \emph{automatically} detect type unsoundness in libraries that rely on internal use of \emph{unsafe features}. To reason about such libraries, we build on prior work by encoding type assignments as \emph{separation logic} assertions. Our key insight is that undefined behaviour obtained from incorrect uses of unsafe features may be reasoned about by refuting such type assignments via \emph{incorrectness logic}. We demonstrate how our approach may be used to detect memory safety bugs in a simple language with an ownership type system.