POPL 2026
Sun 11 - Sat 17 January 2026 Rennes, France
Mon 12 Jan 2026 14:45 - 15:07 at Salle 13 - Session 2

We describe a new LLVM frontend for Infer, specifically for Swift analysis. This project is vital due to Swift’s increasing use in Meta’s iOS applications, with the primary goal of identifying critical issues such as retain cycles and null pointer crashes at the Objective-C and Swift boundary. We cover some highlights of the implementation of the frontend, including the translation of virtual calls and the mapping of LLVM’s memory model to Pulse’s abstract heap. Challenges like opaque pointers are discussed, alongside the comprehensive testing infrastructure established for validation. The work ultimately aims to contribute to more robust and reliable Swift applications by enhancing Infer’s capabilities in detecting memory safety issues for Swift.

Mon 12 Jan

Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

14:00 - 15:30
Session 2TPSA at Salle 13
14:00
22m
Talk
Soteria Rust: Efficient Symbolic Execution for Rust
TPSA
Opale Sjöstedt Imperial College London, Sacha-Élie Ayoun Imperial College London, Azalea Raad Imperial College London
14:22
22m
Talk
Towards automatic functional correctness in the Mopsa static analyzer
TPSA
Milla Valnet Sorbonne Université, Raphaël Monat Inria and University of Lille, Antoine Miné Sorbonne Université
14:45
22m
Talk
An LLVM frontend for Infer for Swift analysis
TPSA
15:07
22m
Talk
Specialisation: Context-Dependent Reasoning in Incorrectness Separation Logic
TPSA
Raquel Fernandes da Silva Imperial College London, Sacha-Élie Ayoun Imperial College London, Azalea Raad Imperial College London, David Pichardie Meta