Filter Program
Dates
Rooms
Tracks
Badges
Your Program
This program is tentative and subject to change.
Mon 15 JunDisplayed time zone: Mountain Time (US & Canada) change
Mon 15 Jun
Displayed time zone: Mountain Time (US & Canada) change
09:00 - 12:00 | |||
09:00 3hTutorial | Writing Performance-Portable Kernels Simplified with Helion Tutorials | ||
09:00 - 10:10 | |||
09:00 40mTalk | Introduction PROPL Cyrus Omar University of Michigan, Anil Madhavapeddy University of Cambridge, UK, Dominic Orchard University of Cambridge; University of Kent, KC Sivaramakrishnan IIT Madras and Tarides | ||
09:40 30mTalk | Marrying engineering rigor & scientific rigor for the planet PROPL Deepak Cherian Earthmover PBC | ||
09:00 - 12:00 | |||
09:00 3hTutorial | Implementing an Integrated Development Environment: a Quick Start Guide for PL Researchers Tutorials | ||
09:00 - 10:10 | |||
09:00 23mTalk | From Rewriting to Fixpoints: Solving Recursive Equations with E-Graphs EGRAPHS Samuel Coward University College London (UCL), Cheng Zhang Worcester Polytechnic Institute, Philip Zucker Draper, Alexandra Silva Cornell University | ||
09:23 23mTalk | Lifting E-Graphs: A Function Isn’t a Constant EGRAPHS Philip Zucker Draper Link to publication | ||
09:46 23mTalk | Predicate E-Graphs with Symbolic Conditional Rewriting EGRAPHS Anders Ågren Thuné Uppsala University, Johannes Borgström Uppsala University, Sweden, Lars-Henrik Eriksson Uppsala University, John Högberg Ericsson, Tjark Weber Uppsala University, Tobias Wrigstad Uppsala University | ||
09:00 - 10:10 | |||
09:00 10mDay closing | Opening remarks PAgE Shraddha Barke Microsoft Research, Redmond | ||
09:10 60mKeynote | Formal Methods for Frontier AI Systems PAgE Gagandeep Singh University of Illinois Urbana-Champaign | ||
09:00 - 12:00 | |||
09:00 3hTutorial | Mechanized Specifications for Real-World Programming Languages Tutorials | ||
10:10 - 10:40 | |||
10:10 30mCoffee break | Break Catering | ||
10:40 - 12:20 | |||
10:40 30mTalk | A Compiler-First Planetary Compute Engine: Automatic differentiable and performance portable Earth System Modeling PROPL William S. Moses University of Illinois Urbana-Champaign, Gong Cheng Dartmouth College, Valentin Churavy Johannes Gutenberg University, Mainz & University of Augsburg, Maximilian Gelbrecht Technical University of Munich & Potsdam Institute for Climate Impact Research, Milan Klower University of Oxford, Joseph Kump UT Austin, Mathieu Morlighem Dartmouth College, Sarah Williamson UT Austin, Dhruv Apte UT Austin, Paul Berg Aeolus Labs, Mosè Giordano UCL, Chris Hill MIT, Nora Loose [C]Worthy, Alexis Montoison Argonne National Laboratory, Sri Hari Krishna Narayanan Argonne National Laboratory, Avik Pal MIT, Michel Schanen Argonne National Laboratory, Simone Silvestri Politecnico di Torino, Greg Wagner MIT; Aeolus Labs, Patrick Heimbach UT Austin | ||
11:10 30mTalk | Mind the Gap: General-Purpose Programming Languages Impede Scientific Model Development and Communication PROPL Dominic Orchard University of Cambridge; University of Kent | ||
11:40 30mTalk | The Basic Model Interface (BMI) PROPL Mark D Piper University of Colorado Boulder, Eric WH Hutton University of Colorado Boulder, Gregory E Tucker University of Colorado Boulder | ||
10:40 - 12:20 | |||
10:40 25mTalk | A Semi-Persistent E-Graph with Native AC Canonization and Leapfrog AC Matching. EGRAPHS Remi Delmas Amazon Web Services | ||
11:05 25mTalk | Associativity and Commutativity in Equality Saturation EGRAPHS Tarik Rosin Saarland University, Marcel Ullrich Saarland University, Saarland Informatics Campus, Sebastian Hack Saarland University, Saarland Informatics Campus Pre-print | ||
11:30 25mTalk | Augmenting Rewrite Rule Sets via Knuth-Bendix Completion EGRAPHS Michael Schifferer Saarland University, Marcel Ullrich Saarland University, Saarland Informatics Campus, Sebastian Hack Saarland University, Saarland Informatics Campus Pre-print | ||
11:55 25mTalk | E-graphs modulo theories EGRAPHS Sofia Brookie Chalmers University of Technology | ||
10:40 - 12:20 | |||
10:40 20mTalk | Agentic Code Reasoning PAgE Pre-print | ||
11:00 20mTalk | Towards Verified Code Reasoning by LLMs PAgE Meghana Aparna Sistla Google DeepMind, Gogul Balakrishnan Google, Patrick Rondon Google, José Pablo Cambronero Google, USA, Michele Tufano Google, Satish Chandra Meta Platforms, Inc. | ||
11:20 20mTalk | Testing LLM-Generated Distributed Protocol Code PAgE | ||
11:40 20mTalk | The Next Frontier for AI-Generated Kernels: Correctness PAgE DOI Pre-print | ||
12:00 20mTalk | Testing, Credible Compilation, and Verification in the Axon Verified Compiler in Lean and Claude Code PAgE Martin C. Rinard Massachusetts Institute of Technology | ||
12:20 - 13:40 | |||
12:20 80mLunch | Lunch Catering | ||
13:40 - 15:20 | |||
13:40 20mMeeting | Guided discussion planning PROPL | ||
14:00 30mMeeting | User experience discussion PROPL | ||
14:30 30mTalk | Programming model discussion PROPL | ||
15:00 20mMeeting | Interoperability discussion PROPL | ||
13:40 - 15:20 | |||
13:40 25mTalk | Rewrite System Showdown: Stochastic Search vs. EqSat EGRAPHS Qiantan Hong Stanford University, Rupanshu Soi Stanford University, Yihong Zhang University of Washington, Alex Aiken Stanford University Pre-print | ||
14:05 25mTalk | A Joint Approach to Instruction Scheduling and Algebraic Rewriting with E-Graphs EGRAPHS | ||
14:30 25mTalk | Answer Set Programming for Egg Extraction and More EGRAPHS | ||
14:55 25mTalk | CERES: Making Equality Saturation Memory-Scalable EGRAPHS Akash Pardeshi University of Illinois at Urbana-Champaign, Devansh Jain University of Illinois at Urbana-Champaign, Saatvik Lochan University of Illinois Urbana-Champaign, Mihir Tandon University of Illinois Urbana-Champaign, Marco Frigo University of Illinois at Urbana-Champaign, Chamika Sudusinghe University of Illinois at Urbana-Champaign, Damitha Lenadora University of Illinois at Urbana-Champaign, Charith Mendis University of Illinois at Urbana-Champaign | ||
14:00 - 15:20 | Session 1: Advanced Compiler TuningLCTES at Flatirons 3 Chair(s): Myeonggyun Han Kyungpook National University | ||
14:00 10mKeynote | Opening Remarks LCTES Jeronimo Castrillon TU Dresden, Germany | ||
14:10 22mTalk | RAPO: Retrieval-Augmented Phase Ordering LCTES Jinwook Yang Seoul National University, Junghyun Lee Seoul National University, South Korea, Yeonsun Hong Seoul National University, Hyojin Sung Seoul National University DOI | ||
14:32 22mTalk | CausalTuner: Feature-Aware Causal Guidance for Compiler Auto-tuning LCTES Jiaqing Zhong National University of Defense Technology, Juan Chen College of Computer Science and Technology, National University of Defense Technology, China, Yichang Zhou National University of Defense Technology, Kuan Li Dongguan University of Technology DOI | ||
14:54 22mTalk | Empirical Observations about Profile-Guided Optimizations for Mainstream C/C++ Compilers LCTES DOI | ||
14:00 - 17:00 | |||
14:00 3hTutorial | Deep dive into the AWS Nitro Isolation Engine Tutorials Ike Mulder Radboud University Nijmegen, Nathan Chong Amazon Web Services, Hanno Becker Amazon Web Services, Dominic P. Mulligan Amazon Web Services, Robert Dockins Amazon | ||
14:00 - 15:20 | |||
14:00 80mTutorial | A guided tour through Oxidized OCaml Tutorials Anil Madhavapeddy University of Cambridge, UK, Gavin Gray Brown University, Shriram Krishnamurthi Brown University, Will Crichton Brown University, Chris Casinghino Jane Street, Richard A. Eisenberg Jane Street, KC Sivaramakrishnan IIT Madras and Tarides | ||
15:20 - 15:50 | |||
15:20 30mCoffee break | Break Catering | ||
15:50 - 17:10 | Session 2: Binary Optimization & System SecurityLCTES at Flatirons 3 Chair(s): Prasad Kulkarni University of Kansas | ||
15:50 22mTalk | DeduBB: Binary Code Size Reduction via Post-Link Basic Block Deduplication LCTES Chaitanya Mamatha Ananda University of California Riverside, Mahbod Afarin University of California, Riverside, Rajiv Gupta University of California at Riverside, Sriraman Tallam Google Inc., Han Shen Google Inc, Xinliang Li Google DOI | ||
16:12 22mTalk | SymFlow: Event-Chain-Aware Symbolic Execution for Serverless Sensitive Data Flow Detection LCTES Yuanpeng Wang Peking University, Zhineng Zhong Key Laboratory of High-Confidence Software Technologies (MOE), School of Computer Science, Peking University, Zhenkai Liang National University of Singapore, Ding Li Peking University, Yao Guo Peking University, Xiangqun Chen Peking University DOI | ||
16:34 10mShort-paper | CVS: A Metric for Security-Aware Compilation against Side-Channel Attacks in Edge SoCs (WIP) LCTES Yi Han College of Computer Science and Technology, National University of Defense Technology, Changsha, China & Key Laboratory of Advanced Microprocessor Chips and Systems, Changsha, China, Puhong Lei Hunan Greatwall Galaxy Science and Technology Co.,Ltd Changsha, P.R. China, Yang Shi National University of Defense Technology, Zhe Li College of Computer Science and Technology, National University of Defense Technology, Changsha, China & Key Laboratory of Advanced Microprocessor Chips and Systems, Changsha, China, Xing Mou College of Computer Science and Technology, National University of Defense Technology, Changsha, China & Key Laboratory of Advanced Microprocessor Chips and Systems, Changsha, China, Jianjun Chen College of Computer Science and Technology, National University of Defense Technology, Changsha, China & Key Laboratory of Advanced Microprocessor Chips and Systems, Changsha, China, Yaohua Wang College of Computer Science and Technology, National University of Defense Technology, Changsha, China & Key Laboratory of Advanced Microprocessor Chips and Systems, Changsha, China DOI | ||
16:44 10mShort-paper | A Programming Model for Efficient Inter-Kernel Control-Flow on Memory-Mapped Near-Data Processing Architecture (WIP) LCTES Seungheon Lee POSTECH, Wonhyuk Yang POSTECH, Seonyeong Heo Kyung Hee University, Gwangsun Kim POSTECH / Arm DOI | ||
16:54 10mShort-paper | FLUX: Frequency Scaling with Layer-wise Utilization for Energy-Efficient NPU Execution (WIP) LCTES Inho Lee Hanyang University, Ky Yeop Lim , Hyejun Kim Yonsei University, Beomseok Kim Seoul National University, Dongsuk Jeon Seoul National University, Hunjun Lee Hanyang University, Yongjun Park Yonsei University DOI | ||
15:50 - 17:20 | |||
15:50 20mMeeting | Scaling discussion PROPL | ||
16:10 30mMeeting | AI discussion PROPL | ||
16:40 30mMeeting | Sociotechnical factors, driving adoption PROPL | ||
17:10 10mMeeting | Next steps and action plan PROPL | ||
15:50 - 17:30 | |||
15:50 25mTalk | Relational E-matching in an SMT solver EGRAPHS Amar Shah Carnegie Mellon University, Marijn Heule Carnegie Mellon University, Bryan Parno Carnegie Mellon University, Max Willsey University of California at Berkeley | ||
16:15 25mTalk | E-Stitch: Top-Down Library Learning for E-Graphs EGRAPHS Kavi Gupta MIT, Maddy Bowers Massachusetts Institute of Technology, Armando Solar-Lezama Massachusetts Institute of Technology | ||
16:40 25mTalk | Optimizing Optimizations, Declaratively: Optimizing the Higher-Order Functions in Mathematical Optimization with egglog EGRAPHS Hiromi Ishii JIJ Pre-print | ||
17:05 25mTalk | Poseidon: Profile-Guided Numerical Rewriting at Full-Application Scale EGRAPHS Siyuan Brant Qian University of Illinois at Urbana-Champaign, Vimarsh Sathia University of Illinois Urbana Champaign, Ivan Ivanov Institute of Science Tokyo, Jan Hueckelheim Argonne National Laboratory, Paul Hovland Argonne National Laboratory, William S. Moses University of Illinois Urbana-Champaign | ||
15:50 - 17:00 | |||
15:50 60mKeynote | Can Coding Agents Write Verifiably Correct Software? PAgE Shan Lu Microsoft; University of Chicago | ||
16:50 10mDay closing | Closing Remarks PAgE Shraddha Barke Microsoft Research, Redmond | ||
15:50 - 17:10 | |||
15:50 80mTutorial | A guided tour through Oxidized OCaml Tutorials Anil Madhavapeddy University of Cambridge, UK, Gavin Gray Brown University, Shriram Krishnamurthi Brown University, Will Crichton Brown University, Chris Casinghino Jane Street, Richard A. Eisenberg Jane Street, KC Sivaramakrishnan IIT Madras and Tarides | ||
18:00 - 20:00 | |||
18:00 2hSocial Event | Hike in Chautauqua PLDI Meetups | ||
19:00 - 21:00 | |||
19:00 2hDinner | Informal Workshop Dinner (at SALT) PROPL | ||
Tue 16 JunDisplayed time zone: Mountain Time (US & Canada) change
Tue 16 Jun
Displayed time zone: Mountain Time (US & Canada) change
09:00 - 12:20 | |||
09:00 3h20mTutorial | ACT: End-to-End Compiler Infrastructure for Emerging AI Accelerators Tutorials Devansh Jain University of Illinois at Urbana-Champaign, Charith Mendis University of Illinois at Urbana-Champaign Media Attached | ||
09:00 - 10:10 | |||
09:00 10mOther | Welcome ISMM | ||
09:10 60mKeynote | How should we evaluate garbage collectors?Keynote ISMM Tobias Wrigstad Uppsala University | ||
09:00 - 10:10 | |||
09:00 70mKeynote | Practical Quantum Machine Learning: Overcoming the Bottlenecks of Scalability and Stability LCTES Aviral Shrivastava Arizona State University File Attached | ||
09:00 - 10:10 | |||
09:00 10mDay opening | Welcome and Opening Remarks SOAP | ||
09:10 60mKeynote | How Context-Sensitive Static Analysis Led to the Best Smart Contract Decompiler SOAP Yannis Smaragdakis University of Athens | ||
09:00 - 09:10 | |||
09:00 10mDay opening | Opening Remarks PLMW @ PLDI | ||
09:00 - 10:05 | |||
09:00 15mTalk | Welcome and logistics Tom Ball @ Sixty Satish Chandra Meta Platforms, Inc., Shuvendu K. Lahiri Microsoft Research, Mayur Naik University of Pennsylvania, Byron Cook Amazon, Madan Musuvathi Microsoft Research | ||
09:15 25mTalk | Recollections from SLAM-ming with Tom Tom Ball @ Sixty Sriram Rajamani Microsoft Research Indua | ||
09:40 25mTalk | Testing, Verification, and Measurement --- Tom's still open challenge Tom Ball @ Sixty Madan Musuvathi Microsoft Research | ||
09:00 - 10:10 | |||
09:00 10mDay opening | Welcoming Remarks ARRAY | ||
09:10 50mKeynote | Tiles, Bricks, and Layouts: How Aggregate Data Abstractions Aid in Optimizing Data Movement ARRAY Mary Hall University of Utah | ||
10:00 10mLive Q&A | Q&A for Keynote-1 ARRAY | ||
09:00 - 10:10 | |||
09:00 10mTalk | Opening remarks CP | ||
09:10 60mKeynote | Interpreters everywhere! CP | ||
09:10 - 10:10 | |||
09:10 60mTalk | Roses are Blue, Violets are Red; With Future AI, is Research Dead? PLMW @ PLDI Thomas Reps University of Wisconsin-Madison | ||
10:10 - 10:40 | |||
10:10 30mCoffee break | Break Catering | ||
10:40 - 12:20 | |||
10:40 25mTalk | Going Where No GC Has Gone Before! ISMM | ||
11:05 25mTalk | Reconsidering "Reconsidering Custom Memory Allocation" ISMM Nicolas van Kempen University of Massachusetts Amherst, USA, Emery D. Berger University of Massachusetts Amherst and Amazon Web Services | ||
11:30 25mTalk | Interpreter Memory Safety via Differential Fuzzing with a CHERI on Top ISMM Kai Feng University of Glasgow, Huanting Wang University of Leeds, Jeremy Singer University of Glasgow, Zheng Wang University of Leeds DOI Pre-print | ||
11:55 25mTalk | Much Ado About Offset Vectors ISMM Hayley Patton Australian National University, Stephen M. Blackburn Google; Australian National University | ||
10:40 - 12:00 | |||
10:40 20mTalk | Exploring Locally Bounded Translation Validation SOAP Alborz Jelvani Rutgers University, Richard P. Martin Rutgers University, Santosh Nagarakatte Rutgers University | ||
11:00 20mTalk | Ravencheck: Effectively-Propositional Reasoning for Rust SOAP Kunha Kim University of Colorado Boulder, Nicholas V. Lewchenko University of Colorado Boulder, Bor-Yuh Evan Chang University of Colorado Boulder & Amazon, Gowtham Kaki University of Colorado at Boulder | ||
11:20 20mTalk | Compile-Time Java Stream Fusion via mapMulti SOAP | ||
11:40 20mTalk | Conditional Execution of Transpiler Passes Based on Per-Script Feature Detection SOAP Rishipal Singh Bhatia Google | ||
10:40 - 12:10 | |||
10:40 30mTalk | TBD PLMW @ PLDI Umang Mathur National University of Singapore | ||
11:10 45mTalk | You and Your PhD PLMW @ PLDI Peter Müller ETH Zurich | ||
11:55 15mTalk | SIGPLAN CARES PLMW @ PLDI Sukyoung Ryu KAIST | ||
10:40 - 12:20 | |||
10:40 25mTalk | From Bebop to Constrained Horn Clauses Tom Ball @ Sixty Nikolaj Bjørner Microsoft Research | ||
11:05 25mTalk | Research in Three-Part Harmony Tom Ball @ Sixty Todd Millstein University of California, Los Angeles | ||
11:30 25mTalk | Riffing on some themes from Tom: Driver Verification, Testing, Abstraction & Theorem Proving Tom Ball @ Sixty Nikhil Swamy Microsoft Research | ||
11:55 25mTalk | The SLAM "GiveUp" Tom Ball @ Sixty Rahul Kumar Amazon | ||
10:40 - 12:20 | |||
10:40 25mTalk | Refined Remora: Constraining Array Shapes ARRAY | ||
11:05 20mTalk | Relational Cell Morphing: Automated Verification of Relational Properties of Array Programs ARRAY Weihao Qu Monmouth University, Marco Gaboardi Boston University, Hiroshi Unno Tohoku University, Eric Koskinen Stevens Institute of Technology | ||
11:25 20mTalk | Graded Monoids for Dependently Typed Array Programming ARRAY Juuso Haavisto University of Oxford, Jeremy Gibbons Department of Computer Science, University of Oxford | ||
11:45 25mTalk | Portable Anomaly Detection for Distributed PGAS Programs based on Array Mapping Abstractions ARRAY Raneem Abu-Yosef Ohio State University, Thomas Huddleston The Ohio State University, Kirshanthan Sundararajah Virginia Tech, Martin Kong Ohio State University | ||
12:10 10mOther | Mini Panel AM ARRAY | ||
10:40 - 12:20 | |||
10:40 25mTalk | The Chor of the Message Passing Interface (MPI) CP | ||
11:05 25mTalk | Towards Quantum Choreographies CP Jennifer Paykin University of Vermont, Joseph P. Near University of Vermont, Christian Skalka University of Vermont | ||
11:30 25mTalk | Pact: A Choreographic Language for Agentic Ecosystems CP File Attached | ||
11:55 25mTalk | Towards Choreographic Programming for Consensus Protocols CP | ||
12:20 - 13:40 | |||
12:20 80mLunch | Lunch Catering | ||
13:40 - 14:40 | |||
13:40 60mKeynote | Reduce, Reuse, Recycle: Is this Mantra under attack with Proliferation of Machine Learning?Keynote ISMM Lizy John University of Texas, Austin | ||
13:40 - 15:20 | Session 4: Specialized Hardware and Accelerator DesignLCTES at Flatirons 3 Chair(s): Jongouk Choi University of Central Florida | ||
13:40 22mTalk | Can Fine-Grain Multi-threading Subsume VLIW? LCTES Scott Pomerville Northern Michigan University, Soner Onder Michigan Technological University, Gang-Ryung Uh Florida State University, David Whalley Florida State University DOI | ||
14:02 22mTalk | Sirop: A Small IR for HLS with Parallel Patterns LCTES DOI | ||
14:24 22mTalk | A Functional Approach to Synthesizing Routable Programmable Accelerators for Neural Networks LCTES Tzung-Han Juang McGill University, Paul Teng McGill University, Canada, Christophe Dubach McGill University DOI | ||
14:46 22mTalk | LoopHint: A Compiler-Assisted Loop Branch Predictor for Embedded DSPs LCTES Yuanyang Xiang Institute of Automation, Chinese Academy of Sciences, Chen Xu , xiaoruozhou Institute of Automation, Chinese Academy of Sciences, Zhiwei Zhang Institute of Automation, Chinese Academy of Sciences DOI | ||
13:40 - 15:10 | |||
13:40 30mTalk | How to Read a PL Paper (while Also Doing Other Things Too) PLMW @ PLDI Justin Hsu Cornell University | ||
14:10 30mTalk | How to Give a Research Talk PLMW @ PLDI Charles Yuan University of Wisconsin-Madison | ||
14:40 30mTalk | Correct Compilation for Asynchronous Dataflow Architectures PLMW @ PLDI Milijana Surbatovich University of Maryland at College Park | ||
13:40 - 15:20 | |||
13:40 25mTalk | Ju-jitsu with Ball-Larus (& Melski-Reps) or "We will publish no algorithm before its time" Tom Ball @ Sixty Thomas Reps University of Wisconsin-Madison | ||
14:05 25mTalk | Interdisciplinary Genius in the 21st Century: The Case of Tom Ball Tom Ball @ Sixty Mooly Sagiv Certora, inc. | ||
14:30 25mTalk | Having a Ball with Tom since 1994 Tom Ball @ Sixty Patrice Godefroid Microsoft, USA | ||
14:55 25mTalk | The Question That Launched a Thousand Derivatives Tom Ball @ Sixty Margus Veanes Microsoft Research | ||
13:40 - 15:20 | |||
13:40 50mKeynote | The Shape of Things to Come ARRAY Jared Roesch NVIDIA | ||
14:30 10mLive Q&A | Q&A for Keynote-2 ARRAY | ||
14:40 20mTalk | Tensor Algebra Equivalence Checker ARRAY | ||
15:00 20mTalk | Rhyme: A Multi-Paradigm Declarative Query Language ARRAY | ||
13:40 - 15:20 | |||
13:40 25mTalk | Probabilistic Performance of Asynchronous Data-Flow Choreographies CP Mako P. Bates University of Vermont | ||
14:05 25mTalk | Bushwhacking towards Event-Driven Chorex CP | ||
14:30 25mTalk | Formalizing the Equivalence between Select-&-Merge and Conclaves-&-MLVs CP Mako P. Bates University of Vermont, Xueying Qin University of Southern Denmark, Joseph P. Near University of Vermont, Marco Peressotti University of Southern Denmark | ||
14:55 25mTalk | Parametric Choreographies for Distributed Programming CP | ||
14:00 - 15:20 | |||
14:00 60mKeynote | Compositional Data-Flow Analysis at Industrial Scale SOAP Michael Emmi Amazon Web Services | ||
15:00 20mTalk | Scaling Static Code Analysis Adoption at WhatsApp iOS SOAP Ákos Hajdu Meta, Jorge Mendez Meta, Sander van Valkenburg Meta, Artem Kupriianets Meta, Matteo Marescotti Meta, Dulma Churchill Meta, Sopot Cela Meta | ||
14:40 - 15:30 | |||
14:40 25mTalk | Stride-Aware Page Prefetching for GPU Unified Memory via Markov Pattern Prediction ISMM | ||
15:05 25mTalk | Consistency and Coherence of the NVIDIA Grace-Hopper Superchip ISMM Soham Bagchi The University of Utah, Sanya Srivastava Duke University, Reese Levine University of California at Santa Cruz, Tyler Sorensen Microsoft Research; University of California at Santa Cruz, Ryan Stutsman University of Utah, Vijay Nagarajan University of Utah | ||
15:20 - 15:50 | |||
15:20 30mCoffee break | Break Catering | ||
15:50 - 17:05 | |||
15:50 25mTalk | Enabling Huge Pages for Real-World Executables ISMM Nadav Amit Technion | ||
16:15 25mTalk | Stretch: A Fault-Driven DSM Runtime for Distributed Multithreaded Applications ISMM Edoardo D'Alessio University of Illinois Chicago, Mohamed Husain Virginia Tech, Xiaoguang Wang University of Illinois Chicago, Binoy Ravindran Virginia Tech | ||
16:40 25mTalk | Bandwidth Speaks, We Listen: Dynamic Memory Interleaving for Tiering ISMM Bijan Tabatabai University of Wisconsin-Madison, Eishan Mirakhur Micron Technology, Ravi Shankar Jonnalagadda Micron Technology, Vinicius Petrucci Micron Technology, Rohit Sehgal Micron Technology, Jus Singh Micron Technology, Michael Swift University of Wisconsin--Madison | ||
15:50 - 17:00 | Session 5: Memory Efficiency and Control-Flow AnalysisLCTES at Flatirons 3 Chair(s): Sandrine Blazy University of Rennes | ||
15:50 22mTalk | MemSpec: Memory-Aware Runtime for Adaptive Draft Scheduling in Speculative Decoding on Edge Devices LCTES Eunjeong Kim Kyungpook National University, Yeong Jun Jeon Kyungpook National University, Myeonggyun Han Kyungpook National University DOI | ||
16:12 22mTalk | Bridging the Memory Hotness Gap in Edge Systems with Hotness-Segregated Object Allocation LCTES Ruizhe Huang Peking University, Jiahua Wang Peking University, Qihang Xu Peking University, Peng Jiang Southeast University, Zhida An Peking University, Ding Li Peking University, Yao Guo Peking University, Xiangqun Chen Peking University, Yuxin Ren Huawei Technologies, Ning Jia Huawei Technologies DOI | ||
16:34 22mTalk | On the Origins of Indirect Jumps in Embedded Software LCTES Ariane Nicolas Univ Rennes, Inria, CNRS, IRISA, Ronan Lashermes Rambus, Isabelle Puaut Université de Rennes - Inria - CNRS - IRISA, Erven Rohou Université de Rennes - Inria - CNRS - IRISA DOI | ||
16:56 4mTalk | Closing Session LCTES Jeronimo Castrillon TU Dresden, Germany | ||
15:50 - 18:00 | |||
15:50 60mKeynote | Compiler-assisted Translation Validation SOAP Qirun Zhang Georgia Institute of Technology | ||
16:50 20mTalk | On the Effectiveness of Modular Testing in EvoSuite SOAP Elizabeth Dinella Bryn Mawr College | ||
17:10 20mTalk | LLM-Integrated Declarative Program Analysis SOAP Sara Baradaran University of Southern California, Amirmohammad Nazari University of Southern California, Mukund Raghothaman University of Southern California | ||
17:30 20mTalk | Detecting Data Leaks in Multi-User LLM Apps via Automated User-Scoped Taint Analysis SOAP Sanjib Kumar Sen Texas A&M University - Corpus Christi, Bozhen Liu Texas A&M University - Corpus Christi | ||
17:50 10mDay closing | Closing Remarks SOAP | ||
15:50 - 16:20 | |||
15:50 30mTalk | Tales of Breaking and Fixing Software PLMW @ PLDI Sasa Misailovic University of Illinois Urbana-Champaign | ||
15:50 - 17:30 | |||
15:50 25mTalk | Tracing the Ball-istic Trajectory of My Research: From Randoop to FastF, Memory Models and Semantic Merging Tom Ball @ Sixty Shuvendu K. Lahiri Microsoft Research | ||
16:15 25mTalk | Tom and the evolution of abstraction Tom Ball @ Sixty Kenneth L. McMillan University of Texas at Austin | ||
16:40 5mTalk | Profiling, not Slicing, is the Path to Success (pre-recorded video) Tom Ball @ Sixty James Larus EPFL | ||
16:45 5mTalk | The BBC micro:bit revolution (pre-recorded video) Tom Ball @ Sixty Steve Hodges Lancaster University, UK | ||
16:50 30mTalk | Paths Converge: Software Model Checking for the BBC micro:bit Tom Ball @ Sixty Thomas Ball University of Washington (USA) and Lancaster University (UK) | ||
15:50 - 17:30 | |||
15:50 20mTalk | Vectorizing Sparse Coiteration for Two-finger Loop Structure (Extended Abstract) ARRAY | ||
16:10 25mTalk | Leveraging AI Ecosystem for Portable and Sustainable GPU Kernels in HPC ARRAY Yanbo Zhao North Carolina State University, Zhaonan Meng North Carolina State University, Sai Krishna Teja Varma Manthena NCSU, Xu Liu North Carolina State University, Ajay Panyala Pacific Northwest National Laboratory, Jiajia Li North Carolina State University | ||
16:35 20mTalk | Lazy Arithmetic using Systolic Arrays for Closing the Verification Gap on Embedded Systems ARRAY | ||
16:55 20mTalk | Towards a Linear-Algebraic Hypervisor ARRAY Pre-print | ||
17:15 5mResearch preview | Semantics as a Tool of Thought: Provenance-Aware Dimensional Checking in a Reactive Array IR ARRAY Christopher Buck None | ||
17:20 10mLive Q&A | Mini Panel ARRAY | ||
15:50 - 17:00 | |||
16:30 - 17:30 | |||
16:30 60mPanel | Research Taste: From Core PL to New Frontiers PLMW @ PLDI P: Peter Müller ETH Zurich, P: Adam Chlipala Massachusetts Institute of Technology, P: Fredrik Kjolstad Stanford University, P: Gagandeep Singh University of Illinois Urbana-Champaign | ||
17:30 - 21:30 | |||
18:00 - 19:30 | |||
18:00 90mSocial Event | Hike in Chautauqua PLDI Meetups | ||
19:30 - 21:30 | PLDI Organizing and Review Committees DinnerPLDI Events | ||
Wed 17 JunDisplayed time zone: Mountain Time (US & Canada) change
Wed 17 Jun
Displayed time zone: Mountain Time (US & Canada) change
07:30 - 08:30 | Student BreakfastPLDI Meetups at Alpine Modern Café Chair(s): Cade Lueker University of Colorado Boulder | ||
07:30 60mSocial Event | Student Breakfast PLDI Meetups | ||
09:00 - 10:10 | |||
09:00 70mKeynote | Programming Language Design and Implementation for the Machine Learning Era: A Personal Perspective PLDI Research Papers Saman Amarasinghe Massachusetts Institute of Technology | ||
10:10 - 11:00 | |||
10:10 50mCoffee break | Break Catering | ||
11:00 - 12:40 | |||
11:00 20mTalk | 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 Pre-print | ||
11:20 20mTalk | 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:40 20mTalk | 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 | ||
12:00 20mTalk | 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 | ||
12:20 20mTalk | 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 | ||
11:00 - 12:40 | |||
11:00 20mTalk | [SIGPLAN OOPSLA’25] Counterexample-Guided Inference of Modular Specifications PLDI Research Papers William Hallahan Binghamton, Ranjit Jhala University of California at San Diego, Ruzica Piskac Yale University | ||
11:20 20mTalk | Choose, Don’t Label: Multiple-Choice Query Synthesis for Program Disambiguation PLDI Research Papers Celeste Barnaby University of Texas at Austin, Danny Ding University of Texas at Austin, Osbert Bastani University of Pennsylvania, Işıl Dillig University of Texas at Austin DOI | ||
11:40 20mTalk | Presynthesis: Towards Scaling Up Program Synthesis with Finer-Grained Abstract Semantics PLDI Research Papers Rui Dong University of Michigan, Qingyue Wu University of Michigan, Danny Ding University of Texas at Austin, Zheng Guo University of Michigan, Ruyi Ji University of Michigan, Xinyu Wang University of Michigan DOI | ||
12:00 20mTalk | Verification Modulo Tested Library Contracts PLDI Research Papers Abhishek Uppar IISc Bangalore, Omar Muhammad IISc Bangalore, Sumanth Prabhu S Relyance AI, Deepak D'Souza IISc Bangalore, P. Madhusudan University of Illinois Urbana-Champaign, Adithya Murali University of Wisconsin-Madison DOI | ||
12:20 20mTalk | Expecto: Extracting Formal Specifications from Natural Language Description for Trustworthy Oracles PLDI Research Papers DOI | ||
11:00 - 12:40 | |||
11:00 20mTalk | Verification of Recursively Defined Quantum CircuitsDistinguished Paper PLDI Research Papers DOI | ||
11:20 20mTalk | SAQR-QC: A Logic for Scalable but Approximate Quantitative Reasoning about Quantum Circuits PLDI Research Papers Nengkun Yu Stony Brook University, Jens Palsberg University of California at Los Angeles, Thomas Reps University of Wisconsin-Madison DOI | ||
11:40 20mTalk | Hybrid Path-Sums for Hybrid Quantum Programs PLDI Research Papers Christopĥe Chareton CEA List - Université Paris-Saclay, Sébastien Bardin CEA List - Université Paris-Saclay, Jad Issa CEA List - Université Paris-Saclay, Mathieu Nguyen CEA List - Université Paris-Saclay, Nicolas Blanco CEA List - Université Paris-Saclay DOI | ||
12:00 20mTalk | [TOPLAS] VyZX: Formal Verification of a Graphical Quantum Language PLDI Research Papers Adrian Lehmann University of Chicago, Ben Caldwell University of Chicago, A: Bhakti Shah , William Spencer , Robert Rand University of Chicago | ||
12:20 20mTalk | Cobble: Compiling Block Encodings for Quantum Computational Linear AlgebraDistinguished Paper PLDI Research Papers Charles Yuan University of Wisconsin-Madison DOI | ||
12:40 - 14:00 | |||
12:40 - 14:00 | |||
12:40 80mLunch | Lunch Catering | ||
14:00 - 15:40 | |||
14:00 20mTalk | State Space Estimation for DPOR-Based Model Checkers PLDI Research Papers A. R. Balasubramanian MPI-SWS, Mohammad Hossein Khoshechin Jorshari MPI-SWS, Rupak Majumdar MPI-SWS, Umang Mathur National University of Singapore, Minjian Zhang University of Illinois Urbana-Champaign DOI Pre-print | ||
14:20 20mTalk | Fixed Parameter Tractable Linearizability Monitoring PLDI Research Papers DOI Pre-print | ||
14:40 20mTalk | SuperCollider: Scalable and Effective Data Race Detection for CUDA PLDI Research Papers Mark Stephenson NVIDIA, Sana Damani NVIDIA, Mohamed Tarek Ibn Ziad NVIDIA, Anis Ladram NVIDIA, Michael Garland NVIDIA DOI | ||
15:00 20mTalk | Fast Atomicity Monitoring PLDI Research Papers DOI | ||
14:00 - 15:40 | |||
14:00 20mTalk | Flow-Analysis-Based Closure Optimization PLDI Research Papers John Reppy University of Chicago, Olin Shivers Northeastern University, Byron Zhong University of Chicago DOI Pre-print | ||
14:20 20mTalk | SSA without Dominance for Higher-Order Programs PLDI Research Papers DOI Pre-print | ||
14:40 20mTalk | Analyzing Bytes: Pre-Disassembly Static Binary Analysis PLDI Research Papers Huan Nguyen Google, Soumyakant Priyadarshan Stony Brook University, Chencheng Jiang Stony Brook University, R. Sekar Stony Brook University DOI | ||
15:00 20mTalk | Exploiting Sophisticated Static Analysis for Verilog PLDI Research Papers Qinlin Chen Nanjing University, Nairen Zhang Nanjing University, Jinpeng Wang Nanjing University, Jiacai Cui Nanjing University, Tian Tan Nanjing University, Xiaoxing Ma Nanjing University, Chang Xu Nanjing University, Jian Lu Nanjing University, Yue Li Nanjing University DOI | ||
15:40 - 16:10 | |||
15:40 30mCoffee break | Break Catering | ||
16:10 - 17:50 | |||
16:10 20mTalk | 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 20mTalk | 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 20mTalk | Abstract Interpretation with Confidence PLDI Research Papers DOI | ||
17:10 20mTalk | 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 | ||
16:10 - 17:50 | |||
16:10 20mTalk | Kuiper: Correct and Efficient GPU Programming with Dependent Types and Separation Logic PLDI Research Papers Guido Martínez Microsoft Research, Bastian Köpcke TU Berlin, Jonáš Fiala ETH Zurich, Gabriel Ebner Microsoft Research, Tahina Ramananandro Microsoft Research, Michel Steuwer TU Berlin, Tyler Sorensen Microsoft Research, Nikhil Swamy Microsoft Research DOI Pre-print | ||
16:30 20mTalk | Modular GPU Programming with Typed PerspectivesDistinguished Paper PLDI Research Papers Manya Bansal Massachusetts Institute of Technology, Daniel Sainati University of Pennsylvania, Joseph W. Cutler University of Pennsylvania, Saman Amarasinghe Massachusetts Institute of Technology, Jonathan Ragan-Kelley Massachusetts Institute of Technology DOI | ||
16:50 20mTalk | [TOPLAS] StreamAlloc: A Framework for Analyzing and Transforming CUDA Code to Enable Asynchronous Execution PLDI Research Papers | ||
17:10 20mTalk | SIMT-Step Execution: A Flexible Operational Semantics For GPU Subgroup Behavior PLDI Research Papers Zheyuan Chen University of California at Santa Cruz, Naomi Rehman University of California at Santa Barbara, Guido Martínez Microsoft Research, Tyler Sorensen Microsoft Research; University of California at Santa Cruz DOI Pre-print | ||
17:30 20mTalk | Uniformity Analysis in the WebGPU Shading Language PLDI Research Papers James Lee-Jones Imperial College London, John Wickerson Imperial College London, Alastair F. Donaldson Imperial College London DOI | ||
16:10 - 17:50 | |||
16:10 20mTalk | [SIGPLAN PLDI’25] Probabilistic Refinement Session Types PLDI Research Papers | ||
16:30 20mTalk | [SIGPLAN OOPSLA’25] Complete the Cycle: Reachability Types with Expressive Cyclic References PLDI Research Papers Haotian Deng Purdue University, Siyuan He Purdue University, Songlin Jia Purdue University, Yuyan Bao Augusta University, Tiark Rompf Purdue University | ||
16:50 20mTalk | Backwards-Compatible Row-Based Exceptions in ML PLDI Research Papers Simcha van Collem Radboud University Nijmegen, Paulo Emílio de Vilhena Imperial College London, Robbert Krebbers Radboud University Nijmegen DOI | ||
17:10 20mTalk | Typestate via Revocable Capabilities PLDI Research Papers Songlin Jia Purdue University, Craig Liu Purdue University, Siyuan He Purdue University, Haotian Deng Purdue University, Yuyan Bao Augusta University, Tiark Rompf Purdue University DOI | ||
17:30 20mTalk | Syntactic Implicit Parameters with Static Overloading PLDI Research Papers DOI Pre-print | ||
17:50 - 19:30 | PLDI Reception with Student Research Competition PostersPLDI Events at The Lawn See here for the SRC posters details. | ||
17:50 - 19:30 | PLDI Reception with Student Research Competition PostersStudent Research Competition at The Lawn Reception for all attendees with light refreshments, with Student Research Competition posters. | ||
17:50 1h40mTalk | K-Sentry: A Verified Order-Sensitive Telemetry Accumulator Student Research Competition Sudrit Ghimire Texas State University | ||
17:50 1h40mTalk | Smocq: Formal Verification of Self Modifying Code Student Research Competition Ilan Buzzetti University of Texas at Dallas | ||
17:50 1h40mTalk | Formal Methods for Securing Federated Authorization: A Case Study of SciTokens Student Research Competition Minh Le Georgia Institute of Technology | ||
17:50 1h40mTalk | Scenario-based Proof for Distributed Protocols Student Research Competition Zhendong Ang National University of Singapore | ||
17:50 1h40mTalk | Language Models Need Some Space: On the Sensitivity of Constrained Decoding to Completeness Student Research Competition Jahrim Gabriele Cesario University of St. Gallen Link to publication | ||
17:50 1h40mTalk | Formal Proofs of Bit Hacks in Machine Code Student Research Competition Humam Alhusaini University of Texas at Arlington | ||
17:50 1h40mTalk | LLMEffect: A Type System for Securing LLM API Boundaries Student Research Competition Sanjib Kumar Sen Texas A&M University - Corpus Christi | ||
17:50 1h40mTalk | Pync: Function-Level Incremental Execution for Python Scripts Student Research Competition Bolun Thompson University of California, Los Angeles | ||
17:50 1h40mTalk | Correctly Rounded Dot Products under Round-to-Odd Student Research Competition Sehyeok Park Rutgers University | ||
17:50 1h40mTalk | Impulse: Momentously Fast, General, and Portable Probabilistic Programming via Compiler Augmentation Student Research Competition Siyuan Brant Qian University of Illinois at Urbana-Champaign | ||
17:50 1h40mTalk | Towards Taming Indirect Control Flow in Binaries with Multi-Task Graph Learning Student Research Competition Kun Liu Tulane University | ||
17:50 1h40mTalk | CAST: Continuous Fuzzing for SMT Solvers Student Research Competition Andrei Zhukov ETH Zürich | ||
17:50 1h40mTalk | Implementing Hybrid Resource Analysis in Resource Aware ML 2 Student Research Competition Arnav Sabharwal Carnegie Mellon University | ||
17:50 1h40mTalk | Modular Verification of Leakage Contracts Student Research Competition Aditya Ranjan Jha National University of Singapore | ||
17:50 1h40mTalk | Cumulating Abstract Semantics via Handlers Student Research Competition Cade Lueker University of Colorado Boulder | ||
17:50 1h40mTalk | Semantics Lifting for Scientific Kernels Student Research Competition Naifeng Zhang Carnegie Mellon University | ||
17:50 1h40mTalk | pp-horn: A Secure Inference Primitive Student Research Competition Sai Lalith Kumar Aka University of Colorado Boulder | ||
17:50 1h40mTalk | Automatic Energy Analysis Using Types Student Research Competition Sai Divvela University of Maryland, College Park, USA | ||
17:50 1h40mTalk | E-Graph-Based Metamorphic Testing for Datalog Engines Student Research Competition Samuel Gerbers ETH Zurich | ||
19:30 - 21:30 | |||
19:30 - 21:00 | Bands on the BricksPLDI Meetups at Flatirons Foyer Chair(s): Dakota Bryan University of Colorado, Boulder | ||
19:30 90mSocial Event | Bands on the Bricks PLDI Meetups | ||
Thu 18 JunDisplayed time zone: Mountain Time (US & Canada) change
Thu 18 Jun
Displayed time zone: Mountain Time (US & Canada) change
07:30 - 08:30 | Student Coffee and PastriesPLDI Meetups at Aviano Coffee Chair(s): Cade Lueker University of Colorado Boulder | ||
07:30 60mSocial Event | Student Coffee and Pastries PLDI Meetups | ||
07:30 - 08:30 | |||
07:30 60mSocial Event | Junior Faculty Breakfast PLDI Meetups | ||
09:00 - 10:10 | |||
09:00 70mKeynote | Happiness U-Curve: Navigating the AI Validation Bottleneck with Conformance Testing and Proof-Engineering PLDI Research Papers Miryung Kim UCLA and Amazon Web Services | ||
10:10 - 11:00 | |||
10:10 50mCoffee break | Break Catering | ||
11:00 - 12:20 | |||
11:00 20mTalk | 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 | ||
11:20 20mTalk | An Efficient Algorithm for Streaming BPE Tokenization PLDI Research Papers DOI | ||
11:40 20mTalk | 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 | ||
12:00 20mTalk | 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 | ||
11:00 - 12:40 | |||
11:00 20mTalk | Decoupling Data Layouts from Bounding Volume Hierarchies PLDI Research Papers Christophe Gyurgyik Stanford University, Alexander J Root Stanford University, Fredrik Kjolstad Stanford University DOI Pre-print | ||
11:20 20mTalk | Contextual Embeddings: Implementing Bound Variables through Instance Resolution PLDI Research Papers Samantha Frohlich University of Bristol, Jessica Foster University of Bristol, Alex Kavvos University of Bristol, Meng Wang University of Bristol DOI Pre-print | ||
11:40 20mTalk | CoTenN: Constrained Optimization with Tensor Networks PLDI Research Papers Ritvik Sharma Stanford University, Cheng Peng Stanford Institute for Materials and Energy Sciences, SLAC National Accelerator Laboratory, Siddharth Dangwal University of Chicago, Sara Achour Stanford University DOI | ||
12:00 20mTalk | Diagramming Program Values by Spatial Refinement PLDI Research Papers Siddhartha Prasad Brown University, Michael Tu Brown University, Karan Kashyap Brown University, Tim Nelson Brown University, Shriram Krishnamurthi Brown University DOI | ||
12:20 20mTalk | Persistent Iterators with Value Semantics PLDI Research Papers DOI | ||
11:00 - 12:40 | |||
11:00 20mTalk | Towards Removing Undef Values from LLVM IRDistinguished Paper 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 | ||
11:20 20mTalk | 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 | ||
11:40 20mTalk | 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 | ||
12:00 20mTalk | Hyper Separation Logic PLDI Research Papers Trayan Gospodinov INSAIT at Sofia University St. Kliment Ohridski, Peter Müller ETH Zurich, Thibault Dardinier EPFL DOI | ||
12:20 20mTalk | 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 | ||
12:40 - 14:00 | |||
12:40 - 14:00 | |||
12:40 80mLunch | Lunch Catering | ||
14:00 - 15:20 | |||
14:00 20mTalk | [SIGPLAN OOPSLA’25] Scalable and Accurate Application-Level Crash-Consistency Testing via Representative Testing PLDI Research Papers Yile Gu University of Washington, Ian Neal University of Michigan and Veridise, Jiexiao Xu University of Washington, Shaun Christopher Lee University of Washington, Ayman Said University of Michigan, Musa Haydar University of Michigan, Jacob Van Geffen , Andrew Quinn University of California at Santa Cruz, Baris Kasikci University of Washington | ||
14:20 20mTalk | Trace-Guided Synthesis of Effectful Test Generators PLDI Research Papers Zhe Zhou Purdue University, Ankush Desai Snowflake, Benjamin Delaware Purdue University, Suresh Jagannathan Purdue University DOI | ||
14:40 20mTalk | Semantic Reification: A New Paradigm for Random Program Generation PLDI Research Papers Kavya Chopra ETH Zurich, Cong Li ETH Zurich, Thodoris Sotiropoulos ETH Zurich, Zhendong Su ETH Zurich DOI Pre-print | ||
15:00 20mTalk | The Search for Constrained Random Generators PLDI Research Papers Harrison Goldstein SUNY Buffalo, Hila Peleg Technion, Cassia Torczon University of Pennsylvania, Daniel Sainati University of Pennsylvania, Leonidas Lampropoulos University of Maryland at College Park, Benjamin C. Pierce University of Pennsylvania DOI | ||
14:00 - 15:20 | |||
14:00 20mTalk | Versioned E-Graphs PLDI Research Papers Jahrim Gabriele Cesario University of St. Gallen, George Zakhour University of St. Gallen, Pascal Weisenburger University of St. Gallen, Guido Salvaneschi University of St. Gallen DOI Pre-print | ||
14:20 20mTalk | Improving Equality Saturation for EDA via Semantic E-Graphs PLDI Research Papers Sijie Kong University of California at Santa Barbara, Jingtao Xia University of California at Santa Barbara, Daniel Ruelas-Petrisko University of Washington, Zachary D. Sisco The Chinese University of Hong Kong, Shenzhen, Jonathan Balkind University of California at Santa Barbara, Gus Henry Smith Southmountain Research DOI | ||
14:40 20mTalk | Equality Saturation for Quantum Circuit Optimization PLDI Research Papers Ganxiang Yang Columbia University, Paige Raun University of Maryland, Runzhou Tao University of Maryland, Ronghui Gu Columbia University; CertiK DOI | ||
15:00 20mTalk | Fungible Memories for Automated Technology Mapping and Retargeting PLDI Research Papers Zachary D. Sisco The Chinese University of Hong Kong, Shenzhen, Sijie Kong University of California at Santa Barbara, Daniel Ruelas-Petrisko University of Washington, Jingtao Xia University of California at Santa Barbara, Julian Springer Technische Universität Berlin, Varun Rao University of California at Berkeley, Spencer Wang University of California at Santa Barbara, Gus Henry Smith Southmountain Research, Ben Hardekopf University of California at Santa Barbara, Jonathan Balkind University of California at Santa Barbara DOI | ||
15:20 - 15:50 | |||
15:20 30mCoffee break | Break Catering | ||
15:50 - 16:30 | |||
15:50 20mTalk | Adding Lifetimes and Ownership to Swift PLDI Events John McCall Apple | ||
16:10 20mTalk | Automating Context Inference at Scale for Security PLDI Events Tristan Ravitch Amazon | ||
15:50 - 17:50 | |||
16:40 - 18:00 | Boulder Dushanbe Tea HousePLDI Meetups at Flatirons Foyer Chair(s): Dakota Bryan University of Colorado, Boulder | ||
16:40 80mSocial Event | Boulder Dushanbe Tea House PLDI Meetups | ||
18:00 - 19:00 | |||
19:00 - 21:00 | |||
Fri 19 JunDisplayed time zone: Mountain Time (US & Canada) change
Fri 19 Jun
Displayed time zone: Mountain Time (US & Canada) change
09:00 - 10:10 | |||
09:00 70mKeynote | The Rise & Collapse of a Quantum State PLDI Research Papers Aws Albarghouthi University of Wisconsin-Madison | ||
10:10 - 11:00 | |||
10:10 50mCoffee break | Break Catering | ||
11:00 - 12:20 | |||
11:00 20mTalk | 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 | ||
11:20 20mTalk | A Categorical Basis for Robust Program Analysis PLDI Research Papers DOI | ||
11:40 20mTalk | Synthesizing Backward Error Bounds, BackwardDistinguished Paper PLDI Research Papers DOI Pre-print | ||
11:00 - 12:40 | |||
11:00 20mTalk | Let It Flow: A Formally Verified Compilation Framework for Asynchronous Dataflow PLDI Research Papers Zhengyao Lin Carnegie Mellon University, Yi Cai University of Maryland at College Park, Milijana Surbatovich University of Maryland at College Park DOI | ||
11:20 20mTalk | Compiling to Recurrent Neurons PLDI Research Papers Joey Velez-Ginorio University of Pennsylvania, Nada Amin Harvard University, Konrad Kording University of Pennsylvania, Steve Zdancewic University of Pennsylvania DOI | ||
11:40 20mTalk | [TOPLAS] Denotation-based Compositional Compiler Verification PLDI Research Papers Zhang Cheng Shanghai Jiao Tong University, Jiyang Wu , Di Wang Peking University, Qinxiang Cao Shanghai Jiao Tong University | ||
12:00 20mTalk | Responsive Parallelism with Dynamic and First-Class Priorities PLDI Research Papers Marelle León Illinois Institute of Technology, My Dinh Illinois Institute of Technology, Stefan K. Muller University of Connecticut DOI | ||
12:20 20mTalk | Escape with Your Self: Sound and Expressive Bidirectional Typing with Avoidance for Reachability Types PLDI Research Papers Songlin Jia Purdue University, Guannan Wei Tufts University, Siyuan He Purdue University, Yuyan Bao Augusta University, Tiark Rompf Purdue University DOI | ||
11:00 - 12:40 | |||
11:00 20mTalk | Compiling Strassen-like Matrix Multiplication Algorithms to Fast CUDA Kernels PLDI Research Papers Abhinav Jangda Microsoft Research DOI | ||
11:20 20mTalk | Parameterized Algorithms and Complexity for Function Merging with Branch Reordering PLDI Research Papers Amir K. Goharshady University of Oxford, Kerim Kochekov Hong Kong University of Science and Technology, Tian Shu Hong Kong University of Science and Technology, Ahmed Khaled Zaher Hong Kong University of Science and Technology DOI | ||
11:40 20mTalk | NEURA: A Unified and Retargetable Compilation Framework for Coarse-Grained Reconfigurable Architectures PLDI Research Papers Shangkun Li Hong Kong University of Science and Technology, Jinming Ge Hong Kong University of Science and Technology, Diyuan Tao Independent Researcher, Zeyu Li Hong Kong University of Science and Technology, Jiawei Liang Hong Kong University of Science and Technology, Linfeng Du Hong Kong University of Science and Technology, Jiang Xu Hong Kong University of Science and Technology (Guangzhou), Wei Zhang Hong Kong University of Science and Technology, Cheng Tan Google; Arizona State University DOI | ||
12:00 20mTalk | Neptune: Advanced ML Operator Fusion for Locality and Parallelism on GPUs PLDI Research Papers Yifan Zhao University of Illinois Urbana-Champaign, Egan Johnson University of Illinois Urbana-Champaign, Prasanth Chatarasi IBM Research, Vikram S. Adve University of Illinois Urbana-Champaign, Sasa Misailovic University of Illinois Urbana-Champaign DOI | ||
12:20 20mTalk | SparseZETA: Intelligent Auto-tuner for Designing High-Performance SpMV Programs PLDI Research Papers Zhen Du Institute of Computing Technology at Chinese Academy of Sciences, Ying Liu Institute of Computing Technology at Chinese Academy of Sciences; University of Chinese Academy of Sciences, Xionghui Chen Nanjing University, Yanbo Zhao North Carolina State University, Xiaobing Feng Institute of Computing Technology at Chinese Academy of Sciences; University of Chinese Academy of Sciences, Huimin Cui Institute of Computing Technology at Chinese Academy of Sciences; University of Chinese Academy of Sciences, Jiajia Li North Carolina State University DOI | ||
12:40 - 14:00 | |||
12:40 - 14:00 | |||
12:40 80mLunch | Lunch Catering | ||
14:00 - 15:40 | |||
14:00 20mTalk | Heterogeneous Dynamic Logic: Provability Modulo Program Theories PLDI Research Papers DOI | ||
14:20 20mTalk | Intrinsically Correct Algorithms and Recursive Coalgebras PLDI Research Papers Cass Alexandru RPTU Kaiserslautern-Landau & Radboud University Nijmegen, Henning Urbat Friedrich-Alexander University Erlangen-Nürnberg, Thorsten Wißmann Friedrich-Alexander University Erlangen-Nürnberg DOI Pre-print | ||
14:40 20mTalk | 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 | ||
15:00 20mTalk | 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 Pre-print | ||
15:20 20mTalk | [TOPLAS] Project Everest: Perspectives from Developing Industrial-Grade High-Assurance Software PLDI Research Papers Danel Ahman University of Tartu, 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 | ||
14:00 - 15:40 | |||
14:00 20mTalk | [SIGPLAN OOPSLA’25] Probabilistic Inference for Datalog with Correlated Inputs PLDI Research Papers Jingbo Wang Purdue University, Shashin Halalingaiah UT Austin, IIT Madras, Weiyi Chen Purdue University, Chao Wang University of Southern California, Işıl Dillig University of Texas at Austin | ||
14:20 20mTalk | A Hierarchy of Supermartingales for ω-Regular Verification PLDI Research Papers DOI | ||
14:40 20mTalk | Incremental Computation for Efficient Programmable Inference in Probabilistic Programs PLDI Research Papers Fabian Zaiser Massachusetts Institute of Technology, Jack Czenszak Yale University, Martin C. Rinard Massachusetts Institute of Technology, Vikash K. Mansinghka Massachusetts Institute of Technology, Alexander K. Lew Yale University DOI | ||
15:00 20mTalk | GradInf: Gradient Estimation as Probabilistic Inference PLDI Research Papers Gaurav Arya Carnegie Mellon University, Mathieu Huot Massachusetts Institute of Technology, Moritz Schauer Chalmers University of Technology - University of Gothenburg, Alexander K. Lew Yale University, Feras A. Saad Carnegie Mellon University DOI | ||
15:20 20mTalk | Categorical Semantics of Probabilistic Symbolic ExecutionDistinguished Paper PLDI Research Papers John Li Northeastern University, Jack Czenszak Yale University, Steven Holtzen Northeastern University DOI | ||
14:00 - 15:40 | |||
14:00 20mTalk | Cpp2Rust: Automatic Translation of C++ to Safe Rust PLDI Research Papers Lucian Popescu INESC-ID; Instituto Superior Técnico - University of Lisbon, Francisco Gouveia INESC-ID; Instituto Superior Técnico - University of Lisbon, Henrique Preto INESC-ID; Instituto Superior Técnico - University of Lisbon, João Silveira INESC-ID; Instituto Superior Técnico - University of Lisbon, Dmytro Hrybenko Google, José Fragoso Santos INESC-ID; Instituto Superior Técnico - University of Lisbon, Nuno P. Lopes INESC-ID; Instituto Superior Técnico - University of Lisbon DOI Pre-print | ||
14:20 20mTalk | &inator: Correct, Precise C-to-Rust Interface Translation PLDI Research Papers Victor Chen Ohio State University, Ayden Coughlin Ohio State University, Michael D. Bond Ohio State University DOI Pre-print | ||
14:40 20mTalk | Hayroll: A Modular Wrapper for Translating C Macros and Conditional Compilation to Rust PLDI Research Papers Haoran Peng University of Washington, Baris Kasikci University of Washington, Gilbert Louis Bernstein University of Washington, Michael D. Ernst University of Washington Link to publication DOI Pre-print | ||
15:00 20mTalk | VerusBelt: A Semantic Foundation for Verus’s Proof-Oriented Extensions to the Rust Type SystemDistinguished Paper PLDI Research Papers Travis Hance MPI-SWS, Laila Elbeheiry MPI-SWS, Yusuke Matsushita Kyoto University, Derek Dreyer MPI-SWS DOI | ||
15:20 20mTalk | Pure Borrow: Linear Haskell Meets Rust-Style Borrowing PLDI Research Papers DOI Pre-print | ||
15:40 - 16:10 | |||
15:40 30mCoffee break | Break Catering | ||
16:10 - 17:30 | |||
16:10 20mTalk | [SIGPLAN OOPSLA’25] 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:30 20mTalk | Bonsai: Compiling Queries to Pruned Tree TraversalsDistinguished Paper 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:50 20mTalk | A Compiler for Fused Relational Operations on Multisets PLDI Research Papers DOI | ||
17:10 20mTalk | 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 | ||
16:10 - 17:30 | |||
16:10 20mTalk | Simplifying Safety Proofs with Forward-Backward Reasoning and Prophecy PLDI Research Papers Eden Frenkel Tel Aviv University, Kenneth L. McMillan University of Texas at Austin, Oded Padon Weizmann Institute of Science, Sharon Shoham Tel Aviv University DOI | ||
16:30 20mTalk | TreeCoder: Systematic Exploration and Optimisation of Decoding and Constraints for LLM Code Generation PLDI Research Papers Henrijs Princis University of Bristol, Arindam Sharma University of Bristol, Cristina David University of Bristol DOI | ||
16:50 20mTalk | [TOPLAS] Guiding LLM-based Loop Invariant Synthesis via Feedback on Local Reasoning Errors PLDI Research Papers Tianchi Li Peking University, China, Zhenyu Yan Peking University, Junhao Liu Peking University, Peng Di Kunlunxin & UNSW Sydney, Xin Zhang Peking University | ||
17:10 20mTalk | [SIGPLAN OOPSLA’25] Active Learning for Neurosymbolic Program Synthesis PLDI Research Papers Celeste Barnaby University of Texas at Austin, Jocelyn Qiaochu Chen New York University, University of Alberta, Ramya Ramalingam , Osbert Bastani University of Pennsylvania, Işıl Dillig University of Texas at Austin | ||
16:10 - 17:30 | |||
16:10 20mTalk | Revisiting Partial Tracing for Safe, Efficient, and Concurrent Garbage Collection in Unmanaged Languages PLDI Research Papers DOI Pre-print | ||
16:30 20mTalk | Dynamically Checked Deep Immutability in Python PLDI Research Papers Fridtjof Stoldt Uppsala University, Sylvan Clebsch Microsoft Azure Research, Matthew A. Johnson Microsoft Azure Research, Matthew J. Parkinson Microsoft Azure Research, Tobias Wrigstad Uppsala University DOI | ||
16:50 20mTalk | FlexHeap: Dynamic I/O-Aware Heap Resizing for Managed Applications PLDI Research Papers Iacovos G. Kolokasis Foundation for Research and Technology Hellas; University of Crete, Shoaib Akram Australian National University, Foivos Zakkak Red Hat, Polyvios Pratikakis Foundation for Research and Technology Hellas; University of Crete, Angelos Bilas Foundation for Research and Technology Hellas; University of Crete DOI | ||
17:10 20mTalk | Virtualizing Continuations PLDI Research Papers Cong Ma University of Waterloo, Jonghyun Jung University of Waterloo, Yizhou Zhang University of Waterloo DOI | ||
18:00 - 20:00 | |||
18:00 - 20:00 | Hike in ChautauquaPLDI Meetups at Flatirons Foyer Chair(s): Dakota Bryan University of Colorado, Boulder | ||
18:00 2hSocial Event | Hike in Chautauqua PLDI Meetups | ||