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

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:30
Creusot: Formal verification of Rust programsTutorials at Salle 12
09:00
90m
Tutorial
Creusot: Formal verification of Rust programs
Tutorials
Li-yao Xia LMF, Inria, Université Paris-Saclay, Jacques-Henri Jourdan CNR, LMF, Arnaud Golfouse Université Paris-Saclay, CNRS, ENS Paris-Saclay, Inria, Laboratoire des méthodes formelles, 91190, Gif-sur-Yvette, France, Vincent Lafeychine Université Paris-Saclay
09:00 - 10:30
BINSEC: Adapting Symbolic Execution for Binary-level SecurityTutorials at Salle 14
09:00
90m
Tutorial
BINSEC: Adapting Symbolic Execution for Binary-level Security
Tutorials
Sébastien Bardin CEA LIST, University Paris-Saclay, Frédéric Recoules CEA, List, Yanis Sellami CEA, List, Univ. Grenoble Alpes
11:00 - 12:30
Creusot: Formal verification of Rust programsTutorials at Salle 12
11:00
90m
Tutorial
Creusot: Formal verification of Rust programs
Tutorials
Li-yao Xia LMF, Inria, Université Paris-Saclay, Jacques-Henri Jourdan CNR, LMF, Arnaud Golfouse Université Paris-Saclay, CNRS, ENS Paris-Saclay, Inria, Laboratoire des méthodes formelles, 91190, Gif-sur-Yvette, France, Vincent Lafeychine Université Paris-Saclay
11:00 - 12:30
BINSEC: Adapting Symbolic Execution for Binary-level SecurityTutorials at Salle 14
11:00
90m
Tutorial
BINSEC: Adapting Symbolic Execution for Binary-level Security
Tutorials
Sébastien Bardin CEA LIST, University Paris-Saclay, Frédéric Recoules CEA, List, Yanis Sellami CEA, List, Univ. Grenoble Alpes
14:00 - 15:30
Verifying Probabilistic Programs Using Separation LogicTutorials at Salle 12
14:00
90m
Tutorial
Verifying Probabilistic Programs Using Separation Logic
Tutorials
Alejandro Aguirre Aarhus University, Simon Oddershede Gregersen New York University, Philipp G. Haselwarter Aarhus University
14:00 - 15:30
Discrete and continuous models for concurrent systemsTutorials at Salle 14
14:00
90m
Tutorial
Discrete and Continuous Models for Concurrent Systems: From Petri Nets to Directed Spaces
Tutorials
Uli Fahrenberg Université Paris-Saclay, CNRS, ENS Paris-Saclay, LMF
16:00 - 17:30
Verifying Probabilistic Programs Using Separation LogicTutorials at Salle 12
16:00
90m
Tutorial
Verifying Probabilistic Programs Using Separation Logic
Tutorials
Alejandro Aguirre Aarhus University, Simon Oddershede Gregersen New York University, Philipp G. Haselwarter Aarhus University
16:00 - 17:30
Discrete and continuous models for concurrent systemsTutorials at Salle 14
16:00
90m
Tutorial
Discrete and Continuous Models for Concurrent Systems: From Petri Nets to Directed Spaces
Tutorials
Uli Fahrenberg Université Paris-Saclay, CNRS, ENS Paris-Saclay, LMF

Mon 12 Jan

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

09:00 - 10:30
Syntactically and Semantically Constraining LLMsTutorials at Salle 20
09:00
90m
Tutorial
Syntactically and Semantically Constraining LLMs with Guarantees using Structured LLM Generation
Tutorials
Sasa Misailovic University of Illinois at Urbana-Champaign, Gagandeep Singh University of Illinois at Urbana-Champaign; VMware Research, Shubham Ugare Meta, Debangshu Banerjee UIUC, Tarun Suresh , Adharsh Kamath UIUC
11:00 - 12:30
Syntactically and Semantically Constraining LLMsTutorials at Salle 20
11:00
90m
Tutorial
Syntactically and Semantically Constraining LLMs with Guarantees using Structured LLM Generation
Tutorials
Sasa Misailovic University of Illinois at Urbana-Champaign, Gagandeep Singh University of Illinois at Urbana-Champaign; VMware Research, Shubham Ugare Meta, Debangshu Banerjee UIUC, Tarun Suresh , Adharsh Kamath UIUC
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
14:00 - 15:30
Veil: Automated and Interactive Verification of Transition SystemsTutorials at Salle 20
14:00
90m
Tutorial
Veil: Automated and Interactive Verification of Transition Systems
Tutorials
George Pîrlea National University of Singapore, Singapore, Qiyuan Zhao National University of Singapore
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
16:00 - 17:30
Veil: Automated and Interactive Verification of Transition SystemsTutorials at Salle 20
16:00
90m
Tutorial
Veil: Automated and Interactive Verification of Transition Systems
Tutorials
George Pîrlea National University of Singapore, Singapore, Qiyuan Zhao National University of Singapore

Tue 13 Jan

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

09:00 - 10:30
Analyzing Shell ScriptsTutorials at Salle 14
09:00
90m
Tutorial
Analyzing Shell Scripts
Tutorials
Michael Greenberg Stevens Institute of Technology, Konstantinos Kallas University of California, Los Angeles, Nikos Vasilakis Brown University
11:00 - 12:30
Analyzing Shell ScriptsTutorials at Salle 14
11:00
90m
Tutorial
Analyzing Shell Scripts
Tutorials
Michael Greenberg Stevens Institute of Technology, Konstantinos Kallas University of California, Los Angeles, Nikos Vasilakis Brown University
14:00 - 15:30
Is Program Synthesis Soluble in Large Language Models?Tutorials at Salle 14
14:00
90m
Tutorial
Is Program Synthesis Soluble in Large Language Models?
Tutorials
Nathanaël Fijalkow CNRS, LaBRI, University of Bordeaux
16:00 - 17:30
Is Program Synthesis Soluble in Large Language Models?Tutorials at Salle 14
16:00
90m
Tutorial
Is Program Synthesis Soluble in Large Language Models?
Tutorials
Nathanaël Fijalkow CNRS, LaBRI, University of Bordeaux