PLDI 2025
Mon 16 - Fri 20 June 2025 Seoul, South Korea
PLDI 2025 (series) / The Westin Josun Seoul /

Room information: Grand Ball Room 1

VenueThe Westin Josun Seoul
Room nameGrand Ball Room 1
Floor1
Room Information

Grand Ball Room 1

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 18 Jun

Displayed time zone: Seoul change

10:30 - 12:10
Compilers 1PLDI Research Papers at Grand Ball Room 1
10:30
20m
Talk
Partial Evaluation, Whole-Program Compilation
PLDI Research Papers
Chris Fallin F5, Maxwell Bernstein Recurse Center
DOI
10:50
20m
Talk
Exploiting Undefined Behavior in C/C++ Programs for Optimization: A Study on the Performance Impact
PLDI Research Papers
Lucian Popescu INESC-ID; Instituto Superior Técnico - University of Lisbon; Politehnica University of Bucharest, Nuno P. Lopes INESC-ID; Instituto Superior Técnico - University of Lisbon
Link to publication DOI
11:10
20m
Talk
Relaxing Alias Analysis: Exploring the Unexplored Space
PLDI Research Papers
Michel Weber ETH Zurich, Theodoros Theodoridis ETH Zurich, Zhendong Su ETH Zurich
DOI
11:30
20m
Talk
Webs and Flow-Directed Well-Typedness Preserving Program Transformations
PLDI Research Papers
Benjamin Quiring University of Maryland, David Van Horn University of Maryland, John Reppy University of Chicago, Olin Shivers Northeastern University
DOI
11:50
20m
Talk
Slotted E-Graphs: First-Class Support for (Bound) Variables in E-Graphs
PLDI Research Papers
Rudi Schneider Technische Universität Berlin, Marcus Rossel Barkhausen Institut, Amir Shaikhha University of Edinburgh, Andrés Goens University of Amsterdam, Thomas Koehler CNRS - ICube Lab, Michel Steuwer Technische Universität Berlin
DOI
14:00 - 15:40
Security & CryptographyPLDI Research Papers at Grand Ball Room 1
14:00
20m
Talk
Verified Foundations for Differential Privacy
PLDI Research Papers
Markus de Medeiros New York University, Muhammad Naveed Amazon, Tancrède Lepoint Amazon, Temesghen Kahsai Amazon, Tristan Ravitch Amazon, Stefan Zetzsche Amazon, Anjali Joshi Amazon, Joseph Tassarotti New York University, Aws Albarghouthi Amazon, Jean-Baptiste Tristan Amazon
DOI
14:20
20m
Talk
Automated Exploit Generation for Node.js Packages
PLDI Research Papers
Filipe Marques INESC-ID; Instituto Superior Técnico - University of Lisbon, Mafalda Ferreira INESC-ID; Instituto Superior Técnico - University of Lisbon, André Nascimento INESC-ID; Instituto Superior Técnico - University of Lisbon, Miguel E. Coimbra INESC-ID; Instituto Superior Técnico - University of Lisbon, Nuno Santos INESC-ID; Instituto Superior Técnico - University of Lisbon, Limin Jia Carnegie Mellon University, José Fragoso Santos INESC-ID; Instituto Superior Técnico - University of Lisbon
DOI
14:40
20m
Talk
Robust Constant-Time Cryptography
PLDI Research Papers
Matthew Kolosick University of California at San Diego, Basavesh Ammanaghatta Shivakumar Virginia Tech, Sunjay Cauligi ICSI, Marco Patrignani University of Trento, Marco Vassena Utrecht University, Ranjit Jhala University of California at San Diego, Deian Stefan University of California at San Diego
DOI
15:00
20m
Talk
Smooth, Integrated Proofs of Cryptographic Constant Time for Nondeterministic Programs and Compilers
PLDI Research Papers
Owen Conoly Massachusetts Institute of Technology, Andres Erbsen Google, Adam Chlipala Massachusetts Institute of Technology
DOI
15:20
20m
Talk
Morello-Cerise: A Proof of Strong Encapsulation for the Arm Morello Capability Hardware Architecture
PLDI Research Papers
Angus Hammond University of Cambridge, Ricardo Almeida University of Glasgow, Thomas Bauereiss University of Cambridge, Brian Campbell University of Edinburgh, Ian Stark University of Edinburgh, Peter Sewell University of Cambridge
DOI
16:00 - 17:20
Big Red KATSPLDI Research Papers at Grand Ball Room 1
16:00
20m
Talk
Active Learning of Symbolic NetKAT Automata
PLDI Research Papers
Mark Moeller Cornell University, Tiago Ferreira University College London, Thomas Lu Cornell University, Nate Foster Cornell University; Jane Street, Alexandra Silva Cornell University
DOI
16:20
20m
Talk
StacKAT: Infinite State Network Verification
PLDI Research Papers
Jules Jacobs Cornell University, Nate Foster Cornell University; Jane Street, Tobias Kappé Leiden University, Dexter Kozen Cornell University, Lily Saada Cornell University, Alexandra Silva Cornell University, Jana Wagemaker Radboud University Nijmegen
DOI
16:40
20m
Talk
Probabilistic Kleene Algebra with Angelic Nondeterminism
PLDI Research Papers
Shawn Ong Cornell University, Stephanie Ma Cornell University, Dexter Kozen Cornell University
DOI
17:00
20m
Talk
Membership Testing for Semantic Regular Expressions
PLDI Research Papers
Yifei Huang University of Southern California, Matin Amini University of Southern California, Alexis Le Glaunec Rice University, Konstantinos Mamouras Rice University, Mukund Raghothaman University of Southern California
DOI

