PLDI 2026
Mon 15 - Fri 19 June 2026 Boulder, Colorado, United States
PLDI 2026 (series) / Limelight Boulder /

Room information: Flatirons 2

VenueLimelight Boulder
Room nameFlatirons 2
Floor1
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

Wed 17 Jun

Displayed time zone: Mountain Time (US & Canada) change

10:30 - 12:10
Mechanized Program Logics and VerificationPLDI Research Papers at Flatirons 2
10:30
20m
Talk
A Deductive System for Contract Satisfaction Proofs
PLDI Research Papers
Arthur Correnson CISPA Helmholtz Center for Information Security, Haoyi Zeng Harvard University, Jana Hofmann MPI-SP
DOI
10:50
20m
Talk
A Mechanized Algebra of Verified Data Structures for Optimizing Sparse Tensor Programs
PLDI Research Papers
Amanda Liu Massachusetts Institute of Technology, Gilbert Louis Bernstein University of Washington, Shoaib Kamil Adobe, Adam Chlipala Massachusetts Institute of Technology, Jonathan Ragan-Kelley Massachusetts Institute of Technology
DOI
11:10
20m
Talk
Iris-WasmFX: Modular Reasoning for Wasm Stack Switching
PLDI Research Papers
Maxime Legoupil Nanyang Technological University, Mathias Pedersen Aarhus University, Lars Birkedal Aarhus University, Sam Lindley University of Edinburgh, Jean Pichon-Pharabod Aarhus University
DOI
11:30
20m
Talk
Code-Specify-Test-Debug-Prove: Flexibly Integrating Separation Logic Specification into Conventional Workflows
PLDI Research Papers
Zain K Aamer University of Pennsylvania, Rini Banerjee University of Cambridge, 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 Oxford, Peter Sewell University of Cambridge
DOI Pre-print
11:50
20m
Talk
Cerisier: A Program Logic for Attestation in a Capability Machine
PLDI Research Papers
June Rousseau Aarhus University, Denis Carnier KU Leuven, Thomas Van Strydonck Fortanix, Steven Keuchel KU Leuven, Dominique Devriese KU Leuven, Lars Birkedal Aarhus University
DOI
13:40 - 15:20
Verification and Synthesis of Distributed SystemsPLDI Research Papers at Flatirons 2
13:40
20m
Talk
MatchBox: A Semantic Foundation for Data Plane Portability
PLDI Research Papers
Eric Hayden Campbell University of Texas at Austin, Robert Zhang University of Texas at Austin, Divyanshu Saxena University of Texas at Austin, Aditya Akella University of Texas at Austin, Işıl Dillig University of Texas at Austin
DOI
14:00
20m
Talk
Weighted NetKAT: A Programming Language For Quantitative Network Verification
PLDI Research Papers
Emmanuel Suárez Acevedo Cornell University, Tiago Ferreira University College London, Kevin Batz Cornell University, Oliver Emil Bøving Technical University of Denmark, Nate Foster EPFL; Jane Street, Alexandra Silva Cornell University
DOI
14:20
20m
Talk
SureDistrib: Verifying Almost-Sure Termination of Composite Asynchronous Byzantine Protocols
PLDI Research Papers
Longfei Qiu Yale University, Jingqi Xiao University of Hong Kong, Ji-Yong Shin Northeastern University, Zhong Shao Yale University
DOI
14:40
20m
Talk
Implementability of Global Distributed Protocols Modulo Network Architectures
PLDI Research Papers
Elaine Li New York University, Thomas Wies New York University
DOI
15:50 - 17:30
Advances in Abstract InterpretationPLDI Research Papers at Flatirons 2
15:50
20m
Talk
Path-Sensitive Abstract Interpretation for WCET Estimation
PLDI Research Papers
Shangshang Xiao Shandong University, Mengxia Sun Shandong University, Wei Zhang Shandong University, Naijun Zhan Peking University; Zhongguancun Laboratory, Lei Ju Shandong University
DOI
16:10
20m
Talk
SAIL: Sound Abstract Interpreters with LLMs
PLDI Research Papers
Qiuhan Gu University of Illinois Urbana-Champaign, Avaljot Singh University of Illinois Urbana-Champaign, Gagandeep Singh University of Illinois Urbana-Champaign
DOI
16:30
20m
Talk
Evolving Abstract Transformers for Gradient-Guided, Adaptable Abstract Interpretation
PLDI Research Papers
Shaurya Gomber University of Illinois Urbana-Champaign, Debangshu Banerjee University of Illinois Urbana-Champaign, Gagandeep Singh University of Illinois Urbana-Champaign
DOI Pre-print
16:50
20m
Talk
Abstract Interpretation with Confidence
PLDI Research Papers
Yuanfeng Shi Peking University, Ziyue Jin Peking University, Xin Zhang Peking University
DOI
17:10
20m
Talk
Optimism in Equality Saturation
PLDI Research Papers
Russel Arbore University of California at Berkeley, Alvin Cheung University of California at Berkeley, Max Willsey University of California at Berkeley
DOI Pre-print

