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

Mon 15 Jun

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

09:00 - 12:00
Session 1EGRAPHS at Flatirons 2
09:00
25m
Talk
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:25
25m
Talk
Lifting E-Graphs: A Function Isn’t a Constant
EGRAPHS
Link to publication
09:51
25m
Talk
E-graphs modulo theories
EGRAPHS
Sofia Brookie Chalmers University of Technology
10:17
25m
Talk
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
10:42
25m
Talk
A Semi-Persistent E-Graph with Native AC Canonization and Leapfrog AC Matching.
EGRAPHS
Remi Delmas Amazon Web Services
11:08
25m
Talk
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
11:34
25m
Talk
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 - 12:00
Position papersPROPL at Flatirons 4
09:00
15m
Talk
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:15
30m
Talk
Marrying engineering rigor & scientific rigor for the planet
PROPL
Deepak Cherian Earthmover PBC
09:45
30m
Talk
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:00
30m
Talk
Mind the Gap: General-Purpose Programming Languages Impede Scientific Model Development and Communication
PROPL
Dominic Orchard University of Cambridge; University of Kent
11:30
30m
Talk
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
09:00 - 12:00
09:00
3h
Tutorial
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
14:00 - 17:00
Session 2EGRAPHS at Flatirons 2
14:00
22m
Talk
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:22
22m
Talk
A Joint Approach to Instruction Scheduling and Algebraic Rewriting with E-Graphs
EGRAPHS
Qiantan Hong Stanford University, Rupanshu Soi Stanford University, Alex Aiken Stanford University
14:45
22m
Talk
Answer Set Programming for Egg Extraction and More
EGRAPHS
Ziyi Yang National University of Singapore, Ilya Sergey National University of Singapore
15:07
22m
Talk
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
15:30
22m
Talk
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
15:52
22m
Talk
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:15
22m
Talk
Optimizing Optimizations, Declaratively: Optimizing the Higher-Order Functions in Mathematical Optimization with egglog
EGRAPHS
Pre-print
16:37
22m
Talk
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
14:00 - 15:20
Session 1: Advanced Compiler TuningLCTES at Flatirons 3
14:00
10m
Keynote
Opening Remarks
LCTES
Jeronimo Castrillon TU Dresden, Germany
14:10
22m
Talk
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
22m
Talk
CausalTuner: Feature-Aware Causal Guidance for Compiler Auto-tuningArtifacts Available
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
22m
Talk
Empirical Observations about Profile-Guided Optimizations for Mainstream C/C++ Compilers
LCTES
Soma Pal U. of Kansas, Prasad Kulkarni U. of Kansas
DOI
14:00 - 17:00
14:00
3h
Meeting
Working groups and discusison
PROPL

14:00 - 17:00
14:00
3h
Tutorial
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
15:45 - 17:00
Session 2: Binary Optimization & System SecurityLCTES at Flatirons 3
15:45
22m
Talk
DeduBB: Binary Code Size Reduction via Post-Link Basic Block DeduplicationResults ReproducedArtifacts AvailableArtifacts Evaluated
LCTES
Chaitanya Mamatha Ananda University of California Riverside, Mahbod Afarin University of California, Riverside, Rajiv Gupta University of California at Riverside (UCR), Sriraman Tallam Google Inc., Han Shen Google Inc, Xinliang Li Google
DOI
16:07
22m
Talk
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:30
10m
Short-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

Tue 16 Jun

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

09:00 - 12:30
09:00
3h30m
Tutorial
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:00
Keynote SessionLCTES at Flatirons 3
Chair(s): Jeronimo Castrillon TU Dresden, Germany
09:00
60m
Keynote
Practical Quantum Machine Learning: Overcoming the Bottlenecks of Scalability and Stability
LCTES
Aviral Shrivastava Arizona State University
File Attached
09:00 - 12:00
SOAP 1SOAP at Flatirons 4
09:00
10m
Day opening
Welcome and Opening Remarks
SOAP

09:10
60m
Keynote
How Context-Sensitive Static Analysis Led to the Best Smart Contract Decompiler
SOAP
Yannis Smaragdakis University of Athens
10:10
20m
Break
Coffee Break
SOAP