Thu 19 Jun

Displayed time zone: Seoul change

10:30 - 12:10
Verification 1PLDI Research Papers at Grand Ball Room 1
10:30
20m
Talk
A Hybrid Approach to Semi-automated Rust Verification
PLDI Research Papers
Sacha-Élie Ayoun Imperial College London, Xavier Denis ETH Zurich, Petar Maksimović Nethermind; Imperial College London, Philippa Gardner Imperial College London
DOI Pre-print
10:50
20m
Talk
RefinedProsa: Connecting Response-Time Analysis with C Verification for Interrupt-Free Schedulers
PLDI Research Papers
Kimaya Bedarkar Max Planck Institute for Software Systems (MPI-SWS), Laila Elbeheiry MPI-SWS, Michael Sammler ETH Zurich; ISTA, Lennard Gäher MPI-SWS, Björn Brandenburg MPI-SWS, Derek Dreyer MPI-SWS, Deepak Garg MPI-SWS
DOI
11:10
20m
Talk
Certified Compilers à la Carte
PLDI Research Papers
Oghenevwogaga Ebresafe University of Waterloo, Ian Zhao University of Waterloo, Ende Jin University of Waterloo, Arthur Bright University of Waterloo, Charles Jian University of Waterloo, Yizhou Zhang University of Waterloo
DOI
11:30
20m
Talk
Destabilizing Iris
PLDI Research Papers
Simon Spies MPI-SWS, Niklas Mück MPI-SWS, Haoyi Zeng Saarland University, Michael Sammler ETH Zurich; ISTA, Andrea Lattuada MPI-SWS, Peter Müller ETH Zurich, Derek Dreyer MPI-SWS
DOI
11:50
20m
Talk
Verifying Lock-Free Traversals in Relaxed Memory Separation Logic
PLDI Research Papers
Sunho Park KAIST, Jaehwang Jung Rebellions Inc, Janggun Lee KAIST, Jeehoon Kang KAIST
DOI
14:00 - 15:00
Automata TheoryPLDI Research Papers at Grand Ball Room 1
14:00
20m
Talk
A Uniform Framework for Handling Position Constraints in String Solving
PLDI Research Papers
Yu-Fang Chen Academia Sinica, Vojtěch Havlena Brno University of Technology, Michal Hečko Brno University of Technology, Lukáš Holík Brno University of Technology; Aalborg University, Ondřej Lengál Brno University of Technology
DOI
14:20
20m
Talk
Intrinsic Verification of Parsers and Formal Grammar Theory in Dependent Lambek Calculus
PLDI Research Papers
Steven Schaefer University of Michigan, Nathan Varner University of Michigan, Pedro Henrique Azevedo de Amorim University of Oxford, Max S. New University of Michigan
DOI
14:40
20m
Talk
Verifying Solutions to Semantics-Guided Synthesis Problems
PLDI Research Papers
Charlie Murphy Amazon Web Services, USA, Keith J.C. Johnson University of Wisconsin-Madison, Thomas Reps University of Wisconsin-Madison, Loris D'Antoni University of California at San Diego
DOI

