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

Room information: Horizons

Venuele Couvent des Jacobins
Room nameHorizons
Floor2
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:30
Session 1Dafny at Horizons
09:00
12m
Day opening
Day opening
Dafny
Stefan Zetzsche Amazon Web Services, Yannick Moy ANSSI
09:12
60m
Keynote
Software Verification meets Real-World Cryptography
Dafny
Karthikeyan Bhargavan Cryspen, France
10:12
18m
Talk
The Design of an Interactive Proof Mode for Dafny
Dafny
Ștefan Ciobâcă Alexandru Ioan Cuza University of Iasi, K. Rustan M. Leino Amazon, Ștefan Mercaș Alexandru Ioan Cuza University, Iasi, Romania, Roxana-Mihaela Timon Alexandru Ioan Cuza University, Iasi, Romania
11:00 - 12:30
Session 2Dafny at Horizons
11:00
18m
Talk
Diagnostics in Probabilistic Program Verification
Dafny
Philipp Schröer RWTH Aachen University, Darion Haase RWTH Aachen University, Joost-Pieter Katoen RWTH Aachen University
11:18
18m
Talk
Explicit Abstraction Barrier for Autoactive Verification
Dafny
Paul Patault Université Paris-Saclay - Laboratoire de Méthodes Formelles
Pre-print
11:36
18m
Talk
Managing the Proof Context in SPARK
Dafny
Claire Dross AdaCore, Joffrey Huguet AdaCore, Johannes Kanig AdaCore
11:54
18m
Talk
Tunable Automation in Automated Program Verification
Dafny
Alexander Bai New York University, Chris Hawblitzel Microsoft Research, Andrea Lattuada VMware Research
12:12
18m
Talk
Velvet: A Multi-Modal Verifier for Effectful Programs
Dafny
Vladimir Gladshtein , George Pîrlea National University of Singapore, Qiyuan Zhao National University of Singapore, Vitaly Kurin Neapolis University Pafos, Ilya Sergey National University of Singapore
Pre-print
14:00 - 15:30
Session 3Dafny at Horizons
14:00
18m
Talk
Lessons from Building an Auto-Active Verifier in Lean
Dafny
George Pîrlea National University of Singapore, Vladimir Gladshtein , Qiyuan Zhao National University of Singapore, Ilya Sergey National University of Singapore
Pre-print
14:18
18m
Talk
Formal Verification of Minimax Algorithms
Dafny
Wieger Wesselink Eindhoven University of Technology, Kees Huizing Eindhoven University of Technology, Huub van de Wetering Eindhoven University of Technology
14:36
18m
Talk
Teaching Automata Theory and Formal Languages with Dafny
Dafny
Ran Ettinger NVIDIA and Ben-Gurion University of the Negev and Israel Academic College in Ramat Gan
14:54
18m
Talk
Verification of E-Voting Algorithms in Dafny
Dafny
Robert Büttner University of Regensburg, Fabian Franz Dießl University of Regensburg, Patrick Janoschek University of Regensburg, Ivana Kostadinovic University of Regensburg, Henrik Oback University of Regensburg, Kilian Voß University of Regensburg, Franziska Alber University of Regensburg, Roland Herrmann University of Regensburg, Sibylle Möhle University of Regensburg, Philipp Rümmer University of Regensburg and Uppsala University
15:12
18m
Talk
A Correct-by-Construction Checker for Validation of Railway Data
Dafny
Benoît Boyer Mitsubishi Electric R&D Centre Europe, Rennes, France, Noé Canva Inria Saclay & Université Paris-Saclay, Matteo Manighetti Inria & École Polytechnique, Claude Marché Inria Saclay & Université Paris-Saclay
16:00 - 18:00
Session 4Dafny at Horizons
16:00
18m
Talk
ATLAS: Automated Toolkit for Large-Scale Verified Code Synthesis
Dafny
Mantas Bakšys University of Cambridge, Stefan Zetzsche Amazon Web Services, Olivier Bouissou Amazon Web Services, Soonho Kong Amazon Web Services, Remi Delmas Amazon Web Services
16:18
18m
Talk
A benchmark for vericoding: formally verified program synthesis
Dafny
Sergiu Bursuc Beneficial AI Foundation, Theodore Ehrenborg Beneficial AI Foundation, Shaowei Lin Beneficial AI Foundation, Lăcrămioara Aștefănoaei Beneficial AI Foundation, Ionel Emilian Chiosa MIT, Jure Kukovec Beneficial AI Foundation, Alok Singh Beneficial AI Foundation, Oliver Butterley Beneficial AI Foundation, Adem Bizid MIT, Quinn Dougherty Beneficial AI Foundation, Miranda Zhao MIT, Max Tan MIT, Max Tegmark Massachusetts Institute of Technology
16:36
18m
Talk
DafnyPro: LLM-Assisted Automated Verification for Dafny Programs
Dafny
Debangshu Banerjee UIUC, Olivier Bouissou Amazon Web Services, Stefan Zetzsche Amazon Web Services
16:54
18m
Talk
MiniF2F-Dafny: LLM-Guided Mathematical Theorem Proving via Auto-Active Verification
Dafny
Mantas Bakšys University of Cambridge, Stefan Zetzsche Amazon Web Services, Olivier Bouissou Amazon Web Services
17:12
18m
Talk
Specification-Guided Repair of Arithmetic Errors in Dafny Programs using LLMs
Dafny
Valentina Wu Faculdade de Engenharia, Universidade do Porto, Alexandra Mendes Faculty of Engineering, University of Porto & INESC TEC, Alexandre Abreu INESC TEC, Faculdade de Engenharia, Universidade do Porto
17:30
18m
Talk
Toward Automated, Contamination-free Dafny Benchmark Generation
Dafny
Changjie Wang KTH Royal Institute of Technology, Mariano Scazzariello RISE Research Institutes of Sweden, Dejan Kostic KTH Royal Institute of Technology, Marco Chiesa KTH Royal Institute of Technology
17:48
12m
Day closing
Day closing
Dafny
Stefan Zetzsche Amazon Web Services, Yannick Moy ANSSI