Thu 18 Jun

Displayed time zone: Mountain Time (US & Canada) change

10:30 - 12:10
Symbolic Methods for Verification and MatchingPLDI Research Papers at Flatirons 2
10:30
20m
Talk
Solvable Tuple Patterns and Their Applications to Program Verification
PLDI Research Papers
Naoki Kobayashi University of Tokyo, Ryosuke Sato Tokyo University of Agriculture and Technology, Ayumi Shinohara Tohoku University, Ryo Yoshinaka Tohoku University
DOI
10:50
20m
Talk
Towards Efficient Matching of Regexes with Backreferences using Register Set Automata
PLDI Research Papers
Vojtěch Havlena Brno University of Technology, Lukáš Holík Brno University of Technology; Aalborg University, Ondřej Lengál Brno University of Technology, Jan Vašák Brno University of Technology, Sabína Gulčíková Brno University of Technology
DOI
11:10
20m
Talk
An Efficient Algorithm for Streaming BPE Tokenization
PLDI Research Papers
Konstantinos Mamouras Rice University, Angela W. Li Rice University, Yudi Yang Rice University
DOI
11:30
20m
Talk
Scalable Floating-Point Satisfiability via Staged Optimization
PLDI Research Papers
Yuanzhuo Zhang Virginia Tech, Zhoulai Fu SUNY Korea; Virginia Tech; Stony Brook University, Binoy Ravindran Virginia Tech
DOI
11:50
20m
Talk
EREQ: Regular Expressions with Quantifiers and Incremental Quantifier Elimination
PLDI Research Papers
Ekaterina Zhuchko Tallinn University of Technology, Ian Erik Varatalu Tallinn University of Technology, Margus Veanes Microsoft Research, Nikolaj Bjørner Microsoft Research
DOI
13:40 - 15:20
Semantics and Hyperproperty ReasoningPLDI Research Papers at Flatirons 2
13:40
20m
Talk
Towards Removing Undef Values from LLVM IR
PLDI Research Papers
Pedro Lobo INESC-ID; Instituto Superior Técnico - University of Lisbon, John McIver Virginia Tech, George Mitenkov Aptos, Juneyoung Lee AWS, Kirshanthan Sundararajah Virginia Tech, Nuno P. Lopes INESC-ID; Instituto Superior Técnico - University of Lisbon
DOI Pre-print
14:00
20m
Talk
The Downgrading Semantics of Memory Safety
PLDI Research Papers
René Rydhof Hansen Aalborg University, Andreas Stenbæk Larsen Aarhus University, Aslan Askarov Aarhus University
DOI
14:20
20m
Talk
Causality and Semantic Separation
PLDI Research Papers
Anna Zhang Massachusetts Institute of Technology, Qinglan Luo Wellesley College; Massachusetts Institute of Technology, London Bielicke University of California at Los Angeles, Eunice Jun University of California at Los Angeles, Adam Chlipala Massachusetts Institute of Technology
DOI
14:40
20m
Talk
Hyper Separation Logic
PLDI Research Papers
Trayan Gospodinov INSAIT at Sofia University St. Kliment Ohridski, Peter Müller ETH Zurich, Thibault Dardinier EPFL
DOI
15:00
20m
Talk
Pantomime: Constructive Leakage Proofs via Simulation
PLDI Research Papers
Robin Webbers Vrije Universiteit Amsterdam, Robert Schenck Northeastern University, Wind Wong Vrije Universiteit Amsterdam, Kristina Sojakova Vrije Universiteit Amsterdam, Klaus von Gleissenthall Vrije Universiteit Amsterdam
DOI