Fri 20 Jun

Displayed time zone: Seoul change

10:30 - 12:10
Compilers 2PLDI Research Papers at Grand Ball Room 1
10:30
20m
Talk
Robustifying Debug Information Updates in LLVM via Control-Flow Conformance Analysis
PLDI Research Papers
Shan Huang East China Normal University, Jingjing Liang East China Normal University, Ting Su East China Normal University, Qirun Zhang Georgia Institute of Technology
DOI
10:50
20m
Talk
CompCertOC: Verified Compositional Compilation of Multi-threaded Programs with Shared Stacks
PLDI Research Papers
Ling Zhang Shanghai Jiao Tong University, Yuting Wang Shanghai Jiao Tong University, Yalun Liang Shanghai Jiao Tong University, Zhong Shao Yale University
DOI
11:10
20m
Talk
Link-Time Optimization of Dynamic Casts in C++ Programs
PLDI Research Papers
Xufan Lu INESC-ID / Instituto Superior Técnico, University of Lisbon, Nuno P. Lopes INESC-ID; Instituto Superior Técnico - University of Lisbon
Link to publication DOI
11:30
20m
Talk
Divergence-Aware Testing of Graphics Shader Compiler Back-Ends
PLDI Research Papers
Dongwei Xiao Hong Kong University of Science and Technology, Shuai Wang Hong Kong University of Science and Technology, Zhibo Liu Hong Kong University of Science and Technology, Yiteng Peng Hong Kong University of Science and Technology, Daoyuan Wu Hong Kong University of Science and Technology, Zhendong Su ETH Zurich
DOI
11:50
20m
Talk
Optimization-Directed Compiler Fuzzing for Continuous Translation Validation
PLDI Research Papers
Jaeseong Kwon KAIST, Bongjun Jang KAIST, Juneyoung Lee AWS, Kihong Heo KAIST
DOI
14:00 - 15:20
DatabasesPLDI Research Papers at Grand Ball Room 1
14:00
20m
Talk
Polygon: Symbolic Reasoning for SQL using Conflict-Driven Under-Approximation Search
PLDI Research Papers
Pinhan Zhao University of Michigan, Yuepeng Wang Simon Fraser University, Xinyu Wang University of Michigan
DOI Pre-print
14:20
20m
Talk
Pointer Analysis for Database-Backed Applications
PLDI Research Papers
Yufei Liang Nanjing University, Teng Zhang Nanjing University, Ganlin Li Nanjing University, Tian Tan Nanjing University, Chang Xu Nanjing University, Chun Cao Nanjing University, Xiaoxing Ma Nanjing University, Yue Li Nanjing University
DOI
14:40
20m
Talk
Graphiti: Bridging Graph and Relational Database Queries
PLDI Research Papers
Yang He Simon Fraser University, Ruijie Fang University of Texas at Austin, Işıl Dillig University of Texas at Austin, Yuepeng Wang Simon Fraser University
DOI
15:00
20m
Talk
AWDIT: An Optimal Weak Database Isolation Tester
PLDI Research Papers
Lasse Møldrup Aarhus University, Andreas Pavlogiannis Aarhus University
DOI

Wed 18 Jun

Displayed time zone: Seoul change

Room10:003011:003012:003013:003014:003015:003016:003017:0030
Grand Ball Room 1

PLDI Research Papers

Compilers 1

PLDI Research Papers

Security & Cryptography

PLDI Research Papers

Big Red KATS

Thu 19 Jun

Displayed time zone: Seoul change

Room10:003011:003012:003013:003014:0030
Grand Ball Room 1

PLDI Research Papers

Verification 1

PLDI Research Papers

Automata Theory

Fri 20 Jun

Displayed time zone: Seoul change