Mon 12 Jan

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

09:00 - 10:30
Analysis 1VMCAI at Horizons
Chair(s): Thomas P. Jensen INRIA Rennes
09:00
60m
Keynote
Current State of the Industrial-Strength Infer Static Analysis Platform
VMCAI
David Pichardie Meta
10:00
30m
Talk
Try-Mopsa: Relational Static Analysis in Your Pocket
VMCAI
Raphaël Monat Inria and University of Lille
11:00 - 12:30
Analysis 2VMCAI at Horizons
Chair(s): Benoît Montagu Inria
11:00
30m
Talk
Data Race Detection by Digest-Driven Abstract Interpretation
VMCAI
Michael Schwarz National University of Singapore, Julian Erhard TU Munich; LMU Munich
11:30
30m
Talk
Termination Resilience Static Analysis
VMCAI
Naïm Moussaoui Remil Inria & ENS | PSL, Paris, France, Caterina Urban Inria Paris - ENS - Université PSL
12:00
30m
Talk
Forward Symbolic Execution for Trustworthy Automation of Binary Code Verification
VMCAI
Andreas Lindner Uppsala universitet, Karl Palmskog KTH Royal Institute of Technology, Scott Constable Intel Corporation, Mads Dam KTH, Roberto Guanciale KTH Royal Institute of Technology, Hamed Nemati KTH Royal Institute of Technology
14:00 - 15:30
Artificial InteligenceVMCAI at Horizons
Chair(s): Yu-Fang Chen Academia Sinica
14:00
60m
Keynote
Understanding Transformers through the Lens of Logic and Automata
VMCAI
Anthony Widjaja Lin TU Kaiserslautern; MPI-SWS
15:00
30m
Talk
Proof Minimization in Neural Network Verification
VMCAI
Omri Isac The Hebrew University of Jerusalem, Idan Refaeli Hebrew University of Jerusalem, Haoze Wu Stanford University, Clark Barrett Stanford University, Guy Katz The Hebrew University of Jerusalem
16:00 - 17:30
Models 1VMCAI at Horizons
16:00
30m
Talk
Verification of Generic VHDL Designs and Their Translation to Rocq
VMCAI
Ocan Sankur University of Rennes, France / Inria, France / CNRS, France / IRISA, France, Benoît Boyer Mitsubishi Electric R&D Centre Europe, Rennes, France, Florian Faissole Mitsubishi Electric R&D Centre Europe
16:30
30m
Talk
A Formal Executable Semantics of PROMELA
VMCAI
Byoungho Son POSTECH, Kyungmin Bae POSTECH
17:00
30m
Talk
Efficient Discovery of Actual Causality in Stochastic Systems
VMCAI
Arshia Rafieioskouei Michigan State University, Kenneth Rogale Michigan State University, Borzoo Bonakdarpour Michigan State University