10:30
20m
Talk
Exploring Locally Bounded Translation Validation
SOAP
Alborz Jelvani Rutgers University, Richard P. Martin Rutgers University, Santosh Nagarakatte Rutgers University
10:50
20m
Talk
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:10
20m
Talk
Compile-Time Java Stream Fusion via mapMulti
SOAP
11:30
20m
Talk
Conditional Execution of Transpiler Passes Based on Per-Script Feature Detection
SOAP
09:00 - 10:10
KEYNOTE-1ARRAY at Meadows CD
Chair(s): Sreepathi Pai University of Rochester
09:00
10m
Day opening
Welcoming Remarks
ARRAY
Ganesh Gopalakrishnan University of Utah, Artjoms Šinkarovs University of Southampton
09:10
50m
Keynote
Tiles, Bricks, and Layouts: How Aggregate Data Abstractions Aid in Optimizing Data Movement
ARRAY
Mary Hall University of Utah
10:00
10m
Live Q&A
Q&A for Keynote-1
ARRAY

10:00 - 10:30
Short Paper SessionLCTES at Flatirons 3
Chair(s): Jeronimo Castrillon TU Dresden, Germany
10:00
10m
Short-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
10:10
10m
Short-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
10:20
10m
Short-paper
Scheduled Partial-Credit RL for Reliable Code Generation with Small Language Models (WIP)
LCTES
Suryansh Singh Sijwali The Pennsylvania State University, Suman Saha pc
DOI
10:30 - 12:10
Array Programming and VerificationARRAY at Meadows CD
Chair(s): Jubi Taneja Gimlet Labs
10:30
20m
Talk
Refined Remora: Constraining Array Shapes
ARRAY
Vadym Matviichuk Northeastern University, Olin Shivers Northeastern University
10:50
25m
Talk
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:15
25m
Talk
Graded Monoids for Dependently Typed Array Programming
ARRAY
Juuso Haavisto University of Oxford, Jeremy Gibbons Department of Computer Science, University of Oxford
11:40
20m
Talk
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:00
10m
Live Q&A
Mini Panel
ARRAY

10:50 - 12:00
Session 3: Formal Methods and Systems ReliabilityLCTES at Flatirons 3
10:50
22m
Talk
Towards Verifiable System Code using a DSL Compiled to Efficient and Readable C CodeArtifacts AvailableArtifacts Evaluated
LCTES
Clément Chavanon Inria, Univ Rennes, CNRS, IRISA, Henrik Karlsson KTH Royal Institute of Technology, Frédéric Besson Univ Rennes, Inria, CNRS, IRISA, Sandrine Blazy University of Rennes, Roberto Guanciale KTH Royal Institute of Technology
DOI
11:12
22m
Talk
A Pointer-Ownership Model for C Inspired by RustResults ReproducedArtifacts AvailableArtifacts Evaluated
LCTES
David Svoboda , William Klieber Software Engineering Institute, Carnegie Mellon University, Lori Flynn CERT, Ruben Martins Carnegie Mellon University, Jeffrey Hoskinson Software Engineering Institute, Carnegie Mellon University
DOI
11:34
22m
Talk
Hikami: A Lightweight Hypervisor for Emulating RISC-V Extension Semantics with Sail-Driven Auto-generationResults ReproducedArtifacts Available
LCTES
Norimasa Takana University of Tsukuba, Yoshihiro Oyama University of Tsukuba
DOI
13:40 - 15:20
KEYNOTE-2 and Tensorial ThemesARRAY at Meadows CD
Chair(s): Sangeeta Chowdhary AMD Research
13:40
50m
Keynote
The Shape of Things to Come
ARRAY
14:30
10m
Live Q&A
Q&A for Keynote-2
ARRAY