Fri 19 Jun

Displayed time zone: Mountain Time (US & Canada) change

10:30 - 12:10
Verified and Robust Program AnalysisPLDI Research Papers at Flatirons 2
10:30
20m
Talk
Verifying Array Properties in Pure Data-Parallel Programs
PLDI Research Papers
Nikolaj Hey Hinnerskov University of Copenhagen, Robert Schenck Northeastern University, Cosmin E. Oancea University of Copenhagen
DOI
10:50
20m
Talk
Soteria: Efficient Symbolic Execution as a Functional Library
PLDI Research Papers
Sacha-Élie Ayoun Imperial College London; Soteria Tools, Opale Sjöstedt Imperial College London; Soteria Tools, Azalea Raad Imperial College London; Soteria Tools
DOI
11:10
20m
Talk
A Categorical Basis for Robust Program Analysis
PLDI Research Papers
Zachary Kincaid Princeton University, Shaowei Zhu Princeton University
DOI
11:30
20m
Talk
Restart and Refine: Scalable IFDS Taint Analysis across Memory Budgets
PLDI Research Papers
Yujiang Gui UNSW, Yonggang Tao UNSW, Jingling Xue UNSW
DOI
11:50
20m
Talk
Synthesizing Backward Error Bounds, Backward
PLDI Research Papers
Laura Zielinski Cornell University, Justin Hsu Cornell University
DOI
13:40 - 15:20
Compositional Verification and Proof ReasoningPLDI Research Papers at Flatirons 2
13:40
20m
Talk
Heterogeneous Dynamic Logic: Provability Modulo Program Theories
PLDI Research Papers
Samuel Teuber KIT, Mattias Ulbrich KIT, André Platzer KIT, Bernhard Beckert KIT
DOI
14:00
20m
Talk
Intrinsically Correct Algorithms and Recursive Coalgebras
PLDI Research Papers
Cass Alexandru RPTU Kaiserslautern-Landau, Henning Urbat Friedrich-Alexander University Erlangen-Nürnberg, Thorsten Wißmann Friedrich-Alexander University Erlangen-Nürnberg
DOI
14:20
20m
Talk
CRIS: The Power of Imagination in Hybrid Verification
PLDI Research Papers
Yonghee Kim Seoul National University, Taeyoung Yoon Seoul National University, Sanghyun Yi Seoul National University, Jaehyung Lee Seoul National University, Soonwon Moon Seoul National University, Yeji Han Seoul National University, Seonho Lee Seoul National University, Taeyoung Rhee Seoul National University, Yujin Im Seoul National University, Donghyun Nam Seoul National University, Jieung Kim Yonsei University, Chung-Kil Hur Seoul National University
DOI
14:40
20m
Talk
Navigating AND–OR Graph Modifications to Debug Failing Proof Search
PLDI Research Papers
Justin Lubin University of California at Berkeley, Marlena Preigh University of California at Berkeley, Max Willsey University of California at Berkeley, Sarah E. Chasins University of California at Berkeley
DOI
15:00
20m
Talk
[TOPLAS] Project Everest: Perspectives from Developing Industrial-Grade High-Assurance Software
PLDI Research Papers
Danel Ahman University of Ljubljana, Karthikeyan Bhargavan Cryspen, France, Barry Bond , Jay Bosamiya Microsoft Research, Christopher Brzuska , Antoine Delignat-Lavaud Microsoft Research, n.n., Cédric Fournet Microsoft Research, Aymeric Fromherz Inria, Sydney Gibson , Chris Hawblitzel Microsoft Research, Cătălin Hriţcu MPI-SP, Markulf Kohlweiss , Guido Martínez Microsoft Research, Haobin Ni University of Washington, Bryan Parno Carnegie Mellon University, Jonathan Protzenko Microsoft Azure Research, Tahina Ramananandro Microsoft Research, Aseem Rastogi Microsoft Research, Exequiel Rivas Tallinn University of Technology, Nikhil Swamy Microsoft Research, Santiago Zanella-Béguelin Microsoft Research, Cambridge
15:50 - 17:10
Semantic Optimization of Data PipelinesPLDI Research Papers at Flatirons 2
15:50
20m
Talk
[SIGPLAN] Homomorphism Calculus for User-Defined Aggregations
PLDI Research Papers
Ziteng Wang University of Texas at Austin, Ruijie Fang University of Texas at Austin, Linus Zheng University of Texas at Austin, Dixin Tang University of Texas at Austin, Işıl Dillig University of Texas at Austin
16:10
20m
Talk
Bonsai: Compiling Queries to Pruned Tree Traversals
PLDI Research Papers
Alexander J Root Stanford University, Christophe Gyurgyik Stanford University, Purvi Goel Stanford University, Kayvon Fatahalian Stanford University, Jonathan Ragan-Kelley Massachusetts Institute of Technology, Andrew Adams Adobe Research, Fredrik Kjolstad Stanford University
DOI Pre-print
16:30
20m
Talk
A Compiler for Fused Relational Operations on Multisets
PLDI Research Papers
James Dong Stanford University, Fredrik Kjolstad Stanford University
DOI
16:50
20m
Talk
Optimal Predicate Pushdown Synthesis
PLDI Research Papers
Robert Zhang University of Texas at Austin, Eric Hayden Campbell University of Texas at Austin, Dixin Tang University of Texas at Austin, Işıl Dillig University of Texas at Austin
DOI