Room10:003011:003012:003013:003014:003015:0030
Grand Ball Room 1

PLDI Research Papers

Compilers 2

PLDI Research Papers

Databases

Wed 18 Jun

Displayed time zone: Seoul change

Room10:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:00153045
Grand Ball Room 1
PLDI Research Papers
Partial Evaluation, Whole-Program Compilation
10:30 - 10:50
PLDI Research Papers
Exploiting Undefined Behavior in C/C++ Programs for Optimization: A Stu ...
10:50 - 11:10
PLDI Research Papers
Relaxing Alias Analysis: Exploring the Unexplored Space
11:10 - 11:30
PLDI Research Papers
Webs and Flow-Directed Well-Typedness Preserving Program Transformations
11:30 - 11:50
PLDI Research Papers
Slotted E-Graphs: First-Class Support for (Bound) Variables in E-Graphs
11:50 - 12:10
PLDI Research Papers
Verified Foundations for Differential Privacy
14:00 - 14:20
PLDI Research Papers
Automated Exploit Generation for Node.js Packages
14:20 - 14:40
PLDI Research Papers
Robust Constant-Time Cryptography
14:40 - 15:00
PLDI Research Papers
Smooth, Integrated Proofs of Cryptographic Constant Time for Nondetermi ...
15:00 - 15:20
PLDI Research Papers
Morello-Cerise: A Proof of Strong Encapsulation for the Arm Morello Cap ...
15:20 - 15:40
PLDI Research Papers
Active Learning of Symbolic NetKAT Automata
16:00 - 16:20
PLDI Research Papers
StacKAT: Infinite State Network Verification
16:20 - 16:40
PLDI Research Papers
Probabilistic Kleene Algebra with Angelic Nondeterminism
16:40 - 17:00
PLDI Research Papers
Membership Testing for Semantic Regular Expressions
17:00 - 17:20

Thu 19 Jun

Displayed time zone: Seoul change

Room10:0015304511:0015304512:0015304513:0015304514:00153045
Grand Ball Room 1
PLDI Research Papers
A Hybrid Approach to Semi-automated Rust Verification
10:30 - 10:50
PLDI Research Papers
RefinedProsa: Connecting Response-Time Analysis with C Verification for ...
10:50 - 11:10
PLDI Research Papers
Certified Compilers à la Carte
11:10 - 11:30
PLDI Research Papers
Destabilizing Iris
11:30 - 11:50
PLDI Research Papers
Verifying Lock-Free Traversals in Relaxed Memory Separation Logic
11:50 - 12:10
PLDI Research Papers
A Uniform Framework for Handling Position Constraints in String Solving
14:00 - 14:20
PLDI Research Papers
Intrinsic Verification of Parsers and Formal Grammar Theory in Dependen ...
14:20 - 14:40
PLDI Research Papers
Verifying Solutions to Semantics-Guided Synthesis Problems
14:40 - 15:00

Fri 20 Jun

Displayed time zone: Seoul change

Room10:0015304511:0015304512:0015304513:0015304514:0015304515:00153045
Grand Ball Room 1
PLDI Research Papers
Robustifying Debug Information Updates in LLVM via Control-Flow Conform ...
10:30 - 10:50
PLDI Research Papers
CompCertOC: Verified Compositional Compilation of Multi-threaded Progra ...
10:50 - 11:10
PLDI Research Papers
Link-Time Optimization of Dynamic Casts in C++ Programs
11:10 - 11:30
PLDI Research Papers
Divergence-Aware Testing of Graphics Shader Compiler Back-Ends
11:30 - 11:50
PLDI Research Papers
Optimization-Directed Compiler Fuzzing for Continuous Translation Valid ...
11:50 - 12:10
PLDI Research Papers
Polygon: Symbolic Reasoning for SQL using Conflict-Driven Under-Approxi ...
14:00 - 14:20
PLDI Research Papers
Pointer Analysis for Database-Backed Applications
14:20 - 14:40
PLDI Research Papers
Graphiti: Bridging Graph and Relational Database Queries
14:40 - 15:00
PLDI Research Papers
AWDIT: An Optimal Weak Database Isolation Tester
15:00 - 15:20