14:40
20m
Talk
Tensor Algebra Equivalence Checker
ARRAY
Jubi Taneja Gimlet Labs, Tom St. John Gimlet Labs, Natalie Serrino Gimlet Labs
15:00
20m
Talk
Rhyme: A Multi-Paradigm Declarative Query Language
ARRAY
Ran Guo Purdue University, Tiark Rompf Purdue University
14:00 - 15:10
Session 4: Specialized Hardware and Accelerator DesignLCTES at Flatirons 3
14:00
22m
Talk
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:22
22m
Talk
Sirop: A Small IR for HLS with Parallel PatternsResults ReproducedArtifacts AvailableArtifacts Evaluated
LCTES
Louis Hildebrand McGill University, Christophe Dubach McGill University
DOI
14:44
22m
Talk
A Functional Approach to Synthesizing Routable Programmable Accelerators for Neural NetworksResults ReproducedArtifacts AvailableArtifacts Evaluated
LCTES
Tzung-Han Juang McGill University, Paul Teng McGill University, Canada, Christophe Dubach McGill University
DOI
14:00 - 18:00
SOAP 2SOAP at Flatirons 4
14:00
60m
Keynote
Compositional Data-Flow Analysis at Industrial Scale
SOAP
Michael Emmi Amazon Web Services
15:00
20m
Talk
Scaling Static Code Analysis Adoption at WhatsApp iOS
SOAP
15:20
20m
Talk
On the Effectiveness of Modular Testing in EvoSuite
SOAP
Elizabeth Dinella Bryn Mawr College
15:40
20m
Break
Coffee Break
SOAP

16:00
60m
Keynote
Compiler-assisted Translation Validation
SOAP
Qirun Zhang Georgia Institute of Technology
17:00
20m
Talk
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:20
20m
Talk
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:40
10m
Day closing
Closing Remarks
SOAP

15:30 - 17:00
Session 5: Memory Efficiency and Control-Flow AnalysisLCTES at Flatirons 3
15:30
22m
Talk
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
15:52
22m
Talk
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:15
22m
Talk
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:37
22m
Talk
On the Origins of Indirect Jumps in Embedded SoftwareResults ReproducedArtifacts AvailableArtifacts Evaluated
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
15:50 - 17:30
HPC ProgrammingARRAY at Meadows CD
15:50
20m
Talk
Vectorizing Sparse Coiteration for Two-finger Loop Structure (Extended Abstract)
ARRAY
Kabilan Mahathevan Virginia Tech, Kirshanthan Sundararajah Virginia Tech
16:10
25m
Talk
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
20m
Talk
Lazy Arithmetic using Systolic Arrays for Closing the Verification Gap on Embedded Systems
ARRAY
Taisa Kushner Galois, Ryan McCleeary Galois, Martin Brain City St. George's, University of London
16:55
20m
Talk
Towards a Linear-Algebraic Hypervisor
ARRAY
Pre-print
17:15
5m
Research preview
Semantics as a Tool of Thought: Provenance-Aware Dimensional Checking in a Reactive Array IR
ARRAY
17:20
10m
Live Q&A
Mini Panel
ARRAY

Wed 17 Jun

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

