POPL 2025
Sun 19 - Sat 25 January 2025 Denver, Colorado, United States
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 Jan

Displayed time zone: Mountain Time (US & Canada) change

14:00 - 15:30
Static Analysis and Abstract InterpretationTPSA at Patty Cake
14:00
18m
Talk
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
18m
Talk
Calculational design of Incorrectness Separation Logic
TPSA
Lorenzo Gazzella Università di Pisa
14:36
18m
Talk
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
18m
Talk
Enhancing Infer Compositional Analysis with Summary Specialization
TPSA
15:12
18m
Talk
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