POPL 2026
Sun 11 - Sat 17 January 2026 Rennes, France

While decades of research in program logics, abstract interpretation, and separation logic provide a strong foundation for automated static analysis, new challenges have arisen in recent years, spurring accelerated innovation in both the underlying theory and practical implementation of static analysis systems.

One such example is the challenge of incorrectness reasoning. Bug-finding has long been an important part of industrial static analysis, but sound logical theories for incorrectness were only recently explored, motivated by the need for tools that efficiently identify true bugs. Subsequently, incorrectness reasoning has become an active area of research with work to combine it with separation logic, concurrency, abstract interpretation, security and hyperproperties, and type systems. Automated reasoning tools based on these theories are under active development at companies such as Meta and Bloomberg.

Another example is reasoning about computational effects, which is notoriously difficult to automate. Such effects include concurrency, randomization, exceptions, and nontermination. Recent work has been done to develop theories and tools for detecting deadlocks, race conditions, and programs with divergent behavior. In addition, automation techniques are under development for randomized programs, to reason about programs in terms of expectations.

This workshop provides a venue where researchers and practitioners can present speculative ideas about new analysis techniques. Since it is very hard to implement and validate these systems, we encourage the sharing of early stage ideas and emerging trends that are not yet ready for publication in conferences like POPL.

Plenary

This program is tentative and subject to change.

You're viewing the program in a time zone which is different from your device's time zone change time zone

Mon 12 Jan

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

10:30 - 11:00
10:30
30m
Coffee break
Break
POPL Catering

11:00 - 12:30
Session 1TPSA at Salle 13
11:00
45m
Keynote
Keynote: Subarno Barnerjee AWS
TPSA
Subarno Banerjee Amazon Web Services
11:45
22m
Talk
Tracking Dynamically Bound Variable Dependencies
TPSA
12:07
23m
Talk
Gradually Retrofitting Assurance into Systems Software: A Separation-Logic Approach
TPSA
Rini Banerjee University of Cambridge, Zain K Aamer University of Pennsylvania, Hiroyuki Katsura University of Cambridge, David Kaloper-Meršinjak University of Cambridge, Dimitrios J. Economou University of Cambridge, Kayvan Memarian University of Cambridge, Dhruv Makwana University of Cambridge, Neel Krishnaswami University of Cambridge, Benjamin C. Pierce University of Pennsylvania, Christopher Pulte University of Cambridge, Peter Sewell University of Cambridge
12:30 - 14:00
12:30
90m
Lunch
Lunch
POPL Catering

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
15:30 - 16:00
15:30
30m
Coffee break
Break
POPL Catering

16:00 - 17:30
Session 3TPSA at Salle 13
16:00
22m
Talk
How to identify security vulnerabilities in Node.js packages?
TPSA
José Fragoso Santos INESC-ID; Instituto Superior Técnico - University of Lisbon
16:22
22m
Talk
Modeling Incorrectness and Unknown Functions with Angelic and Demonic Nondeterminism
TPSA
Noam Zilberstein Cornell University
16:45
22m
Talk
A logic for all reasons
TPSA
Flavio Ascari University of Konstanz, Roberto Bruni University of Pisa, Lorenzo Gazzella Università di Pisa, Roberta Gori Diaprtimento di Informatica, Universita' di Pisa, Italy
17:07
22m
Talk
AMPLE: Fine-grained File Access Policies for Server Applications
TPSA
Seyedhamed Ghavamnia Bloomberg, Julien Vanegue Imperial College London; Bloomberg

Call for Presentations

We invite the submission of talk proposals in topics related to both the mathematical foundations and practical implementations of static analysis. This workshop will not have formal proceedings, so talks covering in-progress or already published work are welcome. Since analysis tools and algorithms are difficult to implement, we also welcome speculative presentations about techniques that are not yet validated. The topics in scope include, but are not limited to:

  • Logical foundations for analysis algorithms (e.g. program logics, abstract interpretation, separation logic, etc)
  • Emerging problems and use cases for static analysis (with or without proposed solutions)
  • Prototype analysis tools
  • Incorrectness, under-approximation, and bug-finding
  • Analysis with computational effects (e.g., probabilistic, quantum, or concurrent programming)
  • Industrial experience reports

Submissions

Submissions should be in the form of extended abstracts and must not exceed three pages (excluding references) in the SIGPLAN two-column format.

The submission website is: https://tpsa26.hotcrp.com