10:30 - 12:10
Mechanized Program Logics and VerificationPLDI Research Papers at Flatirons 2
10:30
20m
Talk
A Deductive System for Contract Satisfaction Proofs
PLDI Research Papers
Arthur Correnson CISPA Helmholtz Center for Information Security, Haoyi Zeng Harvard University, Jana Hofmann MPI-SP
DOI Pre-print
10:50
20m
Talk
A Mechanized Algebra of Verified Data Structures for Optimizing Sparse Tensor Programs
PLDI Research Papers
Amanda Liu Massachusetts Institute of Technology, Gilbert Louis Bernstein University of Washington, Shoaib Kamil Adobe, Adam Chlipala Massachusetts Institute of Technology, Jonathan Ragan-Kelley Massachusetts Institute of Technology
DOI
11:10
20m
Talk
Iris-WasmFX: Modular Reasoning for Wasm Stack Switching
PLDI Research Papers
Maxime Legoupil Nanyang Technological University, Mathias Pedersen Aarhus University, Lars Birkedal Aarhus University, Sam Lindley University of Edinburgh, Jean Pichon-Pharabod Aarhus University
DOI
11:30
20m
Talk
Code-Specify-Test-Debug-Prove: Flexibly Integrating Separation Logic Specification into Conventional Workflows
PLDI Research Papers
Zain K Aamer University of Pennsylvania, Rini Banerjee University of Cambridge, Hiroyuki Katsura University of Cambridge, David Kaloper-Meršinjak University of Cambridge, Dimitrios J. Economou University of Cambridge, Kayvan Memarian University of Cambridge, Dhruv Makwana University of Cambridge, Neel Krishnaswami University of Cambridge, Benjamin C. Pierce University of Pennsylvania, Christopher Pulte University of Oxford, Peter Sewell University of Cambridge
DOI Pre-print
11:50
20m
Talk
Cerisier: A Program Logic for Attestation in a Capability Machine
PLDI Research Papers
June Rousseau Aarhus University, Denis Carnier KU Leuven, Thomas Van Strydonck Fortanix, Steven Keuchel KU Leuven, Dominique Devriese KU Leuven, Lars Birkedal Aarhus University
DOI
10:30 - 12:10
Specification Synthesis and VerificationPLDI Research Papers at Flatirons 3
10:30
20m
Talk
[SIGPLAN] Counterexample-Guided Inference of Modular Specifications
PLDI Research Papers
William Hallahan Binghamton, Ranjit Jhala University of California at San Diego, Ruzica Piskac Yale University
10:50
20m
Talk
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:10
20m
Talk
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
11:30
20m
Talk
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
11:50
20m
Talk
Expecto: Extracting Formal Specifications from Natural Language Description for Trustworthy Oracles
PLDI Research Papers
Dongjae Lee KAIST, Kihong Heo KAIST
DOI
10:30 - 12:10
Quantum ComputingPLDI Research Papers at Flatirons 4
10:30
20m
Talk
Verification of Recursively Defined Quantum Circuits
PLDI Research Papers
Mingsheng Ying University of Technology Sydney, Zhicheng Zhang University of Technology Sydney
DOI
10:50
20m
Talk
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:10
20m
Talk
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
11:30
20m
Talk
[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
11:50
20m
Talk
Cobble: Compiling Block Encodings for Quantum Computational Linear Algebra
PLDI Research Papers
Charles Yuan University of Wisconsin-Madison
DOI
13:40 - 15:20
Networking and Distributed SystemsPLDI Research Papers at Flatirons 2
13:40
20m
Talk
A Formally Verified Foundation for Compositional Heterogeneous Coherence
PLDI Research Papers
An Qi Zhang University of Utah, Andrés Goens TU Darmstadt, Daniel Sorin Duke University, Vijay Nagarajan University of Utah
DOI
14:00
20m
Talk
MatchBox: A Semantic Foundation for Data Plane Portability
PLDI Research Papers
Eric Hayden Campbell University of Texas at Austin, Robert Zhang University of Texas at Austin, Divyanshu Saxena University of Texas at Austin, Aditya Akella University of Texas at Austin, Işıl Dillig University of Texas at Austin
DOI
14:20
20m
Talk
SureDistrib: Verifying Almost-Sure Termination of Composite Asynchronous Byzantine Protocols
PLDI Research Papers
Longfei Qiu Yale University, Jingqi Xiao University of Hong Kong, Ji-Yong Shin Northeastern University, Zhong Shao Yale University
DOI
14:40
20m
Talk
Implementability of Global Distributed Protocols Modulo Network Architectures
PLDI Research Papers
Elaine Li New York University, Thomas Wies New York University
DOI
15:00
20m
Talk
Weighted NetKAT: A Programming Language For Quantitative Network Verification
PLDI Research Papers
Emmanuel Suárez Acevedo Cornell University, Tiago Ferreira University College London, Kevin Batz Cornell University, Oliver Emil Bøving Technical University of Denmark, Nate Foster EPFL; Jane Street, Alexandra Silva Cornell University
DOI
13:40 - 15:20
13:40
20m
Talk
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:00
20m
Talk
Fixed Parameter Tractable Linearizability Monitoring
PLDI Research Papers
Zheng Han Lee National University of Singapore, Umang Mathur National University of Singapore
DOI Pre-print
14:20
20m
Talk
SuperCollider: Scalable and Effective Data Race Detection for CUDA
PLDI Research Papers
DOI
14:40
20m
Talk
Fast Atomicity Monitoring
PLDI Research Papers
Hünkar Can Tunç Uber, Yifan Dong Aarhus University, Andreas Pavlogiannis Aarhus University
DOI
13:40 - 15:20
Static Analysis 1PLDI Research Papers at Flatirons 4
13:40
20m
Talk
Flow-Analysis-Based Closure Optimization
PLDI Research Papers
John Reppy University of Chicago, Olin Shivers Northeastern University, Byron Zhong University of Chicago
DOI
14:00
20m
Talk
SSA without Dominance for Higher-Order Programs
PLDI Research Papers
Roland Leißa University of Göttingen, Johannes Griebler University of Göttingen
DOI Pre-print
14:20
20m
Talk
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
14:40
20m
Talk
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:00
20m
Talk
Bridging Coverage and Confidence: Reliable Static False Alarm Elimination via Input-Agnosticity
PLDI Research Papers
Jiayi Wang Nanjing University, Yu Wang Nanjing University, Linzhang Wang Nanjing University, Ke Wang Nanjing University
DOI
15:50 - 17:30
Abstract InterpretationPLDI Research Papers at Flatirons 2
15:50
20m
Talk
Path-Sensitive Abstract Interpretation for WCET Estimation
PLDI Research Papers
Shangshang Xiao Shandong University, Mengxia Sun Shandong University, Wei Zhang Shandong University, Naijun Zhan Peking University; Zhongguancun Laboratory, Lei Ju Shandong University
DOI
16:10
20m
Talk
SAIL: Sound Abstract Interpreters with LLMs
PLDI Research Papers
Qiuhan Gu University of Illinois Urbana-Champaign, Avaljot Singh University of Illinois Urbana-Champaign, Gagandeep Singh University of Illinois Urbana-Champaign
DOI
16:30
20m
Talk
Evolving Abstract Transformers for Gradient-Guided, Adaptable Abstract Interpretation
PLDI Research Papers
Shaurya Gomber University of Illinois Urbana-Champaign, Debangshu Banerjee University of Illinois Urbana-Champaign, Gagandeep Singh University of Illinois Urbana-Champaign
DOI Pre-print
16:50
20m
Talk
Abstract Interpretation with Confidence
PLDI Research Papers
Yuanfeng Shi Peking University, Ziyue Jin Peking University, Xin Zhang Peking University
DOI
17:10
20m
Talk
Optimism in Equality Saturation
PLDI Research Papers
Russel Arbore University of California at Berkeley, Alvin Cheung University of California at Berkeley, Max Willsey University of California at Berkeley
DOI Pre-print
15:50 - 17:30
15:50
20m
Talk
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
16:10
20m
Talk
Modular GPU Programming with Typed Perspectives
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:30
20m
Talk
[TOPLAS] StreamAlloc: A Framework for Analyzing and Transforming CUDA Code to Enable Asynchronous Execution
PLDI Research Papers
Soumik Kumar Basu IIT Hyderabad, Jyothi Vedurada IIT Hyderabad
16:50
20m
Talk
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
17:10
20m
Talk
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
15:50 - 17:30
15:50
20m
Talk
[SIGPLAN] Probabilistic Refinement Session Types
PLDI Research Papers
Qiancheng Fu Boston University, Ankush Das Boston University, Marco Gaboardi Boston University
16:10
20m
Talk
[SIGPLAN] 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:30
20m
Talk
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
16:50
20m
Talk
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:10
20m
Talk
Syntactic Implicit Parameters with Static Overloading
PLDI Research Papers
Daan Leijen Microsoft Research, Tim Whiting Brigham Young University
DOI Pre-print

Thu 18 Jun

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

09:00 - 10:10
09:00
70m
Keynote
Happiness U-Curve: Navigating the AI Validation Bottleneck
PLDI Research Papers
Miryung Kim UCLA and Amazon Web Services
10:30 - 11:50
Symbolic Methods for Verification and MatchingPLDI Research Papers at Flatirons 2
10:30
20m
Talk
Solvable Tuple Patterns and Their Applications to Program Verification
PLDI Research Papers
Naoki Kobayashi University of Tokyo, Ryosuke Sato Tokyo University of Agriculture and Technology, Ayumi Shinohara Tohoku University, Ryo Yoshinaka Tohoku University
DOI
10:50
20m
Talk
An Efficient Algorithm for Streaming BPE Tokenization
PLDI Research Papers
Konstantinos Mamouras Rice University, Angela W. Li Rice University, Yudi Yang Rice University
DOI
11:10
20m
Talk
Scalable Floating-Point Satisfiability via Staged Optimization
PLDI Research Papers
Yuanzhuo Zhang Virginia Tech, Zhoulai Fu SUNY Korea; Virginia Tech; Stony Brook University, Binoy Ravindran Virginia Tech
DOI
11:30
20m
Talk
EREQ: Regular Expressions with Quantifiers and Incremental Quantifier Elimination
PLDI Research Papers
Ekaterina Zhuchko Tallinn University of Technology, Ian Erik Varatalu Tallinn University of Technology, Margus Veanes Microsoft Research, Nikolaj Bjørner Microsoft Research
DOI
10:30 - 12:10
Domain-Specific LanguagesPLDI Research Papers at Flatirons 3
10:30
20m
Talk
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
10:50
20m
Talk
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
11:10
20m
Talk
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
11:30
20m
Talk
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
11:50
20m
Talk
Persistent Iterators with Value Semantics
PLDI Research Papers
Yihe Li National University of Singapore, Gregory J. Duck National University of Singapore
DOI
10:30 - 12:10
Semantics and Hyperproperty ReasoningPLDI Research Papers at Flatirons 4
10:30
20m
Talk
Towards Removing Undef Values from LLVM IR
PLDI Research Papers
Pedro Lobo INESC-ID; Instituto Superior Técnico - University of Lisbon, John McIver Virginia Tech, George Mitenkov Aptos, Juneyoung Lee AWS, Kirshanthan Sundararajah Virginia Tech, Nuno P. Lopes INESC-ID; Instituto Superior Técnico - University of Lisbon
DOI Pre-print
10:50
20m
Talk
The Downgrading Semantics of Memory Safety
PLDI Research Papers
René Rydhof Hansen Aalborg University, Andreas Stenbæk Larsen Aarhus University, Aslan Askarov Aarhus University
DOI
11:10
20m
Talk
Causality and Semantic Separation
PLDI Research Papers
Anna Zhang Massachusetts Institute of Technology, Qinglan Luo Wellesley College; Massachusetts Institute of Technology, London Bielicke University of California at Los Angeles, Eunice Jun University of California at Los Angeles, Adam Chlipala Massachusetts Institute of Technology
DOI
11:30
20m
Talk
Hyper Separation Logic
PLDI Research Papers
Trayan Gospodinov INSAIT at Sofia University St. Kliment Ohridski, Peter Müller ETH Zurich, Thibault Dardinier EPFL
DOI
11:50
20m
Talk
Pantomime: Constructive Leakage Proofs via Simulation
PLDI Research Papers
Robin Webbers Vrije Universiteit Amsterdam, Robert Schenck Northeastern University, Wind Wong Vrije Universiteit Amsterdam, Kristina Sojakova Vrije Universiteit Amsterdam, Klaus von Gleissenthall Vrije Universiteit Amsterdam
DOI
13:40 - 15:00
Generative Testing and Program SynthesisPLDI Research Papers at Flatirons 2
13:40
20m
Talk
[SIGPLAN] 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:00
20m
Talk
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:20
20m
Talk
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
14:40
20m
Talk
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
13:40 - 15:00
Formal Verification of Probabilistic ProgramsPLDI Research Papers at Flatirons 3
13:40
20m
Talk
Contextual Refinement of Higher-Order Concurrent Probabilistic Programs
PLDI Research Papers
Kwing Hei Li Aarhus University, Alejandro Aguirre Aarhus University, Joseph Tassarotti New York University, Lars Birkedal Aarhus University
DOI
14:00
20m
Talk
Supermartingales for Unique Fixed Points: A Unified Approach to Lower Bound Verification
PLDI Research Papers
Satoshi Kura Waseda University, Hiroshi Unno Tohoku University, Takeshi Tsukada Chiba University
DOI
14:20
20m
Talk
SuperDP: Differential Privacy Refutation via Supermartingales
PLDI Research Papers
Krishnendu Chatterjee IST Austria, Ehsan Kafshdar Goharshady IST Austria, Đorđe Žikelić Singapore Management University
DOI
14:40
20m
Talk
Modular Verification of Differential Privacy in Probabilistic Higher-Order Separation Logic
PLDI Research Papers
Philipp G. Haselwarter Aarhus University, Alejandro Aguirre Aarhus University, Simon Oddershede Gregersen CISPA Helmholtz Center for Information Security, Kwing Hei Li Aarhus University, Joseph Tassarotti New York University, Lars Birkedal Aarhus University
Link to publication DOI Pre-print
13:40 - 15:00
Equality SaturationPLDI Research Papers at Flatirons 4
13:40
20m
Talk
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:00
20m
Talk
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:20
20m
Talk
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
14:40
20m
Talk
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:50 - 16:30
Industry SessionPLDI Events at Flatirons 2
15:50
20m
Talk
Adding Lifetimes and Ownership to Swift
PLDI Events
16:10
20m
Talk
TBA
PLDI Events

Fri 19 Jun

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

09:00 - 10:10
09:00
70m
Keynote
The Rise & Collapse of a Quantum State
PLDI Research Papers
Aws Albarghouthi University of Wisconsin-Madison
10:30 - 11:50
Static Analysis 2PLDI Research Papers at Flatirons 2
10:30
20m
Talk
Verifying Array Properties in Pure Data-Parallel Programs
PLDI Research Papers
Nikolaj Hey Hinnerskov University of Copenhagen, Robert Schenck Northeastern University, Cosmin E. Oancea University of Copenhagen
DOI
10:50
20m
Talk
A Categorical Basis for Robust Program Analysis
PLDI Research Papers
Zachary Kincaid Princeton University, Shaowei Zhu Princeton University
DOI
11:10
20m
Talk
Restart and Refine: Scalable IFDS Taint Analysis across Memory Budgets
PLDI Research Papers
DOI
11:30
20m
Talk
Synthesizing Backward Error Bounds, Backward
PLDI Research Papers
Laura Zielinski Cornell University, Justin Hsu Cornell University
DOI Pre-print
10:30 - 12:10
Verified Compilation and Type SystemsPLDI Research Papers at Flatirons 3
10:30
20m
Talk
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
10:50
20m
Talk
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:10
20m
Talk
[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
11:30
20m
Talk
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
11:50
20m
Talk
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
10:30 - 12:10
Compiler Optimization for AcceleratorsPLDI Research Papers at Flatirons 4
10:30
20m
Talk
Compiling Strassen-like Matrix Multiplication Algorithms to Fast CUDA Kernels
PLDI Research Papers
Abhinav Jangda Microsoft Research
DOI
10:50
20m
Talk
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:10
20m
Talk
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
11:30
20m
Talk
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
11:50
20m
Talk
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
13:40 - 15:20
Verification and Proof ReasoningPLDI Research Papers at Flatirons 2
13:40
20m
Talk
Heterogeneous Dynamic Logic: Provability Modulo Program Theories
PLDI Research Papers
DOI
14:00
20m
Talk
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:20
20m
Talk
CRIS: The Power of Imagination in Hybrid Verification
PLDI Research Papers
Yonghee Kim Seoul National University, Taeyoung Yoon Seoul National University, Sanghyun Yi Seoul National University, Jaehyung Lee Seoul National University, Soonwon Moon Seoul National University, Yeji Han Seoul National University, Seonho Lee Seoul National University, Taeyoung Rhee Seoul National University, Yujin Im Seoul National University, Donghyun Nam Seoul National University, Jieung Kim Yonsei University, Chung-Kil Hur Seoul National University
DOI
14:40
20m
Talk
Navigating AND–OR Graph Modifications to Debug Failing Proof Search
PLDI Research Papers
Justin Lubin University of California at Berkeley, Marlena Preigh University of California at Berkeley, Max Willsey University of California at Berkeley, Sarah E. Chasins University of California at Berkeley
DOI Pre-print
15:00
20m
Talk
[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
13:40 - 15:20
Probabilistic Inference and VerificationPLDI Research Papers at Flatirons 3
13:40
20m
Talk
[SIGPLAN] 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:00
20m
Talk
A Hierarchy of Supermartingales for ω-Regular Verification
PLDI Research Papers
Satoshi Kura Waseda University, Hiroshi Unno Tohoku University
DOI
14:20
20m
Talk
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
14:40
20m
Talk
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:00
20m
Talk
Categorical Semantics of Probabilistic Symbolic Execution
PLDI Research Papers
John Li Northeastern University, Jack Czenszak Yale University, Steven Holtzen Northeastern University
DOI
13:40 - 15:20
Rust Translation and BorrowingPLDI Research Papers at Flatirons 4
13:40
20m
Talk
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:00
20m
Talk
&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:20
20m
Talk
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
DOI Pre-print
14:40
20m
Talk
VerusBelt: A Semantic Foundation for Verus’s Proof-Oriented Extensions to the Rust Type System
PLDI Research Papers
Travis Hance MPI-SWS, Laila Elbeheiry MPI-SWS, Yusuke Matsushita Kyoto University, Derek Dreyer MPI-SWS
DOI
15:00
20m
Talk
Pure Borrow: Linear Haskell Meets Rust-Style Borrowing
PLDI Research Papers
Yusuke Matsushita Kyoto University, Hiromi Ishii JIJ
DOI Pre-print
15:50 - 17:10
Optimization of Data PipelinesPLDI Research Papers at Flatirons 2
15:50
20m
Talk
[SIGPLAN] Homomorphism Calculus for User-Defined Aggregations
PLDI Research Papers
Ziteng Wang University of Texas at Austin, Ruijie Fang University of Texas at Austin, Linus Zheng University of Texas at Austin, Dixin Tang University of Texas at Austin, Işıl Dillig University of Texas at Austin
16:10
20m
Talk
Bonsai: Compiling Queries to Pruned Tree Traversals
PLDI Research Papers
Alexander J Root Stanford University, Christophe Gyurgyik Stanford University, Purvi Goel Stanford University, Kayvon Fatahalian Stanford University, Jonathan Ragan-Kelley Massachusetts Institute of Technology, Andrew Adams Adobe Research, Fredrik Kjolstad Stanford University
DOI Pre-print
16:30
20m
Talk
A Compiler for Fused Relational Operations on Multisets
PLDI Research Papers
James Dong Stanford University, Fredrik Kjolstad Stanford University
DOI
16:50
20m
Talk
Optimal Predicate Pushdown Synthesis
PLDI Research Papers
Robert Zhang University of Texas at Austin, Eric Hayden Campbell University of Texas at Austin, Dixin Tang University of Texas at Austin, Işıl Dillig University of Texas at Austin
DOI
15:50 - 17:10
15:50
20m
Talk
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:10
20m
Talk
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:30
20m
Talk
[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
16:50
20m
Talk
[SIGPLAN] 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
15:50 - 17:10
Runtime Memory and Control AbstractionsPLDI Research Papers at Flatirons 4
15:50
20m
Talk
Revisiting Partial Tracing for Safe, Efficient, and Concurrent Garbage Collection in Unmanaged Languages
PLDI Research Papers
Jeonghyeon Kim KAIST, Jongse Park KAIST, Youngjin Kwon KAIST, Jeehoon Kang FuriosaAI
DOI Pre-print
16:10
20m
Talk
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:30
20m
Talk
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
16:50
20m
Talk
Virtualizing Continuations
PLDI Research Papers
Cong Ma University of Waterloo, Jonghyun Jung University of Waterloo, Yizhou Zhang University of Waterloo
DOI