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

Room information: Grand Ball Room 2

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

Grand Ball Room 2

Program

You're viewing the program in a time zone which is different from your device's time zone change time zone

Mon 16 Jun

Displayed time zone: Seoul change

14:00 - 15:20
Session 1PLMW @ PLDI / Catering at Grand Ball Room 2
14:00
10m
Social Event
Day Opening
PLMW @ PLDI

14:10
70m
Social Event
PL Cards
PLMW @ PLDI

15:40 - 17:00
Session 2PLMW @ PLDI at Grand Ball Room 2
15:40
60m
Social Event
Skill exchange
PLMW @ PLDI

16:40
20m
Social Event
Conclusion
PLMW @ PLDI

Tue 17 Jun

Displayed time zone: Seoul change

09:00 - 10:10
Session 1PLMW @ PLDI at Grand Ball Room 2
Chair(s): Umang Mathur National University of Singapore
09:00
10m
Day opening
Opening remarks
PLMW @ PLDI

09:10
60m
Talk
Research on Different Time Horizons (and an Example with Machine-Checked Proofs)
PLMW @ PLDI
Adam Chlipala Massachusetts Institute of Technology
10:30 - 12:00
Session 2PLMW @ PLDI at Grand Ball Room 2
Chair(s): Đorđe Žikelić Singapore Management University, Singapore
10:30
35m
Talk
Graduate School Revisited: An Assistant Professor's Perspective
PLMW @ PLDI
Qirun Zhang Georgia Institute of Technology
11:05
55m
Talk
From Formal Verification to Correctly Rounded Math Libraries
PLMW @ PLDI
Santosh Nagarakatte Rutgers University
14:00 - 15:20
Session 3PLMW @ PLDI at Grand Ball Room 2
Chair(s): Đorđe Žikelić Singapore Management University, Singapore
14:00
35m
Talk
Regularizing the Irregular
PLMW @ PLDI
Milind Kulkarni Purdue University
14:35
35m
Talk
Language Design Where Paradigms Meet
PLMW @ PLDI
Yizhou Zhang University of Waterloo
15:10
10m
Talk
Standardaizing JavaScript: Call for PL researchers
PLMW @ PLDI
Mikhail Barash University of Bergen, Yulia Startsev Mozilla
15:40 - 17:45
Session 4PLMW @ PLDI at Grand Ball Room 2
Chair(s): Jingbo Wang Purdue University
15:40
35m
Talk
Usable PL: Human-Computer Interaction for PL Research
PLMW @ PLDI
Sarah E. Chasins University of California at Berkeley
16:15
30m
Talk
Nomads and Anvil makers
PLMW @ PLDI
Rachit Nigam Massachusetts Institute of Technology
16:45
50m
Panel
PL and beyond
PLMW @ PLDI
P: Işıl Dillig University of Texas at Austin, P: Andrew Myers Cornell University, P: Ilya Sergey National University of Singapore, P: Rachit Nigam Massachusetts Institute of Technology, P: Pavel Panchekha University of Utah, P: David Tarditi Apple Inc.
17:35
10m
Day closing
Concluding remarks
PLMW @ PLDI

Wed 18 Jun

Displayed time zone: Seoul change

10:30 - 12:10
Compilers 1PLDI Research Papers at Grand Ball Room 2
Chair(s): Bor-Yuh Evan Chang University of Colorado Boulder & Amazon
10:30
20m
Talk
Partial Evaluation, Whole-Program Compilation
PLDI Research Papers
Chris Fallin F5, Maxwell Bernstein Recurse Center
DOI Pre-print
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 Pre-print File Attached
14:00 - 15:40
Security & CryptographyPLDI Research Papers at Grand Ball Room 2
Chair(s): Thomas Bourgeat EPFL
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
Circuit Optimization using Arithmetic Table Lookups
PLDI Research Papers
Raghav Malik Purdue University, Vedant Paranjape Purdue University, Milind Kulkarni Purdue University
DOI
16:00 - 17:20
Big Red KATsPLDI Research Papers at Grand Ball Room 2
Chair(s): Alex Potanin Australian National University
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 2
Chair(s): Samuel Gruetter ETH Zurich
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 Institute of Science and Technology Austria, 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 IrisDistinguished Paper
PLDI Research Papers
Simon Spies Jane Street, Niklas Mück MPI-SWS, Haoyi Zeng Saarland University, Michael Sammler Institute of Science and Technology Austria, 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 2
Chair(s): Umang Mathur National University of Singapore
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 Pre-print
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 2
Chair(s): Michel Steuwer Technische Universität Berlin
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 Pre-print
14:00 - 15:20
DatabasesPLDI Research Papers at Grand Ball Room 2
Chair(s): Adam Chlipala Massachusetts Institute of Technology
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 TesterDistinguished Paper
PLDI Research Papers
Lasse Møldrup Aarhus University, Andreas Pavlogiannis Aarhus University
DOI

Mon 16 Jun

Displayed time zone: Seoul change

Room14:003015:003016:0030
Grand Ball Room 2

PLMW @ PLDI + Catering

Session 1

PLMW @ PLDI

Session 2

Tue 17 Jun

Displayed time zone: Seoul change

Room9:003010:003011:003012:003013:003014:003015:003016:003017:0030
Grand Ball Room 2

PLMW @ PLDI

Session 1

PLMW @ PLDI

Session 2

PLMW @ PLDI

Session 3

PLMW @ PLDI

Session 4

Wed 18 Jun

Displayed time zone: Seoul change

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

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 2

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 2

PLDI Research Papers

Compilers 2

PLDI Research Papers

Databases

Mon 16 Jun

Displayed time zone: Seoul change

Room14:0015304515:0015304516:00153045
Grand Ball Room 2
PLMW @ PLDI
Day Opening
14:00 - 14:10
PLMW @ PLDI
PL Cards
14:10 - 15:20
PLMW @ PLDI
Skill exchange
15:40 - 16:40
PLMW @ PLDI
Conclusion
16:40 - 17:00

Tue 17 Jun

Displayed time zone: Seoul change

Room9:0015304510:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:00153045
Grand Ball Room 2
PLMW @ PLDI
Opening remarks
09:00 - 09:10
PLMW @ PLDI
Research on Different Time Horizons (and an Example with Machine-Checke ...
09:10 - 10:10
PLMW @ PLDI
Graduate School Revisited: An Assistant Professor's Perspective
10:30 - 11:05
PLMW @ PLDI
From Formal Verification to Correctly Rounded Math Libraries
11:05 - 12:00
PLMW @ PLDI
Regularizing the Irregular
14:00 - 14:35
PLMW @ PLDI
Language Design Where Paradigms Meet
14:35 - 15:10
PLMW @ PLDI
Standardaizing JavaScript: Call for PL researchers
15:10 - 15:20
PLMW @ PLDI
Usable PL: Human-Computer Interaction for PL Research
15:40 - 16:15
PLMW @ PLDI
Nomads and Anvil makers
16:15 - 16:45
PLMW @ PLDI
PL and beyond
16:45 - 17:35
PLMW @ PLDI
Concluding remarks
17:35 - 17:45

Wed 18 Jun

Displayed time zone: Seoul change

Room10:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:00153045
Grand Ball Room 2
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
Circuit Optimization using Arithmetic Table Lookups
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 2
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 PapersDistinguished Paper
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 2
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 PapersDistinguished Paper
AWDIT: An Optimal Weak Database Isolation Tester
15:00 - 15:20