POPL 2026
Sun 11 - Sat 17 January 2026 Rennes, France
POPL 2026 (series) / le Couvent des Jacobins /

Room information: Salle 19

Venuele Couvent des Jacobins
Room nameSalle 19
Floor2
Capacity70
Room InformationNo extra information available
Program

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

Sun 11 Jan

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

09:00 - 10:00
KeynotePriSC at Salle 19
09:00
20m
Day opening
Day opening
PriSC

09:20
20m
Keynote
The V8 Sandbox: From Compiler Correctness to Runtime Containment
PriSC
Samuel Groß Google
09:40
20m
Talk
Efficient Dependency Resolution in IFC-aware Decentralized Programming
PriSC
Steffan Sølvsten Aarhus University, Aslan Askarov Aarhus University
11:00 - 12:30
Secure Compilation & VerificationPriSC at Salle 19
11:00
18m
Talk
Mind the Boundary: Detecting Undefined Behavior Across Rust’s FFI
PriSC
Andreea Costea TU Delft
11:18
18m
Talk
Specifying ABIs with Realizability and Type-Preserving Compilation
PriSC
Brianna Marshall Northeastern University, Ryan Doenges Boston College, Owen Duckham Northeastern University, Ari Prakash Northeastern University, Maxime Legoupil Aarhus University, Elan Semenova Northeastern University, Lars Birkedal Aarhus University, Amal Ahmed Northeastern University, USA
11:36
18m
Talk
Towards formally secure compilation of verified F* programs against unverified ML contexts
PriSC
Cezar-Constantin Andrici MPI-SP, Danel Ahman University of Ljubljana, Cătălin Hriţcu MPI-SP, Guido Martínez Microsoft Research, Abigail Pribisova MPI-SP and MPI-SWS, Exequiel Rivas Tallinn University of Technology; Ahrefs, Théo Winterhalter INRIA
11:54
18m
Talk
Blame-aware Recomposition for Formally Secure Low-level Compiler Backends
PriSC
Basile Schlosser ENS Paris-Saclay, Jérémy Thibault EPFL, Cătălin Hriţcu MPI-SP
12:12
18m
Talk
WP-Preserving Compilation -- Preserving Weakest Preconditions For End-to-End Verification
PriSC
Carmine Abate Barkhausen Institute, Dresden, Mohamed Elsheikh Barkhausen Institute, Dresden, Kleio Liotati Barkhausen Institute, Dresden, Frantisek Farka Barkhausen Institute, Dresden, Sebastian Ertel Barkhausen Institute, Dresden
14:00 - 15:30
Timing Side ChannelsPriSC at Salle 19
14:00
18m
Talk
Fun with flags: How Compilers Break and Fix Constant-Time Code
PriSC
Antoine Geimer Univ. Lille, CNRS, Inria, Clémentine Maurice Univ. Lille, Inria, CNRS
14:18
18m
Talk
GnuZero: A Compiler-Based Zeroization Static Detection Tool for the Masses
PriSC
Pierrick Philippe Univ Rennes, CNRS, IRISA, Mohamed Sabt Univ Rennes, CNRS, IRISA, Pierre-Alain Fouque Univ Rennes, CNRS, IRISA
14:36
18m
Talk
Tooling Design and Lessons Learned from Systematic Evaluations of the Preservation of Low-level Security Properties by Compilers with BinSec
PriSC
Yanis Sellami CEA, List, Univ. Grenoble Alpes, Frédéric Recoules CEA, List, Sébastien Bardin CEA LIST, University Paris-Saclay
14:54
18m
Talk
Decompiling for Constant-Time Analysis
PriSC
Sören van der Wall TU Braunschweig, Santiago Arranz Olmos Max Planck Institute for Security and Privacy, Gilles Barthe MPI-SP; IMDEA Software Institute, Lionel Blatter Max Planck Institute for Security and Privacy, Youcef Bouzid , Zhiyuan Zhang
15:12
18m
Talk
Modular Verification of Probabilistic Constant-Time
PriSC
Xingyu Xie MPI-SP
16:00 - 17:30
Hardware SecurityPriSC at Salle 19
16:00
12m
Talk
FSLH: Flexible Mechanized Speculative Load Hardening
PriSC
Jonathan Baumann MPI-SP, Roberto Blanco Max Planck Institute for Security and Privacy (MPI-SP), Léon Ducruet Aarhus University, Sebastian Harwig MPI-SP and Ruhr University Bochum, Cătălin Hriţcu MPI-SP
16:12
12m
Talk
Towards Robust Secure Compilation in Presence of Speculative Execution
PriSC
Léopold Clément Télécom Paris, Ulrich Kühne Télécom Paris, Florian Brandner Télécom Paris, Renaud Pacalet Télécom Paris
16:25
12m
Talk
Compiling countermeasures against fault attacks with “Tracing LLVM”
PriSC
Sébastien Michelland Université Grenoble-Alpes - Grenoble INP - LCIS, Christophe Deleuze Université Grenoble-Alpes - Grenoble INP - LCIS, Laure Gonnord Université Grenoble-Alpes - Grenoble INP - LCIS
16:38
12m
Talk
Calling Conventions for Secure Stack Sharing on CHERI Capability Machines in Practice
PriSC
Elias Storme KU Leuven, Sander Huyghebaert Vrije Universiteit Brussel, Steven Keuchel KU Leuven, Thomas Van Strydonck KULeuven, Dominique Devriese KU Leuven
16:51
12m
Talk
Modular and automatic formal verification of a RISC-V processor with security mechanisms
PriSC
Pierre Wilke CentraleSupélec, Cyprien Jules CentraleSupélec, Inria, CNRS, Univ. Rennes, Guillaume Hiet CentraleSupélec, Inria, CNRS, Univ. Rennes
17:04
12m
Talk
Lightning Talks
PriSC