Tue 13 Jan

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

09:00 - 10:30
Analysis 3VMCAI at Horizons
Chair(s): Ondřej Lengál Brno University of Technology
09:00
60m
Keynote
TypedC: Spatial Memory Safety for Low Level Programs by Abstract Interpretation
VMCAI
Mihaela Sighireanu University Paris-Saclay, ENS Paris-Saclay, CNRS, LMF
10:00
30m
Talk
Input-based Three-Valued Abstraction Refinement
VMCAI
Jan Onderka University of Freiburg, Stefan Ratschan The Czech Academy of Sciences
11:00 - 12:30
SolversVMCAI at Horizons
Chair(s): Borzoo Bonakdarpour Michigan State University
11:00
30m
Talk
Multi-variable Quantification of BDDs in External Memory using Nested Sweeping
VMCAI
Steffan Sølvsten Aarhus University, Jaco van de Pol Aarhus University
11:30
30m
Talk
Producing Shorter Congruence Closure Proofs in a State-of-the-Art SMT Solver
VMCAI
Bruno Andreotti Universidade Federal de Minas Gerais, Haniel Barbosa Universidade Federal de Minas Gerais
12:00
30m
Talk
SAT-Based Synthesis of Minimal Deterministic Real-Time Automata via 3DRTA Representation
VMCAI
Junjie Meng School of Computer Science and Technology, Tongji University, Jie An Institute of Software Chinese Academy of Sciences, Yong Li Institute of Software, Chinese Academy of Sciences, Andrea Turrini Institute of Software, Chinese Academy of Sciences, Miaomiao Zhang School of Computer Science and Technology, Tongji University
14:00 - 15:30
Models 2VMCAI at Horizons
14:00
30m
Talk
Atomic Gliders and Cellular Automata as Language Generators
VMCAI
Dana Fisman Ben-Gurion University, Noa Izsak CISPA Helmholtz Center for Information Security, Germany
14:30
30m
Talk
Reachability in multi-agent transfer systems
VMCAI
Nathalie Bertrand INRIA Rennes, Loic Helouet INRIA, Engel Lefaucheux Université de Lorraine; CNRS; Inria; LORIA, Luca Paparazzo Inria, IRISA, Université de Rennes
15:00
30m
Talk
A Hybrid Meta-Learning Framework for Adaptive Safe Controller Synthesis of Dynamical Models
VMCAI
Rui Guo Zhejiang Sci-Tech University, Yang Li Zhejiang Sci-Tech University, Xiuqing Cao Zhejiang Sci-Tech University, Wang Lin
16:00 - 17:30
Quantum and Probabilistic VerificationVMCAI at Horizons
Chair(s): Jyun-Ao Lin National Taipei University of Technology
16:00
30m
Talk
Efficiently Verifying Quantum Programs with Few T Gates
VMCAI
Youngchan Cho The University of Chicago, Robert Rand University of Chicago
16:30
30m
Talk
Finding Photonics Circuits via δ-weakening SMT
VMCAI
Marco Lewis Inria, Benoît Valiron Université Paris-Saclay, CNRS, CentraleSupélec, LMF
17:00
30m
Talk
Probabilistic Verification for Modular Network-on-Chip Systems
VMCAI
Nick Waddoups nick.waddoups@usu.edu, Jonah Boe Hill Air Force Base, Utah, Arnd Hartmanns University of Twente, Prabal Basu Utah State University, Sanghamitra Roy Utah State University, Koushik Chakraborty Utah State University, Zhen Zhang Utah State University

Sun 11 Jan

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

Room9:003010:003011:003012:003013:003014:003015:003016:003017:0030
Horizons

Dafny

Session 1

Dafny

Session 2

Dafny

Session 3

Dafny

Session 4

Mon 12 Jan

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

Room9:003010:003011:003012:003013:003014:003015:003016:003017:0030
Horizons

VMCAI

Analysis 1

VMCAI

Analysis 2

VMCAI

Artificial Inteligence

VMCAI

Models 1

Tue 13 Jan

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

Room9:003010:003011:003012:003013:003014:003015:003016:003017:0030
Horizons

VMCAI

Analysis 3

VMCAI