Mon 15 Jun

Displayed time zone: Mountain Time (US & Canada) change

Room9:003010:003011:003012:003013:003014:003015:003016:0030
Flatirons 2

PROPL

PROPL

Tue 16 Jun

Displayed time zone: Mountain Time (US & Canada) change

Room9:003010:003011:003012:003013:003014:003015:003016:0030
Flatirons 2

SOAP

SOAP

Wed 17 Jun

Displayed time zone: Mountain Time (US & Canada) change

Room10:003011:003012:003013:003014:003015:003016:003017:0030
Flatirons 2

PLDI Research Papers

Mechanized Program Logics and Verification

PLDI Research Papers

Verification and Synthesis of Distributed Systems

PLDI Research Papers

Advances in Abstract Interpretation

Thu 18 Jun

Displayed time zone: Mountain Time (US & Canada) change

Room10:003011:003012:003013:003014:003015:0030
Flatirons 2

PLDI Research Papers

Symbolic Methods for Verification and Matching

PLDI Research Papers

Semantics and Hyperproperty Reasoning

Fri 19 Jun

Displayed time zone: Mountain Time (US & Canada) change

Room10:003011:003012:003013:003014:003015:003016:003017:0030
Flatirons 2

PLDI Research Papers

Verified and Robust Program Analysis

PLDI Research Papers

Compositional Verification and Proof Reasoning

PLDI Research Papers

Semantic Optimization of Data Pipelines

Wed 17 Jun

Displayed time zone: Mountain Time (US & Canada) change