17:17
12m
Day closing
Day closing
PriSC

Mon 12 Jan

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

14:00 - 15:30
A Guided Tour through Oxidized OCamlTutorials at Salle 19
14:00
90m
Tutorial
A Guided Tour through Oxidized OCaml
Tutorials
Gavin Gray Brown University, Anil Madhavapeddy University of Cambridge, UK, KC Sivaramakrishnan IIT Madras and Tarides, Will Crichton Brown University, Shriram Krishnamurthi Brown University, Chris Casinghino Jane Street, Richard A. Eisenberg Jane Street
16:00 - 17:30
A Guided Tour through Oxidized OCamlTutorials at Salle 19
16:00
90m
Tutorial
A Guided Tour through Oxidized OCaml
Tutorials
Gavin Gray Brown University, Anil Madhavapeddy University of Cambridge, UK, KC Sivaramakrishnan IIT Madras and Tarides, Will Crichton Brown University, Shriram Krishnamurthi Brown University, Chris Casinghino Jane Street, Richard A. Eisenberg Jane Street

Tue 13 Jan

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

09:00 - 10:30
KeynotePEPM at Salle 19
09:00
5m
Day opening
Welcome
PEPM
Yukiyoshi Kameyama University of Tsukuba, Ningning Xie University of Toronto
09:05
85m
Keynote
TBD
PEPM

Sun 11 Jan

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

Room9:003010:003011:003012:003013:003014:003015:003016:003017:0030
Salle 19

PriSC

Keynote

PriSC

PriSC

Secure Compilation & Verification

PriSC

Timing Side Channels

PriSC

Hardware Security

PriSC

Mon 12 Jan

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

Room14:003015:003016:003017:0030
Salle 19

Tutorials

A Guided Tour through Oxidized OCaml

Tutorials

A Guided Tour through Oxidized OCaml

Tue 13 Jan

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

Room9:003010:003011:003012:003013:003014:003015:003016:003017:0030
Salle 19

PEPM

Keynote

PEPM

PEPM

PEPM

Sat 17 Jan

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

Room9:003010:003011:003012:003013:003014:003015:003016:003017:0030
Salle 19

GiacoFest

GiacoFest

GiacoFest

GiacoFest

Sun 11 Jan

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

Room9:0015304510:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:00153045
Salle 19
PriSC
Day opening
09:00 - 09:20
PriSC
The V8 Sandbox: From Compiler Correctness to Runtime Containment
09:20 - 09:40
PriSC
Efficient Dependency Resolution in IFC-aware Decentralized Programming
09:40 - 10:00
PriSC
Mind the Boundary: Detecting Undefined Behavior Across Rust’s FFI
11:00 - 11:18
PriSC
Specifying ABIs with Realizability and Type-Preserving Compilation
11:18 - 11:36
PriSC
Towards formally secure compilation of verified F* programs against unv ...
11:36 - 11:54
PriSC
Blame-aware Recomposition for Formally Secure Low-level Compiler Backends
11:54 - 12:12
PriSC
WP-Preserving Compilation -- Preserving Weakest Preconditions For End-t ...
12:12 - 12:30
PriSC
Fun with flags: How Compilers Break and Fix Constant-Time Code
14:00 - 14:18
PriSC
GnuZero: A Compiler-Based Zeroization Static Detection Tool for the Masses
14:18 - 14:36
PriSC
Tooling Design and Lessons Learned from Systematic Evaluations of the P ...
14:36 - 14:54
PriSC
Decompiling for Constant-Time Analysis
14:54 - 15:12
PriSC
Modular Verification of Probabilistic Constant-Time
15:12 - 15:30
PriSC
FSLH: Flexible Mechanized Speculative Load Hardening
16:00 - 16:12
PriSC
Towards Robust Secure Compilation in Presence of Speculative Execution
16:12 - 16:25
PriSC
Compiling countermeasures against fault attacks with “Tracing LLVM”
16:25 - 16:38
PriSC
Calling Conventions for Secure Stack Sharing on CHERI Capability Machin ...
16:38 - 16:51
PriSC
Modular and automatic formal verification of a RISC-V processor with se ...
16:51 - 17:04
PriSC
Lightning Talks
17:04 - 17:17
PriSC
Day closing
17:17 - 17:30

Mon 12 Jan

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

Room14:0015304515:0015304516:0015304517:00153045
Salle 19
POPL Tutorials
A Guided Tour through Oxidized OCaml
14:00 - 15:30
POPL Tutorials
A Guided Tour through Oxidized OCaml
16:00 - 17:30

Tue 13 Jan

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

Room9:0015304510:00153045
Salle 19
PEPM
Welcome
09:00 - 09:05
PEPM
TBD
09:05 - 10:30