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
Tue 21 Jan 2025 14:36 - 14:54 at Patty Cake - Static Analysis and Abstract Interpretation
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.
Tue 21 JanDisplayed time zone: Mountain Time (US & Canada) change
Tue 21 Jan
Displayed time zone: Mountain Time (US & Canada) change
14:00 - 15:30 | |||
14:00 18mTalk | Compositional Shape Analysis with Shared Abduction and Biabductive Loop Acceleration (Extended Abstract)Remote TPSA Florian Sextl TU Wien, Austria, Adam Rogalewicz Brno University of Technology, Czechia, Tomáš Vojnar Brno University of Technology, Florian Zuleger TU Vienna Pre-print | ||
14:18 18mTalk | Calculational design of Incorrectness Separation Logic TPSA Lorenzo Gazzella Università di Pisa | ||
14:36 18mTalk | Scalable Bug Detection for Internally Unsafe Libraries: A Logical Approach to Type Refutation TPSA Pedro Carrott Imperial College London, Sacha-Élie Ayoun Imperial College London, Azalea Raad Imperial College London | ||
14:54 18mTalk | Enhancing Infer Compositional Analysis with Summary Specialization TPSA David Pichardie Meta | ||
15:12 18mTalk | Cyclic Message Histories for Automated Safety Verification of Distributed Algorithms TPSA Christian Fontenot University of Colorado Boulder, Gowtham Kaki University of Colorado at Boulder, Bor-Yuh Evan Chang University of Colorado Boulder & Amazon |