Room10:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:00153045
Flatirons 2
PLDI Research Papers
A Deductive System for Contract Satisfaction Proofs
10:30 - 10:50
PLDI Research Papers
A Mechanized Algebra of Verified Data Structures for Optimizing Sparse ...
10:50 - 11:10
PLDI Research Papers
Iris-WasmFX: Modular Reasoning for Wasm Stack Switching
11:10 - 11:30
PLDI Research Papers
Code-Specify-Test-Debug-Prove: Flexibly Integrating Separation Logic Sp ...
11:30 - 11:50
PLDI Research Papers
Cerisier: A Program Logic for Attestation in a Capability Machine
11:50 - 12:10
PLDI Research Papers
MatchBox: A Semantic Foundation for Data Plane Portability
13:40 - 14:00
PLDI Research Papers
Weighted NetKAT: A Programming Language For Quantitative Network Verifi ...
14:00 - 14:20
PLDI Research Papers
SureDistrib: Verifying Almost-Sure Termination of Composite Asynchronou ...
14:20 - 14:40
PLDI Research Papers
Implementability of Global Distributed Protocols Modulo Network Archite ...
14:40 - 15:00
PLDI Research Papers
Path-Sensitive Abstract Interpretation for WCET Estimation
15:50 - 16:10
PLDI Research Papers
SAIL: Sound Abstract Interpreters with LLMs
16:10 - 16:30
PLDI Research Papers
Evolving Abstract Transformers for Gradient-Guided, Adaptable Abstract ...
16:30 - 16:50
PLDI Research Papers
Abstract Interpretation with Confidence
16:50 - 17:10
PLDI Research Papers
Optimism in Equality Saturation
17:10 - 17:30

Thu 18 Jun

Displayed time zone: Mountain Time (US & Canada) change

Room10:0015304511:0015304512:0015304513:0015304514:0015304515:00153045
Flatirons 2
PLDI Research Papers
Solvable Tuple Patterns and Their Applications to Program Verification
10:30 - 10:50
PLDI Research Papers
Towards Efficient Matching of Regexes with Backreferences using Registe ...
10:50 - 11:10
PLDI Research Papers
An Efficient Algorithm for Streaming BPE Tokenization
11:10 - 11:30
PLDI Research Papers
Scalable Floating-Point Satisfiability via Staged Optimization
11:30 - 11:50
PLDI Research Papers
EREQ: Regular Expressions with Quantifiers and Incremental Quantifier E ...
11:50 - 12:10
PLDI Research Papers
Towards Removing Undef Values from LLVM IR
13:40 - 14:00
PLDI Research Papers
The Downgrading Semantics of Memory Safety
14:00 - 14:20
PLDI Research Papers
Causality and Semantic Separation
14:20 - 14:40
PLDI Research Papers
Hyper Separation Logic
14:40 - 15:00
PLDI Research Papers
Pantomime: Constructive Leakage Proofs via Simulation
15:00 - 15:20

Fri 19 Jun

Displayed time zone: Mountain Time (US & Canada) change

Room10:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:00153045
Flatirons 2
PLDI Research Papers
Verifying Array Properties in Pure Data-Parallel Programs
10:30 - 10:50
PLDI Research Papers
Soteria: Efficient Symbolic Execution as a Functional Library
10:50 - 11:10
PLDI Research Papers
A Categorical Basis for Robust Program Analysis
11:10 - 11:30
PLDI Research Papers
Restart and Refine: Scalable IFDS Taint Analysis across Memory Budgets
11:30 - 11:50
PLDI Research Papers
Synthesizing Backward Error Bounds, Backward
11:50 - 12:10
PLDI Research Papers
Heterogeneous Dynamic Logic: Provability Modulo Program Theories
13:40 - 14:00
PLDI Research Papers
Intrinsically Correct Algorithms and Recursive Coalgebras
14:00 - 14:20
PLDI Research Papers
CRIS: The Power of Imagination in Hybrid Verification
14:20 - 14:40
PLDI Research Papers
Navigating AND–OR Graph Modifications to Debug Failing Proof Search
14:40 - 15:00
PLDI Research Papers
[TOPLAS] Project Everest: Perspectives from Developing Industrial-Grade ...
15:00 - 15:20
PLDI Research Papers
[SIGPLAN] Homomorphism Calculus for User-Defined Aggregations
15:50 - 16:10
PLDI Research Papers
Bonsai: Compiling Queries to Pruned Tree Traversals
16:10 - 16:30
PLDI Research Papers
A Compiler for Fused Relational Operations on Multisets
16:30 - 16:50
PLDI Research Papers
Optimal Predicate Pushdown Synthesis
16:50 - 17:10