Solvers

VMCAI

Models 2

VMCAI

Quantum and Probabilistic Verification

Sun 11 Jan

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

Room9:0015304510:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:00153045
Horizons
Dafny
Day opening
09:00 - 09:12
Dafny
Software Verification meets Real-World Cryptography
09:12 - 10:12
Dafny
The Design of an Interactive Proof Mode for Dafny
10:12 - 10:30
Dafny
Diagnostics in Probabilistic Program Verification
11:00 - 11:18
Dafny
Explicit Abstraction Barrier for Autoactive Verification
11:18 - 11:36
Dafny
Managing the Proof Context in SPARK
11:36 - 11:54
Dafny
Tunable Automation in Automated Program Verification
11:54 - 12:12
Dafny
Velvet: A Multi-Modal Verifier for Effectful Programs
12:12 - 12:30
Dafny
Lessons from Building an Auto-Active Verifier in Lean
14:00 - 14:18
Dafny
Formal Verification of Minimax Algorithms
14:18 - 14:36
Dafny
Teaching Automata Theory and Formal Languages with Dafny
14:36 - 14:54
Dafny
Verification of E-Voting Algorithms in Dafny
14:54 - 15:12
Dafny
A Correct-by-Construction Checker for Validation of Railway Data
15:12 - 15:30
Dafny
ATLAS: Automated Toolkit for Large-Scale Verified Code Synthesis
16:00 - 16:18
Dafny
A benchmark for vericoding: formally verified program synthesis
16:18 - 16:36
Dafny
DafnyPro: LLM-Assisted Automated Verification for Dafny Programs
16:36 - 16:54
Dafny
MiniF2F-Dafny: LLM-Guided Mathematical Theorem Proving via Auto-Active ...
16:54 - 17:12
Dafny
Specification-Guided Repair of Arithmetic Errors in Dafny Programs usin ...
17:12 - 17:30
Dafny
Toward Automated, Contamination-free Dafny Benchmark Generation
17:30 - 17:48
Dafny
Day closing
17:48 - 18:00

Mon 12 Jan

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

Room9:0015304510:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:00153045
Horizons
VMCAI
Current State of the Industrial-Strength Infer Static Analysis Platform
09:00 - 10:00
VMCAI
Try-Mopsa: Relational Static Analysis in Your Pocket
10:00 - 10:30
VMCAI
Data Race Detection by Digest-Driven Abstract Interpretation
11:00 - 11:30
VMCAI
Termination Resilience Static Analysis
11:30 - 12:00
VMCAI
Forward Symbolic Execution for Trustworthy Automation of Binary Code Ve ...
12:00 - 12:30
VMCAI
Understanding Transformers through the Lens of Logic and Automata
14:00 - 15:00
VMCAI
Proof Minimization in Neural Network Verification
15:00 - 15:30
VMCAI
Verification of Generic VHDL Designs and Their Translation to Rocq
16:00 - 16:30
VMCAI
A Formal Executable Semantics of PROMELA
16:30 - 17:00
VMCAI
Efficient Discovery of Actual Causality in Stochastic Systems
17:00 - 17:30

Tue 13 Jan

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

Room9:0015304510:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:00153045
Horizons
VMCAI
TypedC: Spatial Memory Safety for Low Level Programs by Abstract Interp ...
09:00 - 10:00
VMCAI
Input-based Three-Valued Abstraction Refinement
10:00 - 10:30
VMCAI
Multi-variable Quantification of BDDs in External Memory using Nested S ...
11:00 - 11:30
VMCAI
Producing Shorter Congruence Closure Proofs in a State-of-the-Art SMT S ...
11:30 - 12:00
VMCAI
SAT-Based Synthesis of Minimal Deterministic Real-Time Automata via 3DR ...
12:00 - 12:30
VMCAI
Atomic Gliders and Cellular Automata as Language Generators
14:00 - 14:30
VMCAI
Reachability in multi-agent transfer systems
14:30 - 15:00
VMCAI
A Hybrid Meta-Learning Framework for Adaptive Safe Controller Synthesis ...
15:00 - 15:30
VMCAI
Efficiently Verifying Quantum Programs with Few T Gates
16:00 - 16:30
VMCAI
Finding Photonics Circuits via δ-weakening SMT
16:30 - 17:00
VMCAI
Probabilistic Verification for Modular Network-on-Chip Systems
17:00 - 17:30