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

Mon 13 Jun

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

08:00 - 09:00
Monday RegistrationPLDI at Kon-Tiki Foyer
08:00
60m
Registration
Registration
PLDI

09:00 - 10:00
Morning IMAPS at Boardroom
Chair(s): Charles Sutton Google Research
09:00
45m
Keynote
Competitive Programming with AlphaCodevirtual
MAPS
Yujia Li Deepmind
09:00 - 10:00
TalkPLMW at Kon-Tiki
09:00
60m
Talk
Verified Trustworthy Software Specification
PLMW
Philippa Gardner Imperial College London
09:00 - 10:00
Invited TalkARRAY at Macaw
09:00
60m
Talk
Multidimensional C++
ARRAY
File Attached
09:00 - 10:00
(Tutorial) Checked C Part ITutorials at Rousseau Center +12h
09:00
60m
Tutorial
Making C Programs Safer with Checked C
Tutorials
Jie Zhou University of Rochester, Yudi Yang University of Rochester, USA, Michael Hicks University of Maryland at College Park, John Criswell University of Rochester, USA
09:00 - 09:50
Session 1Infer at Rousseau East
Chair(s): Dulma Churchill Facebook London
09:00
40m
Talk
Three years of analyzing Ada code with Infer: a retrospectivevirtual
Infer
09:40
10m
Live Q&A
Q&A 1
Infer

09:00 - 10:00
(Tutorial) Discover[i] Part ITutorials at Rousseau West +12h
09:00
60m
Tutorial
Discover[i]: Taming Unbounded Distributed Systems with Modular, Bounded Reasoning
Tutorials
Roopsha Samanta Purdue University, Nouraldin Jaber Purdue University, Christopher Wagner Purdue University
09:00 - 10:00
(Tutorial) Egg Part ITutorials at Toucan +12h
09:00
60m
Tutorial
Build your own optimizer with egg!
Tutorials
Max Willsey University of Washington, Zachary Tatlock University of Washington
10:00 - 10:30
PLTea (Mon AM)PLMW at Kon-Tiki Foyer
Chair(s): Rachit Nigam Cornell University
10:00
30m
Social Event
PLTeasocial
PLMW

10:20 - 12:00
Session 2Infer at Rousseau East +12h
Chair(s): Nikos Gorogiannis Facebook
10:20
40m
Talk
Higher-order function specialization in Infervirtual
Infer
11:00
10m
Live Q&A
Q&A 2
Infer

11:10
40m
Talk
InfERL: Scalable and extensible static analysis for Erlangvirtual
Infer
11:50
10m
Live Q&A
Q&A 3
Infer

10:30 - 12:00
Morning IIMAPS at Boardroom +12h
Chair(s): Satish Chandra Facebook
10:30
45m
Keynote
Improving Software Reliability using Machine Learningvirtual
MAPS
Baishakhi Ray Columbia University
11:15
15m
Talk
Productivity Assessment of Neural Code Completion
MAPS
Pre-print
11:30
15m
Talk
Predictive Synthesis of API-Centric Code
MAPS
Daye Nam CMU, Carnegie Mellon University, Baishakhi Ray Columbia University, Seohyun Kim Meta, xianshan qu , Satish Chandra Facebook
Pre-print
11:45
15m
Talk
From Perception to Programs: Regularize, Overparameterize, and Amortize
MAPS
Hao Tang Cornell University, Kevin Ellis Cornell University
10:30 - 12:00
Monday MorningCommute at Cockatoo
10:30
10m
Talk
Welcome Remarks
Commute
Azadeh Farzan University of Toronto, Constantin Enea Ecole Polytechnique / LIX / CNRS, Eric Koskinen Stevens Institute of Technology
10:40
30m
Talk
Practical Smart Contract Sharding with Commutativity Analysis
Commute
Ilya Sergey National University of Singapore
11:10
10m
Live Q&A
Discussion
Commute

11:20
30m
Talk
Commutativity reasoning for automated distributed coordination
Commute
Mohsen Lesani University of California at Riverside
11:50
10m
Live Q&A
Discussion
Commute

10:30 - 12:00
Panel DiscussionPLMW at Kon-Tiki
10:30
90m
Panel
Mentoring Panel: Surviving Grad School
PLMW
Sunjay Cauligi University of California at San Diego, USA, Ethan Cecchetti University of Maryland, College Park, Niki Vazou IMDEA Software Institute, Ningning Xie University of Toronto, S: Tamara Rezk INRIA
10:30 - 12:00
Array Languages for ApplicationsARRAY at Macaw +12h
10:30
22m
Talk
Distributed parallel computing with Futhark
ARRAY
Michaël El Kharroubi University of Applied Sciences and Arts Western Switzerland, Baptiste Coudray , Orestis Malaspinas
10:52
22m
Talk
Mech: An Array Programming Language for Robots (extended abstract)
ARRAY
Corey Montella Lehigh University
11:15
22m
Talk
Probabilistic Array Programming on Galois Fields (extended abstract)
ARRAY
Breandan Considine McGill University, Jin L.C. Guo McGill University, Xujie Si McGill University, Canada
11:37
22m
Talk
Parallel Scan As a Multidimensional Array Problem
ARRAY
Artjoms Šinkarovs Heriot-Watt University, UK, Sven-Bodo Scholz Heriot-Watt University
10:30 - 12:00
(Tutorial) Checked C Part IITutorials at Rousseau Center +12h
10:30
90m
Tutorial
Making C Programs Safer with Checked C
Tutorials
Jie Zhou University of Rochester, Yudi Yang University of Rochester, USA, Michael Hicks University of Maryland at College Park, John Criswell University of Rochester, USA
10:30 - 12:00
(Tutorial) Discover[i] Part IITutorials at Rousseau West +12h
10:30
90m
Tutorial
Discover[i]: Taming Unbounded Distributed Systems with Modular, Bounded Reasoning
Tutorials
Roopsha Samanta Purdue University, Nouraldin Jaber Purdue University, Christopher Wagner Purdue University
10:30 - 12:00
(Tutorial) Egg Part IITutorials at Toucan +12h
10:30
90m
Tutorial
Build your own optimizer with egg!
Tutorials
Max Willsey University of Washington, Zachary Tatlock University of Washington
12:00 - 13:00
Monday LunchPLDI at Beach North
12:00
60m
Lunch
Lunchsocial
PLDI

13:30 - 15:00
AfternoonMAPS at Boardroom +12h
Chair(s): Charles Sutton Google Research
13:30
45m
Keynote
Can Transformers Code?virtual
MAPS
14:15
15m
Talk
Syntax-Guided Program Reduction for Understanding Neural Code Intelligence Modelsvirtual
MAPS
Md Rafiqul Islam Rabin University of Houston, Aftab Hussain University of Houston, Amin Alipour University of Houston
DOI Pre-print
14:30
15m
Talk
A Systematic Evaluation of Large Language Models of Codevirtual
MAPS
Frank F. Xu Carnegie Mellon University, Uri Alon Carnegie Mellon University, Graham Neubig Carnegie Mellon University, Vincent J. Hellendoorn Carnegie Mellon University
14:45
15m
Poster
Poster Session
MAPS

13:30 - 15:00
Monday AfternoonCommute at Cockatoo
13:30
30m
Talk
A Tree Clock Data Structure for Causal Orderings in Concurrent Executions
Commute
Andreas Pavlogiannis Aarhus University
14:00
10m
Live Q&A
Discussion
Commute

14:10
30m
Talk
Commutativity condition synthesis and language support for commute blocks
Commute
Eric Koskinen Stevens Institute of Technology
14:40
10m
Live Q&A
Discussion
Commute

14:50
5m
Talk
Lightning: Servois2: An Extended Commutativity Condition Synthesizer
Commute
Adam Chen Stevens Institute of Technology
13:30 - 15:00
TalkPLMW at Kon-Tiki +12h
13:30
90m
Talk
Your Research and Everyone Else
PLMW
Martin C. Rinard Massachusetts Institute of Technology
13:30 - 15:00
(Tutorial) Alive2 Part ITutorials at Rousseau Center +12h
13:30
90m
Tutorial
Reasoning About and Discovering LLVM Optimizations
Tutorials
John Regehr University of Utah, Nuno P. Lopes Universidade de Lisboa
13:30 - 15:10
Session 3Infer at Rousseau East +12h
Chair(s): Jules Villard Facebook London
13:30
40m
Talk
Finding Real Bugs in Big Programs with Incorrectness Logicvirtual
Infer
Quang Loc Le University College London, Azalea Raad Imperial College London, Jules Villard Facebook London, Josh Berdine Meta, Derek Dreyer MPI-SWS, Peter W. O'Hearn Meta; University College London
14:10
10m
Live Q&A
Q&A 4
Infer

14:20
40m
Talk
HIPPODROME: Data Race Repair using Static Analysis Summaries
Infer
Andreea Costea School of Computing, National University Of Singapore, Abhishek Tiwari National University of Singapore, Sigmund Chianasta , Kishore R , Abhik Roychoudhury National University of Singapore, Ilya Sergey National University of Singapore
15:00
10m
Live Q&A
Q&A 5
Infer

13:30 - 15:00
(Tutorial) JISET Part ITutorials at Rousseau West +12h
13:30
90m
Tutorial
Filling the gap between the JavaScript language specification and tools using the JISET family
Tutorials
Sukyoung Ryu KAIST, Jihyeok Park Oracle Labs, Australia, Seungmin An KAIST
15:30 - 17:00
EveningMAPS at Boardroom +12h
Chair(s): Swarat Chaudhuri University of Texas at Austin
15:30
45m
Keynote
Unsupervised Program Synthesis: Hierarchy and Perception
MAPS
Kevin Ellis Cornell University
16:15
15m
Talk
ExeBench: An ML-scale dataset of executable C functions
MAPS
Jordi Armengol-Estapé University of Edinburgh, Jackson Woodruff University of Edinburgh, Alexander Brauckmann University of Edinburgh, José Wesley de Souza Magalhães University of Edinburgh, Michael F. P. O'Boyle University of Edinburgh
16:30
15m
Talk
Automatically Debugging AutoML Pipelines Using Maro: ML Automated Remediation Oracle
MAPS
Julian Dolby IBM Research, USA, Jason Tsay IBM Research, Martin Hirzel IBM Research
16:45
15m
Talk
A Graph Neural Network-based performance model for Deep Learning Applications
MAPS
Shikhar Singh University of Texas, James Hegarty Facebook, Hugh Leather University of Edinburgh, UK, Benoit Steiner Facebook
15:30 - 17:00
Monday EveningCommute at Cockatoo
15:30
30m
Talk
Commutativity Reasoning in the Civl Verifier
Commute
Shaz Qadeer Novi, USA
16:00
10m
Live Q&A
Discussion
Commute

16:10
30m
Talk
Commutativity in quantum computing
Commute
Jens Palsberg University of California, Los Angeles (UCLA)
16:40
10m
Live Q&A
Discussion
Commute

16:50
5m
Talk
Lightning-2
Commute

15:30 - 17:00
TalkPLMW at Kon-Tiki +12h
15:30
90m
Talk
How to Write a Technical Paper
PLMW
Michael Hicks University of Maryland at College Park
15:30 - 16:30
(Tutorial) Alive2 Part IITutorials at Rousseau Center +12h
15:30
60m
Tutorial
Reasoning About and Discovering LLVM Optimizations
Tutorials
John Regehr University of Utah, Nuno P. Lopes Universidade de Lisboa
15:30 - 16:45
Session 4Infer at Rousseau East +12h
Chair(s): Jules Villard Facebook London
15:30
40m
Talk
Infer#’s journey to bring Infer to the .NET world
Infer
Xin Shi Microsoft Corporation, Xiaoyu Liu Microsoft Corporation, Matthew Jin Microsoft Corporation, Neel Sundaresan Microsoft Corporation
16:10
10m
Live Q&A
Q&A 6
Infer

16:20
20m
Talk
Infer in the cloud: An Overview of Infer Usage via Sonatype Lift
Infer
16:40
5m
Live Q&A
Q&A 7
Infer

15:30 - 16:30
(Tutorial) JISET Part IITutorials at Rousseau West +12h
15:30
60m
Tutorial
Filling the gap between the JavaScript language specification and tools using the JISET family
Tutorials
Sukyoung Ryu KAIST, Jihyeok Park Oracle Labs, Australia, Seungmin An KAIST
21:00 - 22:00
(Tutorial) Checked C Part ITutorials at Rousseau Center
21:00
60m
Tutorial
Making C Programs Safer with Checked C
Tutorials
Jie Zhou University of Rochester, Yudi Yang University of Rochester, USA, Michael Hicks University of Maryland at College Park, John Criswell University of Rochester, USA
21:00 - 22:00
(Tutorial) Discover[i] Part ITutorials at Rousseau West
21:00
60m
Tutorial
Discover[i]: Taming Unbounded Distributed Systems with Modular, Bounded Reasoning
Tutorials
Roopsha Samanta Purdue University, Nouraldin Jaber Purdue University, Christopher Wagner Purdue University
21:00 - 22:00
(Tutorial) Egg Part ITutorials at Toucan
21:00
60m
Tutorial
Build your own optimizer with egg!
Tutorials
Max Willsey University of Washington, Zachary Tatlock University of Washington
22:30 - 00:00
Array Languages for ApplicationsARRAY at Macaw
22:30
22m
Talk
Distributed parallel computing with Futhark
ARRAY
Michaël El Kharroubi University of Applied Sciences and Arts Western Switzerland, Baptiste Coudray , Orestis Malaspinas
22:52
22m
Talk
Mech: An Array Programming Language for Robots (extended abstract)
ARRAY
Corey Montella Lehigh University
23:15
22m
Talk
Probabilistic Array Programming on Galois Fields (extended abstract)
ARRAY
Breandan Considine McGill University, Jin L.C. Guo McGill University, Xujie Si McGill University, Canada
23:37
22m
Talk
Parallel Scan As a Multidimensional Array Problem
ARRAY
Artjoms Šinkarovs Heriot-Watt University, UK, Sven-Bodo Scholz Heriot-Watt University
22:30 - 00:00
(Tutorial) Checked C Part IITutorials at Rousseau Center
22:30
90m
Tutorial
Making C Programs Safer with Checked C
Tutorials
Jie Zhou University of Rochester, Yudi Yang University of Rochester, USA, Michael Hicks University of Maryland at College Park, John Criswell University of Rochester, USA
22:30 - 00:00
(Tutorial) Discover[i] Part IITutorials at Rousseau West
22:30
90m
Tutorial
Discover[i]: Taming Unbounded Distributed Systems with Modular, Bounded Reasoning
Tutorials
Roopsha Samanta Purdue University, Nouraldin Jaber Purdue University, Christopher Wagner Purdue University
22:30 - 00:00
(Tutorial) Egg Part IITutorials at Toucan
22:30
90m
Tutorial
Build your own optimizer with egg!
Tutorials
Max Willsey University of Washington, Zachary Tatlock University of Washington

Tue 14 Jun

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

01:30 - 03:00
AfternoonMAPS at Boardroom
01:30
45m
Keynote
Can Transformers Code?virtual
MAPS
02:15
15m
Talk
Syntax-Guided Program Reduction for Understanding Neural Code Intelligence Modelsvirtual
MAPS
Md Rafiqul Islam Rabin University of Houston, Aftab Hussain University of Houston, Amin Alipour University of Houston
DOI Pre-print
02:30
15m
Talk
A Systematic Evaluation of Large Language Models of Codevirtual
MAPS
Frank F. Xu Carnegie Mellon University, Uri Alon Carnegie Mellon University, Graham Neubig Carnegie Mellon University, Vincent J. Hellendoorn Carnegie Mellon University
02:45
15m
Poster
Poster Session
MAPS

01:30 - 03:00
TalkPLMW at Kon-Tiki
01:30
90m
Talk
Your Research and Everyone Else
PLMW
Martin C. Rinard Massachusetts Institute of Technology
01:30 - 03:00
(Tutorial) Alive2 Part ITutorials at Rousseau Center
01:30
90m
Tutorial
Reasoning About and Discovering LLVM Optimizations
Tutorials
John Regehr University of Utah, Nuno P. Lopes Universidade de Lisboa
01:30 - 03:10
Session 3Infer at Rousseau East
01:30
40m
Talk
Finding Real Bugs in Big Programs with Incorrectness Logicvirtual
Infer
Quang Loc Le University College London, Azalea Raad Imperial College London, Jules Villard Facebook London, Josh Berdine Meta, Derek Dreyer MPI-SWS, Peter W. O'Hearn Meta; University College London
02:10
10m
Live Q&A
Q&A 4
Infer

02:20
40m
Talk
HIPPODROME: Data Race Repair using Static Analysis Summaries
Infer
Andreea Costea School of Computing, National University Of Singapore, Abhishek Tiwari National University of Singapore, Sigmund Chianasta , Kishore R , Abhik Roychoudhury National University of Singapore, Ilya Sergey National University of Singapore
03:00
10m
Live Q&A
Q&A 5
Infer

01:30 - 03:00
(Tutorial) JISET Part ITutorials at Rousseau West
01:30
90m
Tutorial
Filling the gap between the JavaScript language specification and tools using the JISET family
Tutorials
Sukyoung Ryu KAIST, Jihyeok Park Oracle Labs, Australia, Seungmin An KAIST
03:30 - 05:00
EveningMAPS at Boardroom
03:30
45m
Keynote
Unsupervised Program Synthesis: Hierarchy and Perception
MAPS
Kevin Ellis Cornell University
04:15
15m
Talk
ExeBench: An ML-scale dataset of executable C functions
MAPS
Jordi Armengol-Estapé University of Edinburgh, Jackson Woodruff University of Edinburgh, Alexander Brauckmann University of Edinburgh, José Wesley de Souza Magalhães University of Edinburgh, Michael F. P. O'Boyle University of Edinburgh
04:30
15m
Talk
Automatically Debugging AutoML Pipelines Using Maro: ML Automated Remediation Oracle
MAPS
Julian Dolby IBM Research, USA, Jason Tsay IBM Research, Martin Hirzel IBM Research
04:45
15m
Talk
A Graph Neural Network-based performance model for Deep Learning Applications
MAPS
Shikhar Singh University of Texas, James Hegarty Facebook, Hugh Leather University of Edinburgh, UK, Benoit Steiner Facebook
03:30 - 05:00
TalkPLMW at Kon-Tiki
03:30
90m
Talk
How to Write a Technical Paper
PLMW
Michael Hicks University of Maryland at College Park
03:30 - 04:30
(Tutorial) Alive2 Part IITutorials at Rousseau Center
03:30
60m
Tutorial
Reasoning About and Discovering LLVM Optimizations
Tutorials
John Regehr University of Utah, Nuno P. Lopes Universidade de Lisboa
03:30 - 04:45
Session 4Infer at Rousseau East
03:30
40m
Talk
Infer#’s journey to bring Infer to the .NET world
Infer
Xin Shi Microsoft Corporation, Xiaoyu Liu Microsoft Corporation, Matthew Jin Microsoft Corporation, Neel Sundaresan Microsoft Corporation
04:10
10m
Live Q&A
Q&A 6
Infer

04:20
20m
Talk
Infer in the cloud: An Overview of Infer Usage via Sonatype Lift
Infer
04:40
5m
Live Q&A
Q&A 7
Infer

03:30 - 04:30
(Tutorial) JISET Part IITutorials at Rousseau West
03:30
60m
Tutorial
Filling the gap between the JavaScript language specification and tools using the JISET family
Tutorials
Sukyoung Ryu KAIST, Jihyeok Park Oracle Labs, Australia, Seungmin An KAIST
09:00 - 10:00
Keynote 1SOAP at Boardroom +12h
Chair(s): Laura Titolo NIA/NASA LaRC
09:00
60m
Keynote
Program Analysis for the Optimization and Verification of (Ethereum) Smart Contracts
SOAP
K: Elvira Albert Complutense University of Madrid
09:00 - 10:00
TalkPLMW at Kon-Tiki +12h
09:00
60m
Talk
A Research Mindset
PLMW
09:00 - 10:00
KeynoteLCTES at Rousseau Center +12h
Chair(s): Tobias Grosser University of Edinburgh
09:00
60m
Keynote
Domain-specific programming methodologies for domain-specific and emerging computing systems
LCTES
Jeronimo Castrillon TU Dresden, Germany
09:00 - 10:00
OpeningEGRAPHS at Toucan +12h
Chair(s): Max Willsey University of Washington
09:00
5m
Day opening
Welcome
EGRAPHS
Max Willsey University of Washington
09:05
30m
Talk
Sketch-Guided Equality Saturation
EGRAPHS
Thomas Koehler University of Glasgow
Pre-print File Attached
09:35
25m
Talk
Synthesizing Mathematical Identities with E-graphs
EGRAPHS
Ian Briggs University of Utah, Pavel Panchekha University of Utah
Link to publication Pre-print
10:00 - 10:30
PLTea (Tue AM)PLMW at Kon-Tiki Foyer
Chair(s): Rachit Nigam Cornell University
10:00
30m
Social Event
PLTeasocial
PLMW

10:00 - 12:00
Welcome and Session AISMM at Rousseau East +12h
Chair(s): Martin Maas Google Research
10:15
15m
Day opening
Welcome from the Chairs and Conference Reportvirtual
ISMM
David Chisnall Microsoft Research, Michael Lippautz Google
10:30
60m
Panel
Industry panel: Memory management priorities for the next few yearsvirtual
ISMM
11:30
30m
Talk
Reconsidering OS Memory Optimizations in the Presence of Disaggregated Memoryvirtual
ISMM
Shai Bergman Technion, Priyank Faldu ARM, Boris Grot University of Edinburgh, UK, Lluís Vilanova Imperial College London, Mark Silberstein Technion
10:30 - 12:00
Paper Session 1 SOAP at Boardroom +12h
Chair(s): Caterina Urban Inria & École Normale Supérieure | Université PSL

All papers will be allocated a time slot of 25 min (20min talk + 5 min questions)

10:30
25m
Talk
Abstract interpretation of Michelson smart-contracts
SOAP
P: Guillaume Bau , Antoine Miné Sorbonne Université, Vincent Botbol Nomadic Labs, Mehdi Bouaziz Nomadic Labs Paris
10:55
25m
Talk
BinFPE: Accurate Floating-Point Exception Detection for GPU Applications
SOAP
P: Ignacio Laguna Lawrence Livermore National Laboratory, Xinyi Li University of Utah, Ganesh Gopalakrishnan University of Utah
11:20
25m
Talk
Towards an Implementation of Differential Dynamic Logic in PVSvirtual
SOAP
P: J Tanner Slagel , César Muñoz NASA Langley Research Center, Swee Balachandran National Institute of Aerospace, Mariano Moscato National Institute of Aerospace, Aaron Dutle NASA Langley Research Center, Paolo Masci National Institute of Aerospace, USA, Lauren White NASA Langley Research Center
11:45
25m
Talk
Statically Detecting Data Leakages in Data Science Codevirtual
SOAP
Pavle Subotic Microsoft Azure, Uros Bojanic Microsoft, Milan Stojic Microsoft
10:30 - 12:00
Tuesday MorningCommute at Cockatoo
10:30
30m
Talk
Safety Proof Simplification Through Commutativity
Commute
Azadeh Farzan University of Toronto
11:00
10m
Live Q&A
Discussion
Commute

11:10
30m
Talk
Commutativity and Approximate Computing
Commute
Martin C. Rinard Massachusetts Institute of Technology
11:40
10m
Live Q&A
Discussion
Commute

11:50
5m
Talk
Lightning: Extending Commutativity via Safe Abstraction
Commute
Dominik Klumpp University of Freiburg
File Attached
10:30 - 12:00
PanelPLMW at Kon-Tiki +12h
10:30
90m
Panel
Mentoring Panel: Post-graduate Career Paths
PLMW
Michael Greenberg Stevens Institute of Technology, Chris Hawblitzel Microsoft Research, Hila Peleg Technion, Sukyoung Ryu KAIST, S: Deian Stefan University of California at San Diego
10:30 - 12:00
Optimization for Compilers and LanguagesLCTES at Rousseau Center +12h
Chair(s): Yousun Ko Yonsei University
10:30
20m
Talk
RollBin: Reducing code-size via loop rerolling at binary levelVirtual
LCTES
Tianao Ge Sun Yat-sen University, Zewei Mo Sun Yat-sen University, Kan Wu Sun Yat-sen University, Xianwei Zhang Sun Yat-sen University, Yutong Lu Sun Yat-sen University
10:50
20m
Talk
Tighten Rust's Belt: Shrinking Embedded Rust Binaries
LCTES
Hudson Ayers Stanford University, Google, Evan Laufer Stanford University, Paul Mure Stanford University, Jaehyeon Park Stanford University, Eduardo Rodelo Stanford University, Thea Rossman Stanford University, Andrey Pronin Google, Philip Levis Stanford University, Johnathan Van Why Google
11:10
20m
Talk
JAX Based Parallel Inference for Reactive Probabilistic Programming
LCTES
Guillaume Baudart IBM Research, USA, Louis Mandel IBM Research, USA, Reyyan Tekin
11:30
20m
Talk
Implicit State MachinesVirtual
LCTES
Fengyun Liu Oracle Labs, Aleksandar Prokopec Oracle Labs
11:50
5m
Talk
(WIP) Scalable Size Inliner for Mobile Applications
LCTES
10:30 - 12:00
Thinking AlikeEGRAPHS at Toucan +12h
Chair(s): Max Willsey University of Washington
10:30
15m
Talk
Logging an Egg: Datalog on E-Graphs
EGRAPHS
Philip Zucker Draper Laboratory
Pre-print Media Attached
10:45
15m
Talk
Chasing an egg
EGRAPHS
Yihong Zhang University of Washington
Pre-print
11:00
15m
Talk
ECTAs: E-Graphs Better (at Encoding)
EGRAPHS
James Koppel Massachusetts Institute of Technology, USA, Zheng Guo University of California, San Diego, Edsko de Vries Well-Typed LLP, Armando Solar-Lezama Massachusetts Institute of Technology, Nadia Polikarpova University of California at San Diego
11:15
15m
Talk
E-Graphs, VSAs, and Tree Automata: a Rosetta StoneVirtual
EGRAPHS
Yisu Remy Wang University of Washington, James Koppel Massachusetts Institute of Technology, USA, Altan Haan OctoML, Josh Pollock MIT CSAIL
Link to publication Pre-print
11:30
15m
Talk
Equality Saturation as a Tactic for Proof Assistants
EGRAPHS
Andrés Goens the University of Edinburgh, Siddharth Bhat the University of Edinburgh
11:45
15m
Talk
Towards Optimising Certified Programs by Proof Rewriting
EGRAPHS
Kiran Gopinathan National University of Singapore, Ilya Sergey National University of Singapore
12:00 - 13:00
Tuesday LunchPLDI at Beach North
12:00
60m
Lunch
Lunchsocial
PLDI

12:00 - 14:00
LunchISMM at Rousseau East +12h
12:00
2h
Lunch
Lunchsocial
ISMM

13:30 - 15:00
Keynote 2 + PapersSOAP at Boardroom +12h
Chair(s): Laure Gonnord Univ. Grenoble Alpes, Grenoble INP, LCIS, Valence, France, Laura Titolo NIA/NASA LaRC
13:30
60m
Keynote
Static Analysis for Data Scientists
SOAP
K: Caterina Urban Inria & École Normale Supérieure | Université PSL
14:30
25m
Talk
Ensuring Determinism in Blockchain Software with GoLiSA: An Industrial Experience Report
SOAP
P: Luca Olivieri University of Verona, Corvallis S.r.l., Fabio Tagliaferro University of Verona, Commercio.network S.p.A., Vincenzo Arceri University of Parma, Italy, Marco Ruaro Commercio.network S.p.A., Luca Negrini Ca’ Foscari University of Venice, Corvallis S.r.l., Agostino Cortesi Università Ca' Foscari Venezia, Pietro Ferrara Università Ca' Foscari, Venezia, Italy, Fausto Spoto U. Verona, Enrico Talin Commercio.network S.p.A.
13:30 - 15:00
Tuesday AfternoonCommute at Cockatoo
13:30
30m
Talk
Weakening Mazurkiewicz Traces
Commute
Umang Mathur National University of Singapore
14:00
10m
Live Q&A
Discussion
Commute

14:10
30m
Talk
Mergeable Replicated Datatypes
Commute
Suresh Jagannathan Purdue University
14:40
10m
Live Q&A
Discussion
Commute

14:50
5m
Talk
Lightning-4
Commute

13:30 - 15:00
TalkPLMW at Kon-Tiki +12h
13:30
90m
Talk
Whose Life Are You Making Better
PLMW
John Regehr University of Utah
13:30 - 15:00
Be aware of HardwareLCTES at Rousseau Center +12h
Chair(s): Kyoungwoo Lee Yonsei University
13:30
20m
Talk
Optimizing Data Reshaping Operations in Functional IRs for High-Level Synthesis
LCTES
Christof Schlaak University of Edinburgh, Tzung-Han Juang McGill University, Christophe Dubach McGill University
13:50
20m
Talk
Co-Mining: A Processing-in-Memory Assisted Framework for Memory-Intensive PoW AccelerationVirtual
LCTES
Tianyu Wang The Chinese University of Hong Kong, Zhaoyan Shen Shandong University, Zili Shao The Chinese University of Hong Kong
14:10
20m
Talk
ISKEVA: In-SSD Key-Value Database Engine for Video Analytics ApplicationsVirtual
LCTES
Yi Zheng The Pennsylvania State University, Joshua Fixelle University of Virginia, ‪Nagadastagiri Challapalle‬ The Pennsylvania State University, Pingyi Huo The Pennsylvania State University, Vijaykrishnan Narayanan The Pennsylvania State University, Zili Shao The Chinese University of Hong Kong, Mircea R. Stan University of Virginia, Zhaoyan Shen Shandong University
14:30
20m
Talk
An Old Friend Is Better Than Two New Ones: Dual-Screen AndroidVirtual
LCTES
Zizhan Chen The Chinese University of Hong Kong, Siqi Shang The Chinese University of Hong Kong, Qihong Wu The Chinese University of Hong Kong, Jin Xue The Chinese University of Hong Kong, Zhaoyan Shen Shandong University, Zili Shao The Chinese University of Hong Kong
14:50
5m
Talk
(WIP) Cache-Coherent CLAMVirtual
LCTES
Chen Ding University of Rochester, Benjamin Reber University of Rochester, Dorin Patru Rochester Institute of Technology
14:00 - 16:00
Session BISMM at Rousseau East +12h
Chair(s): Chen Ding University of Rochester
14:00
30m
Talk
MemSweeper: Virtualizing Cluster Memory Management for High Memory Utilization and Isolationvirtual
ISMM
AmirHossein Seyri University of Illinois at Chicago, Abhisek Pan Microsoft, Balajee Vamanan University of Illinois at Chicago
14:30
30m
Talk
Replication-based Object Persistence by Reachabilityvirtual
ISMM
Kotaro Matsumoto Kochi University of Technology, Tomoharu Ugawa University of Tokyo, Hideya Iwasaki University of Electro-Communications, Japan
15:00
30m
Talk
Concurrent and Parallel Garbage Collection for Lightweight Threads on Multicore Processorsvirtual
ISMM
Katsuhiro Ueno Niigata University, Atsushi Ohori Tohoku University, Japan
15:30
30m
Break
Social breaksocial
ISMM

14:00 - 15:00
ApplicationsEGRAPHS at Toucan +12h
Chair(s): Chandrakana Nandi Certora, inc.
14:00
15m
Talk
Quiche: A Python Implementation of E-Graphs
EGRAPHS
Rebecca Swords Unaffiliated
14:15
15m
Talk
Optimizing Large Integer Multiplier on FPGAs Using Equality SaturationVirtual
EGRAPHS
Ecenur Ustun Cornell University, Jiaqi Yin University of Utah, Zhiru Zhang Cornell University, USA
14:30
15m
Talk
Wasm-mutate: Fuzzing WebAssembly Compilers with E-GraphsVirtual
EGRAPHS
Javier Cabrera Arteaga KTH Royal Institute of Technology, Nicholas Fitzgerald Fastly Inc., Martin Monperrus KTH Royal Institute of Technology, Benoit Baudry KTH
Pre-print
14:45
15m
Talk
QuEgg: Automatic Optimization of Quantum Circuits Using Equality Graphs
EGRAPHS
Spencer King Unaffiliated
15:30 - 17:20
Keynote 3 + PapersSOAP at Boardroom +12h
Chair(s): Roberto Giacobazzi University of Verona, Laura Titolo NIA/NASA LaRC

Laura Titolo is chairing the Keynote Talk by Francesco Logozzo. Roberto Giacobazzi is chairing the paper session from 16:30 to 17:20.

15:30
60m
Keynote
Using static analysis to scale security at Meta
SOAP
K: Francesco Logozzo Facebook
16:30
25m
Talk
ADA: A Tool for Visualizing The Architectural Overview of Open-Source Repositories
SOAP
P: Md Rakib Hossain Misu University of California, Irvine, Aleksandar Saša Janjanin University College London, Zhiqiang Bian University College London, Valentin-Sebastian Burlacu University College London, Naum Anteski University College London
16:55
25m
Talk
Modeling Code Manipulation in JIT Compilers
SOAP
P: HeuiChan Lim University of Arizona, Xiyu Kang University of Arizona, Saumya Debray University of Arizona
15:30 - 17:00
Tuesday EveningCommute at Cockatoo
15:30
30m
Talk
Testing Distributed Protocols using Communication Closure
Commute
Constantin Enea Ecole Polytechnique / LIX / CNRS
16:00
10m
Live Q&A
Discussion
Commute

16:10
30m
Talk
Pretend synchrony: synchronous verification of asynchronous distributed programs
Commute
Klaus v. Gleissenthall Vrije Universiteit Amsterdam, Netherlands
16:40
10m
Live Q&A
Discussion
Commute

16:50
10m
Day closing
Closing Remarks & Business Meeting
Commute
Eric Koskinen Stevens Institute of Technology, Azadeh Farzan University of Toronto, Constantin Enea Ecole Polytechnique / LIX / CNRS
15:30 - 17:00
PanelPLMW at Kon-Tiki +12h
15:30
90m
Panel
Mentoring Panel: Hot Topics in PL
PLMW
Michael Carbin Massachusetts Institute of Technology, Andrew Myers Cornell University, Nadia Polikarpova University of California at San Diego, S: Limin Jia Carnegie Mellon University, Nikhil Swamy Microsoft Research
15:30 - 17:00
Complementary ApproachesASA at Macaw +12h
15:30
45m
Talk
Automated Software Testing: Bridging The Gap With Deep Learningvirtual
ASA
Elizabeth Dinella University of Pennsylvania
16:15
45m
Talk
Precise Program Reasoning using Probabilistic Methods
ASA
Mukund Raghothaman University of Southern California
15:30 - 17:00
How to Analyze and Utilize LCTES at Rousseau Center +12h
Chair(s): Guillaume Baudart IBM Research, USA
15:30
20m
Talk
Code Generation Criteria for Buffered Exposed Datapath Architectures from Dataflow GraphsVirtual
LCTES
Klaus Schneider University of Kaiserslautern, Anoop Bhagyanath University of Kaiserslautern, Julius Roob University of Kaiserslautern
Pre-print
15:50
20m
Talk
Trace-and-Brace (TAB): Bespoke Software Countermeasures against Soft Errors
LCTES
Yousun Ko Yonsei University, Alex Bradbury lowRISC C.I.C., Bernd Burgstaller Yonsei University, Robert Mullins University of Cambridge
16:10
20m
Talk
Automated Kernel Fusion for GPU Based on Code Motion
LCTES
Junji Fukuhara Tokyo University of Science, Munehiro Takimoto Tokyo University of Science
16:30
20m
Talk
TCPS: A Task and Cache-aware Partitioned Scheduler for Hard Real-time Multi-core SystemsVirtual
LCTES
Yixian Shen University of Amsterdam, Jun Xiao University of Amsterdam, Andy Pimentel University of Amsterdam
16:50
5m
Talk
(WIP) A Memory Interference Analysis using a Formal Timing Analyzer
LCTES
Mihail Asavoae Univ. Paris-Saclay, CEA List, Oumaima Matoussi Univ. Paris-Saclay, CEA List, Asmae Bouachtala Univ. Paris-Saclay, CEA List, Hai-Dang Vu Univ. Paris-Saclay, CEA List, Mathieu Jan Univ. Paris-Saclay, CEA List
15:30 - 16:30
ExtensionsEGRAPHS at Toucan +12h
Chair(s): Zachary Tatlock University of Washington
15:30
15m
Talk
On the Optimization of Equivalent Concurrent ComputationsVirtual
EGRAPHS
Henrich Lauko Trail of Bits, Lukáš Korenčik Trail of Bits, Peter Goodman Trail of Bits
15:45
15m
Talk
Abstract Interpretation on E-Graphs
EGRAPHS
Samuel Coward Imperial College London, UK, George A. Constantinides Imperial College London, UK, Theo Drane Intel Corporation, USA
Pre-print
16:00
15m
Talk
Colored E-Graph: Supporting Multiple Equivalence Relations with Resource SharingVirtual
EGRAPHS
Eytan Singher Technion - Israel Institute of Technology, Shachar Itzhaky Technion
16:15
15m
Talk
Toward a Unified Framework for Program Optimization, Bug-Finding, and Repair
EGRAPHS
Jordan Schmerge Colorado School of Mines, Jake Vossen Colorado School of Mines, Jedidiah McClurg Colorado School of Mines
16:00 - 17:30
Keynote and ClosingISMM at Rousseau East +12h
Chair(s): Michael Lippautz Google
16:00
60m
Keynote
We Live in Interesting Timesvirtual
ISMM
Steve Blackburn Google and Australian National University
17:00
15m
Day closing
Closing Remarksvirtual
ISMM
David Chisnall Microsoft Research, Michael Lippautz Google
21:00 - 22:00
Keynote 1SOAP at Boardroom
21:00
60m
Keynote
Program Analysis for the Optimization and Verification of (Ethereum) Smart Contracts
SOAP
K: Elvira Albert Complutense University of Madrid
21:00 - 22:00
TalkPLMW at Kon-Tiki
21:00
60m
Talk
A Research Mindset
PLMW
21:00 - 22:00
KeynoteLCTES at Rousseau Center
Chair(s): Tobias Grosser University of Edinburgh
21:00
60m
Keynote
Domain-specific programming methodologies for domain-specific and emerging computing systems
LCTES
Jeronimo Castrillon TU Dresden, Germany
21:00 - 22:00
OpeningEGRAPHS at Toucan
21:00
5m
Day opening
Welcome
EGRAPHS
Max Willsey University of Washington
21:05
30m
Talk
Sketch-Guided Equality Saturation
EGRAPHS
Thomas Koehler University of Glasgow
Pre-print File Attached
21:35
25m
Talk
Synthesizing Mathematical Identities with E-graphs
EGRAPHS
Ian Briggs University of Utah, Pavel Panchekha University of Utah
Link to publication Pre-print
22:30 - 00:00
Paper Session 1 SOAP at Boardroom
22:30
25m
Talk
Abstract interpretation of Michelson smart-contracts
SOAP
P: Guillaume Bau , Antoine Miné Sorbonne Université, Vincent Botbol Nomadic Labs, Mehdi Bouaziz Nomadic Labs Paris
22:55
25m
Talk
BinFPE: Accurate Floating-Point Exception Detection for GPU Applications
SOAP
P: Ignacio Laguna Lawrence Livermore National Laboratory, Xinyi Li University of Utah, Ganesh Gopalakrishnan University of Utah
23:20
25m
Talk
Towards an Implementation of Differential Dynamic Logic in PVSvirtual
SOAP
P: J Tanner Slagel , César Muñoz NASA Langley Research Center, Swee Balachandran National Institute of Aerospace, Mariano Moscato National Institute of Aerospace, Aaron Dutle NASA Langley Research Center, Paolo Masci National Institute of Aerospace, USA, Lauren White NASA Langley Research Center
23:45
25m
Talk
Statically Detecting Data Leakages in Data Science Codevirtual
SOAP
Pavle Subotic Microsoft Azure, Uros Bojanic Microsoft, Milan Stojic Microsoft
22:30 - 00:00
PanelPLMW at Kon-Tiki
22:30
90m
Panel
Mentoring Panel: Post-graduate Career Paths
PLMW
Michael Greenberg Stevens Institute of Technology, Chris Hawblitzel Microsoft Research, Hila Peleg Technion, Sukyoung Ryu KAIST, S: Deian Stefan University of California at San Diego
22:30 - 00:00
Optimization for Compilers and LanguagesLCTES at Rousseau Center
Chair(s): Yousun Ko Yonsei University
22:30
20m
Talk
RollBin: Reducing code-size via loop rerolling at binary levelVirtual
LCTES
Tianao Ge Sun Yat-sen University, Zewei Mo Sun Yat-sen University, Kan Wu Sun Yat-sen University, Xianwei Zhang Sun Yat-sen University, Yutong Lu Sun Yat-sen University
22:50
20m
Talk
Tighten Rust's Belt: Shrinking Embedded Rust Binaries
LCTES
Hudson Ayers Stanford University, Google, Evan Laufer Stanford University, Paul Mure Stanford University, Jaehyeon Park Stanford University, Eduardo Rodelo Stanford University, Thea Rossman Stanford University, Andrey Pronin Google, Philip Levis Stanford University, Johnathan Van Why Google
23:10
20m
Talk
JAX Based Parallel Inference for Reactive Probabilistic Programming
LCTES
Guillaume Baudart IBM Research, USA, Louis Mandel IBM Research, USA, Reyyan Tekin
23:30
20m
Talk
Implicit State MachinesVirtual
LCTES
Fengyun Liu Oracle Labs, Aleksandar Prokopec Oracle Labs
23:50
5m
Talk
(WIP) Scalable Size Inliner for Mobile Applications
LCTES
22:30 - 00:00
Thinking AlikeEGRAPHS at Toucan
22:30
15m
Talk
Logging an Egg: Datalog on E-Graphs
EGRAPHS
Philip Zucker Draper Laboratory
Pre-print Media Attached
22:45
15m
Talk
Chasing an egg
EGRAPHS
Yihong Zhang University of Washington
Pre-print
23:00
15m
Talk
ECTAs: E-Graphs Better (at Encoding)
EGRAPHS
James Koppel Massachusetts Institute of Technology, USA, Zheng Guo University of California, San Diego, Edsko de Vries Well-Typed LLP, Armando Solar-Lezama Massachusetts Institute of Technology, Nadia Polikarpova University of California at San Diego
23:15
15m
Talk
E-Graphs, VSAs, and Tree Automata: a Rosetta StoneVirtual
EGRAPHS
Yisu Remy Wang University of Washington, James Koppel Massachusetts Institute of Technology, USA, Altan Haan OctoML, Josh Pollock MIT CSAIL
Link to publication Pre-print
23:30
15m
Talk
Equality Saturation as a Tactic for Proof Assistants
EGRAPHS
Andrés Goens the University of Edinburgh, Siddharth Bhat the University of Edinburgh
23:45
15m
Talk
Towards Optimising Certified Programs by Proof Rewriting
EGRAPHS
Kiran Gopinathan National University of Singapore, Ilya Sergey National University of Singapore

Wed 15 Jun

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

00:00 - 02:00
00:00
2h
Lunch
Lunchsocial
ISMM

01:30 - 03:00
Keynote 2 + PapersSOAP at Boardroom
Chair(s): Laure Gonnord Univ. Grenoble Alpes, Grenoble INP, LCIS, Valence, France, Laura Titolo NIA/NASA LaRC
01:30
60m
Keynote
Static Analysis for Data Scientists
SOAP
K: Caterina Urban Inria & École Normale Supérieure | Université PSL
02:30
25m
Talk
Ensuring Determinism in Blockchain Software with GoLiSA: An Industrial Experience Report
SOAP
P: Luca Olivieri University of Verona, Corvallis S.r.l., Fabio Tagliaferro University of Verona, Commercio.network S.p.A., Vincenzo Arceri University of Parma, Italy, Marco Ruaro Commercio.network S.p.A., Luca Negrini Ca’ Foscari University of Venice, Corvallis S.r.l., Agostino Cortesi Università Ca' Foscari Venezia, Pietro Ferrara Università Ca' Foscari, Venezia, Italy, Fausto Spoto U. Verona, Enrico Talin Commercio.network S.p.A.
01:30 - 03:00
TalkPLMW at Kon-Tiki
01:30
90m
Talk
Whose Life Are You Making Better
PLMW
John Regehr University of Utah
01:30 - 03:00
Be aware of HardwareLCTES at Rousseau Center
Chair(s): Kyoungwoo Lee Yonsei University
01:30
20m
Talk
Optimizing Data Reshaping Operations in Functional IRs for High-Level Synthesis
LCTES
Christof Schlaak University of Edinburgh, Tzung-Han Juang McGill University, Christophe Dubach McGill University
01:50
20m
Talk
Co-Mining: A Processing-in-Memory Assisted Framework for Memory-Intensive PoW AccelerationVirtual
LCTES
Tianyu Wang The Chinese University of Hong Kong, Zhaoyan Shen Shandong University, Zili Shao The Chinese University of Hong Kong
02:10
20m
Talk
ISKEVA: In-SSD Key-Value Database Engine for Video Analytics ApplicationsVirtual
LCTES
Yi Zheng The Pennsylvania State University, Joshua Fixelle University of Virginia, ‪Nagadastagiri Challapalle‬ The Pennsylvania State University, Pingyi Huo The Pennsylvania State University, Vijaykrishnan Narayanan The Pennsylvania State University, Zili Shao The Chinese University of Hong Kong, Mircea R. Stan University of Virginia, Zhaoyan Shen Shandong University
02:30
20m
Talk
An Old Friend Is Better Than Two New Ones: Dual-Screen AndroidVirtual
LCTES
Zizhan Chen The Chinese University of Hong Kong, Siqi Shang The Chinese University of Hong Kong, Qihong Wu The Chinese University of Hong Kong, Jin Xue The Chinese University of Hong Kong, Zhaoyan Shen Shandong University, Zili Shao The Chinese University of Hong Kong
02:50
5m
Talk
(WIP) Cache-Coherent CLAMVirtual
LCTES
Chen Ding University of Rochester, Benjamin Reber University of Rochester, Dorin Patru Rochester Institute of Technology
02:00 - 04:00
Session BISMM at Rousseau East
02:00
30m
Talk
MemSweeper: Virtualizing Cluster Memory Management for High Memory Utilization and Isolationvirtual
ISMM
AmirHossein Seyri University of Illinois at Chicago, Abhisek Pan Microsoft, Balajee Vamanan University of Illinois at Chicago
02:30
30m
Talk
Replication-based Object Persistence by Reachabilityvirtual
ISMM
Kotaro Matsumoto Kochi University of Technology, Tomoharu Ugawa University of Tokyo, Hideya Iwasaki University of Electro-Communications, Japan
03:00
30m
Talk
Concurrent and Parallel Garbage Collection for Lightweight Threads on Multicore Processorsvirtual
ISMM
Katsuhiro Ueno Niigata University, Atsushi Ohori Tohoku University, Japan
03:30
30m
Break
Social breaksocial
ISMM

02:00 - 03:00
ApplicationsEGRAPHS at Toucan
02:00
15m
Talk
Quiche: A Python Implementation of E-Graphs
EGRAPHS
Rebecca Swords Unaffiliated
02:15
15m
Talk
Optimizing Large Integer Multiplier on FPGAs Using Equality SaturationVirtual
EGRAPHS
Ecenur Ustun Cornell University, Jiaqi Yin University of Utah, Zhiru Zhang Cornell University, USA
02:30
15m
Talk
Wasm-mutate: Fuzzing WebAssembly Compilers with E-GraphsVirtual
EGRAPHS
Javier Cabrera Arteaga KTH Royal Institute of Technology, Nicholas Fitzgerald Fastly Inc., Martin Monperrus KTH Royal Institute of Technology, Benoit Baudry KTH
Pre-print
02:45
15m
Talk
QuEgg: Automatic Optimization of Quantum Circuits Using Equality Graphs
EGRAPHS
Spencer King Unaffiliated
03:30 - 05:20
Keynote 3 + PapersSOAP at Boardroom
Chair(s): Roberto Giacobazzi University of Verona, Laura Titolo NIA/NASA LaRC
03:30
60m
Keynote
Using static analysis to scale security at Meta
SOAP
K: Francesco Logozzo Facebook
04:30
25m
Talk
ADA: A Tool for Visualizing The Architectural Overview of Open-Source Repositories
SOAP
P: Md Rakib Hossain Misu University of California, Irvine, Aleksandar Saša Janjanin University College London, Zhiqiang Bian University College London, Valentin-Sebastian Burlacu University College London, Naum Anteski University College London
04:55
25m
Talk
Modeling Code Manipulation in JIT Compilers
SOAP
P: HeuiChan Lim University of Arizona, Xiyu Kang University of Arizona, Saumya Debray University of Arizona
03:30 - 05:00
PanelPLMW at Kon-Tiki
03:30
90m
Panel
Mentoring Panel: Hot Topics in PL
PLMW
Michael Carbin Massachusetts Institute of Technology, Andrew Myers Cornell University, Nadia Polikarpova University of California at San Diego, S: Limin Jia Carnegie Mellon University, Nikhil Swamy Microsoft Research
03:30 - 05:00
Complementary ApproachesASA at Macaw
03:30
45m
Talk
Automated Software Testing: Bridging The Gap With Deep Learningvirtual
ASA
Elizabeth Dinella University of Pennsylvania
04:15
45m
Talk
Precise Program Reasoning using Probabilistic Methods
ASA
Mukund Raghothaman University of Southern California
03:30 - 05:00
How to Analyze and Utilize LCTES at Rousseau Center
Chair(s): Guillaume Baudart IBM Research, USA
03:30
20m
Talk
Code Generation Criteria for Buffered Exposed Datapath Architectures from Dataflow GraphsVirtual
LCTES
Klaus Schneider University of Kaiserslautern, Anoop Bhagyanath University of Kaiserslautern, Julius Roob University of Kaiserslautern
Pre-print
03:50
20m
Talk
Trace-and-Brace (TAB): Bespoke Software Countermeasures against Soft Errors
LCTES
Yousun Ko Yonsei University, Alex Bradbury lowRISC C.I.C., Bernd Burgstaller Yonsei University, Robert Mullins University of Cambridge
04:10
20m
Talk
Automated Kernel Fusion for GPU Based on Code Motion
LCTES
Junji Fukuhara Tokyo University of Science, Munehiro Takimoto Tokyo University of Science
04:30
20m
Talk
TCPS: A Task and Cache-aware Partitioned Scheduler for Hard Real-time Multi-core SystemsVirtual
LCTES
Yixian Shen University of Amsterdam, Jun Xiao University of Amsterdam, Andy Pimentel University of Amsterdam
04:50
5m
Talk
(WIP) A Memory Interference Analysis using a Formal Timing Analyzer
LCTES
Mihail Asavoae Univ. Paris-Saclay, CEA List, Oumaima Matoussi Univ. Paris-Saclay, CEA List, Asmae Bouachtala Univ. Paris-Saclay, CEA List, Hai-Dang Vu Univ. Paris-Saclay, CEA List, Mathieu Jan Univ. Paris-Saclay, CEA List
03:30 - 04:30
ExtensionsEGRAPHS at Toucan
03:30
15m
Talk
On the Optimization of Equivalent Concurrent ComputationsVirtual
EGRAPHS
Henrich Lauko Trail of Bits, Lukáš Korenčik Trail of Bits, Peter Goodman Trail of Bits
03:45
15m
Talk
Abstract Interpretation on E-Graphs
EGRAPHS
Samuel Coward Imperial College London, UK, George A. Constantinides Imperial College London, UK, Theo Drane Intel Corporation, USA
Pre-print
04:00
15m
Talk
Colored E-Graph: Supporting Multiple Equivalence Relations with Resource SharingVirtual
EGRAPHS
Eytan Singher Technion - Israel Institute of Technology, Shachar Itzhaky Technion
04:15
15m
Talk
Toward a Unified Framework for Program Optimization, Bug-Finding, and Repair
EGRAPHS
Jordan Schmerge Colorado School of Mines, Jake Vossen Colorado School of Mines, Jedidiah McClurg Colorado School of Mines
04:00 - 05:30
Keynote and ClosingISMM at Rousseau East
04:00
60m
Keynote
We Live in Interesting Timesvirtual
ISMM
Steve Blackburn Google and Australian National University
05:00
15m
Day closing
Closing Remarksvirtual
ISMM
David Chisnall Microsoft Research, Michael Lippautz Google
09:00 - 10:10
Keynote: Emery BergerPLDI at Kon-Tiki +12h
Chair(s): Işıl Dillig University of Texas at Austin
09:00
10m
Other
Welcome to PLDI 2022
PLDI
Işıl Dillig University of Texas at Austin, Ranjit Jhala University of California at San Diego; Amazon Web Services
09:10
60m
Keynote
Getting Your Research Adopted
PLDI
Emery D. Berger University of Massachusetts Amherst
Pre-print Media Attached
10:00 - 10:30
PLTea Virtual (Wed 10am)PLDI at PLTea (Virtual see event for Zoom)
10:00
30m
Social Event
PL Teasocial
PLDI
Rachit Nigam Cornell University
10:10 - 10:40
PL Tea (Wed AM)PLDI at Boardroom
10:10
30m
Social Event
PL Teasocial
PLDI
Rachit Nigam Cornell University
10:40 - 12:00
Distributed SystemsSIGPLAN Track at Cockatoo
Chair(s): Adam Chlipala MIT CSAIL
10:40
20m
Talk
(ICFP 2020) TLC: Temporal Logic of Distributed Components
SIGPLAN Track
Jeremiah Griffin University of California, Riverside, Mohsen Lesani University of California at Riverside, Narges Shadab University of California at Riverside, Xizhe Yin University of California, Riverside
Link to publication DOI Authorizer link Pre-print
11:00
20m
Talk
(OOPSLA 2021) Durable functions: semantics for stateful serverless
SIGPLAN Track
Sebastian Burckhardt Microsoft Research, Chris Gillum Microsoft Azure, David Justo Microsoft Azure, Konstantinos Kallas University of Pennsylvania, Connor McMahon Microsoft Azure, Christopher Meiklejohn Carnegie Mellon University
Link to publication DOI Authorizer link Pre-print
11:20
20m
Talk
(OOPSLA 2021) ECROs: building global scale systems from sequential code
SIGPLAN Track
Kevin De Porre Vrije Universiteit Brussel, Carla Ferreira NOVA School of Science and Technology, Nuno Preguica , Elisa Gonzalez Boix Vrije Universiteit Brussel, Belgium
Link to publication DOI Authorizer link Pre-print
11:40
20m
Talk
(POPL 2022) Induction Duality: Primal-Dual Search for Invariants
SIGPLAN Track
Oded Padon VMware Research, James R. Wilcox Certora, Jason R. Koenig Stanford University, Kenneth L. McMillan University of Texas at Austin, Alex Aiken Stanford Univeristy
10:40 - 12:00
SecurityPLDI at Kon-Tiki +12h
Chair(s): Yu Feng University of California, Santa Barbara
10:40
20m
Talk
P4BID: Information Flow Control in P4
PLDI
Karuna Grewal , Loris D'Antoni University of Wisconsin-Madison, USA, Justin Hsu Cornell University
DOI
11:00
20m
Talk
ANOSY: Approximated Knowledge Synthesis with Refinement Types for Declassification
PLDI
Sankha Narayan Guria University of Maryland, College Park, Niki Vazou IMDEA Software Institute, Marco Guarnieri IMDEA Software Institute, James Parker Galois, Inc.
DOI Pre-print
11:20
20m
Talk
Hardening Attack Surfaces with Formally Proven Binary Format Parsers
PLDI
Nikhil Swamy Microsoft Research, Tahina Ramananandro Microsoft Research, Aseem Rastogi Microsoft Research, Irina Spiridonova Microsoft Research, Haobin Ni Cornell University, Dmitry Malloy Microsoft, Juan Vazquez Microsoft, Michael Tang Microsoft, Omar Cardona Microsoft, Arti Gupta Microsoft
DOI
11:40
20m
Talk
Modular Information Flow Through Ownership
PLDI
Will Crichton Stanford University, Marco Patrignani University of Trento, Maneesh Agrawala Stanford University, Pat Hanrahan Stanford University, USA
DOI Pre-print
10:40 - 12:00
Program AnalysisSIGPLAN Track at Macaw
Chair(s): Qirun Zhang Georgia Institute of Technology, USA
10:40
20m
Talk
(OOPSLA 2020) Perfectly Parallel Fairness Certification of Neural Networks
SIGPLAN Track
Caterina Urban Inria & École Normale Supérieure | Université PSL, Maria Christakis MPI-SWS, Valentin Wüstholz ConsenSys, Fuyuan Zhang MPI-SWS
11:00
20m
Talk
(PLDI 2020) OOElala : Order-Of-Evaluation based Alias Analysis for compiler optimization
SIGPLAN Track
Ankush Phulia IIT Delhi, India, Vaibhav Bhagee IIT Delhi, India, Sorav Bansal IIT Delhi and CompilerAI Labs
11:20
20m
Talk
(POPL 2021) Simplifying Dependent Reductions with the Polyhedral Model
SIGPLAN Track
Cambridge Yang MIT CSAIL, Eric Atkinson MIT CSAIL, Michael Carbin Massachusetts Institute of Technology
11:40
20m
Talk
(POPL 2021) The Fine-Grained and Parallel Complexity of Andersen's Pointer Analysis
SIGPLAN Track
Andreas Pavlogiannis Aarhus University, Anders Alnor Mathiasen Aarhus University
10:40 - 12:00
MemoryPLDI at Toucan +12h
Chair(s): Clément Pit-Claudel EPFL, AWS
10:40
20m
Talk
Is it Time to Retire Manual Concurrent Memory Reclamation?
PLDI
Daniel Anderson Carnegie Mellon University, Guy E. Blelloch Carnegie Mellon University, Yuanhao Wei Carnegie Mellon University, USA
11:00
20m
Talk
Low-Latency, High-Throughput Garbage CollectionDistinguished Paper Award
PLDI
Wenyu Zhao Australian National University, Steve Blackburn Google and Australian National University, Kathryn S McKinley Google
DOI
11:20
20m
Talk
Mako: A Low-Pause, High-Throughput Evacuating Collector for Memory-Disaggregated Datacenters
PLDI
Haoran Ma University of California, Los Angeles, Shi Liu UCLA, Chenxi Wang UCLA, Yifan Qiao UCLA, Michael D. Bond Ohio State University, Steve Blackburn Google and Australian National University, Miryung Kim University of California at Los Angeles, USA, Guoqing Harry Xu University of California at Los Angeles
DOI
11:40
20m
Talk
PaC-trees: Supporting Parallel and Compressed Purely-Functional Collections
PLDI
Laxman Dhulipala Carnegie Mellon University, Guy E. Blelloch Carnegie Mellon University, Yan Gu UC Riverside, Yihan Sun University of California, Riverside
DOI
12:00 - 13:00
Wednesday Lunch & SIGPLAN AwardsPLDI at Beach North
12:00
60m
Lunch
Lunchsocial
PLDI

13:30 - 14:50
Domain Specific LanguagesSIGPLAN Track at Cockatoo
Chair(s): Zachary Tatlock University of Washington
13:30
20m
Talk
(POPL 2021) Petr4: Formal Foundations for P4 Data Planes
SIGPLAN Track
Ryan Doenges Cornell University, Mina Tahmasbi Arashloo Cornell University, Santiago Bautista Univ Rennes, ENS Rennes, Inria, IRISA, Alexander Chang Cornell University, Newton Ni Cornell University, Samwise Parkinson Cornell University, Rudy Peterson Cornell University, Alaia Solko-Breslin Cornell University, Amanda Xu Cornell University, Nate Foster Cornell University
13:50
20m
Talk
(PLDI 2020) Predictable Accelerator Design with Time-Sensitive Affine Types
SIGPLAN Track
Rachit Nigam Cornell University, Sachille Atapattu Cornell University, USA, Samuel Thomas Cornell University, USA, Theodore Bauer AWS Inc, Apurva Koti Cornell University, USA, Zhijing Li Cornell University, USA, Yuwei Ye Cornell University, USA, Adrian Sampson Cornell University, Zhiru Zhang Cornell University, USA
14:10
20m
Talk
(POPL 2022) Dependently-Typed Data Plane Programming
SIGPLAN Track
Matthias Eichholz Technical University of Darmstadt, Eric Campbell Cornell University, Matthias Krebs TU Darmstadt, Nate Foster Cornell University, Mira Mezini TU Darmstadt
14:30
20m
Talk
(POPL 2022) Safe, Modular Packet Pipeline Programming
SIGPLAN Track
Devon Loehr Princeton University, David Walker Princeton University
13:30 - 14:50
Synthesis I PLDI at Kon-Tiki +12h
Chair(s): Ruben Martins Carnegie Mellon University
13:30
20m
Talk
WebRobot: Web Robotic Process Automation using Interactive Programming-by-Demonstration
PLDI
Rui Dong University of Michigan, Zhicheng Huang University of Michigan, Ian Iong Lam University of Michigan, Yan Chen University of Michigan, Xinyu Wang University of Michigan
DOI Pre-print
13:50
20m
Talk
Synthesizing Analytical SQL Queries from Computation DemonstrationDistinguished Paper Award
PLDI
Xiangyu Zhou University of Washington, Rastislav Bodík University of Washington, Alvin Cheung University of California, Berkeley, Chenglong Wang University of Washington, USA
DOI
14:10
20m
Talk
Type-Directed Program Synthesis for RESTful APIs
PLDI
Zheng Guo University of California, San Diego, David Cao University of California, San Diego, Davin Tjong University of California, San Diego, Jean Yang Akita Software, Cole Schlesinger Akita Software, Nadia Polikarpova University of California at San Diego
DOI
14:30
20m
Talk
Visualization Question Answering Using Introspective Program SynthesisDistinguished Paper Award
PLDI
Yanju Chen University of California, Santa Barbara, Xifeng Yan University of California, Santa Barbara, Yu Feng University of California, Santa Barbara
DOI
13:30 - 14:50
Secure SpeculationSIGPLAN Track at Macaw
Chair(s): Marco Patrignani University of Trento
13:30
20m
Talk
(OOPSLA 2021) Reconciling Optimization with Secure Compilation
SIGPLAN Track
Son Tuan Vu Sorbonne Université, CNRS, Laboratoire d'Informatique de Paris 6, LIP6, Albert Cohen Google, Arnaud de Grandmaison , Christophe Guillon STMicroelectronics, Karine Heydemann Sorbonne University; CNRS; LIP6
Link to publication DOI Authorizer link Pre-print
13:50
20m
Talk
(PLDI 2020) Constant-Time Foundations for the New Spectre Era
SIGPLAN Track
Sunjay Cauligi University of California at San Diego, USA, Craig Disselkoen University of California at San Diego, USA, Klaus v. Gleissenthall Vrije Universiteit Amsterdam, Netherlands, Dean Tullsen University of California at San Diego, USA, Deian Stefan University of California at San Diego, Tamara Rezk INRIA, Gilles Barthe MPI-SP, Germany / IMDEA Software Institute, Spain
14:10
20m
Talk
(PLDI 2020) SCAF: A Speculation-Aware Collaborative Dependence Analysis Framework
SIGPLAN Track
Sotiris Apostolakis Google, Ziyang Xu Princeton University, Zujun Tan Princeton University, USA, Greg Chan Princeton University, USA, Simone Campanoni Northwestern University, USA, David I. August Princeton University
14:30
20m
Talk
(POPL 2021) Automatically Eliminating Speculative Leaks from Cryptographic Code with Blade
SIGPLAN Track
Marco Vassena Utrecht University, Craig Disselkoen University of California at San Diego, USA, Klaus v. Gleissenthall Vrije Universiteit Amsterdam, Netherlands, Sunjay Cauligi University of California at San Diego, USA, Rami Gökhan Kıcı University of California at San Diego, USA, Ranjit Jhala University of California at San Diego; Amazon Web Services, Dean Tullsen University of California at San Diego, USA, Deian Stefan University of California at San Diego
13:30 - 14:50
CompilationPLDI at Toucan +12h
Chair(s): James Larus EPFL
13:30
20m
Talk
Finding Typing Compiler BugsDistinguished Paper Award
PLDI
Stefanos Chaliasos Imperial College London, Thodoris Sotiropoulos Athens University of Economics and Business, Diomidis Spinellis Athens University of Economics and Business & Delft University of Technology, Arthur Gervais Imperial College London, Ben Livshits Imperial College London, UK, Dimitris Mitropoulos University of Athens
DOI
13:50
20m
Talk
IRDL: An IR Definition Language for SSA Compilers
PLDI
Mathieu Fehr University of Edinburgh, Jeff Niu University of Waterloo, River Riddle Google, Mehdi Amini Google, Zhendong Su ETH Zurich, Tobias Grosser University of Edinburgh
DOI
14:10
20m
Talk
Sequential Reasoning for Optimizing Compilers Under Weak Memory Concurrency
PLDI
Minki Cho Seoul National University, Sung-Hwan Lee Seoul National University, Dongjae Lee Seoul National University, Chung-Kil Hur Seoul National University, Ori Lahav Tel Aviv University
DOI Pre-print
14:30
20m
Talk
Deoptless: Speculation with Dispatched On-Stack Replacement and Specialized Continuations
PLDI
Olivier Flückiger Northeastern University, Jan Ječmen Czech Technical University, Sebastián Krynski Czech Technical University, Jan Vitek Northeastern University; Czech Technical University
DOI Pre-print
14:50 - 15:30
Boba Social (PLTea)PLDI at Boardroom
14:50
40m
Social Event
PL Teasocial
PLDI
Rachit Nigam Cornell University
15:30 - 16:50
ConcurrencySIGPLAN Track at Cockatoo
Chair(s): Umang Mathur National University of Singapore
15:30
20m
Talk
(PLDI 2020) Inductive Sequentialization of Asynchronous Programs
SIGPLAN Track
Constantin Enea Ecole Polytechnique / LIX / CNRS, Thomas A. Henzinger IST Austria, Austria, Bernhard Kragl IST Austria, Suha Orhun Mutluergil IRIF, France / University Paris Diderot, France / CNRS, France, Shaz Qadeer Novi, USA
15:50
20m
Talk
(PLDI 2021) When Threads Meet Events: Efficient and Precise Static Race Detection with Origins
SIGPLAN Track
Bozhen Liu Texas A&M University, USA, Peiming Liu Texas A&M University, Yanze Li University of British Columbia, Chia-Che Tsai Texas A&M University, Dilma Da Silva Texas A&M, Jeff Huang Texas A&M University
16:10
20m
Talk
(POPL 2021) Optimal Prediction of Synchronization-Preserving Races
SIGPLAN Track
Umang Mathur National University of Singapore, Andreas Pavlogiannis Aarhus University, Mahesh Viswanathan University of Illinois at Urbana-Champaign
16:30
20m
Talk
(POPL 2022) Visibility Reasoning for Concurrent Snapshot Algorithms
SIGPLAN Track
Joakim Öhman IMDEA Software Institute; Universidad Politécnica de Madrid, Aleksandar Nanevski IMDEA Software Institute
15:30 - 16:55
Synthesis IIPLDI at Kon-Tiki +12h
Chair(s): Roopsha Samanta Purdue University
15:30
20m
Talk
Can Reactive Synthesis and Syntax-Guided Synthesis Be Friends?
PLDI
Wonhyuk Choi Meta; Columbia University, Bernd Finkbeiner CISPA Helmholtz Center for Information Security, Ruzica Piskac Yale University, Mark Santolucito Barnard College, Columbia University, USA
DOI Pre-print
15:50
20m
Talk
Recursion Synthesis with Unrealizability Witnesses
PLDI
Azadeh Farzan University of Toronto, Danya Lette University of Toronto, Victor Nicolet University of Toronto
DOI
16:10
20m
Talk
TF-Coder: Program Synthesis for Tensor Manipulations (TOPLAS)
PLDI
Kensen Shi Google Brain, David Bieber Google Brain, Rishabh Singh Google Brain
Link to publication DOI Authorizer link Pre-print
16:30
20m
Talk
“Synthesizing Input Grammars”: A Replication Study
PLDI
Bachir Bendrissou CISPA Helmholtz Center for Information Security, Rahul Gopinath University of Sydney, Andreas Zeller CISPA Helmholtz Center for Information Security
DOI Pre-print
16:50
5m
Talk
Response by authors of "Synthesizing Input Grammars"
PLDI
Osbert Bastani University of Pennsylvania
15:30 - 16:50
Neural Networks and NumbersSIGPLAN Track at Macaw
Chair(s): Madan Musuvathi Microsoft Research
15:30
20m
Talk
(OOPSLA 2021) FPL: fast Presburger arithmetic through transprecision
SIGPLAN Track
Arjun Pitchanathan University of Edinburgh, Christian Ulmann ETH Zurich, Michel Weber ETH Zurich, Torsten Hoefler ETH Zurich, Tobias Grosser University of Edinburgh
Link to publication DOI Authorizer link Pre-print
15:50
20m
Talk
(PLDI 2021) Provable Repair of Deep Neural Networks
SIGPLAN Track
Matthew Sotoudeh University of California, Davis, Aditya V. Thakur University of California at Davis
16:10
20m
Talk
(POPL 2022) One Polynomial Approximation to Produce Correctly Rounded Results of an Elementary Function for Multiple Representations and Rounding Modes
SIGPLAN Track
Jay P. Lim Yale University, Santosh Nagarakatte Rutgers University
16:30
20m
Talk
(POPL 2022) Provably Correct, Asymptotically Efficient, Higher-Order Reverse-Mode Automatic Differentiation
SIGPLAN Track
Faustyna Krawiec University of Cambridge, Simon Peyton Jones Microsoft Research, Neel Krishnaswami University of Cambridge, Tom Ellis Microsoft Research, Richard A. Eisenberg Tweag, Andrew Fitzgibbon Graphcore
DOI
15:30 - 16:50
TensorsPLDI at Toucan +12h
Chair(s): Sreepathi Pai University of Rochester
15:30
20m
Talk
Autoscheduling for Sparse Tensor Algebra with an Asymptotic Cost Model
PLDI
Peter Ahrens MIT CSAIL, Fredrik Kjolstad Stanford University, Saman Amarasinghe MIT CSAIL
DOI
15:50
20m
Talk
DISTAL: The Distributed Tensor Algebra Compiler
PLDI
Rohan Yadav Stanford University, Alex Aiken Stanford Univeristy, Fredrik Kjolstad Stanford University
DOI
16:10
20m
Talk
All you need is Superword-Level Parallelism: Systematic Control-Flow Vectorization with SLP
PLDI
Yishen Chen Massachusetts Institute of Technology, Charith Mendis University of Illinois at Urbana-Champaign, Saman Amarasinghe Massachusetts Institute of Technology
DOI
16:30
20m
Talk
Warping Cache Simulation of Polyhedral Programs
PLDI
Canberk Morelli Saarland University, Jan Reineke Saarland University
DOI
17:30 - 19:00
Student Research Competition (SRC) Session and ReceptionSRC at Beach North
17:30
90m
Poster
Control Logic Synthesis Using Formal ISA Specifications
SRC
Benjamin Darnell University of California, Santa Barbara
Media Attached
17:30
90m
Poster
Coupled Applicative Functors
SRC
Lisa Vasilenko IMDEA Software Institute
Media Attached
17:30
90m
Poster
Program Synthesis for Processor Development Using Formal Specifications
SRC
Zachary Sisco UC Santa Barbara
Media Attached
17:30
90m
Poster
Path Alignment Automata are Probabilistic Couplings
SRC
Qian Meng Cornell university
Media Attached
17:30
90m
Poster
Multi-Phase Invariant Synthesis
SRC
Daniel Riley Florida State University
Media Attached
17:30
90m
Poster
Finding Good Generators with Multi-Armed Bandits
SRC
Joseph W. Cutler University of Pennsylvania
Media Attached
17:30
90m
Poster
Impacts of Range Reduction on Polynomial Approximation Efficiency
SRC
Sehyeok Park Rutgers University
Media Attached
17:30
90m
Poster
Automating NISQ Application Design with Meta Quantum Circuits with Constraints (MQCC)
SRC
Haowei Deng University of Maryland at College Park
Media Attached
17:30
90m
Poster
A Type System for Safe Intermittent Computing
SRC
Milijana Surbatovich Carnegie Mellon University
Media Attached
17:30
90m
Poster
PBUnit: A Live Programming Environment for Unit Testing
SRC
Justin Du University of California, San Diego, Mandeep Syal University of California, San Diego, Thanh-Nha Tran University of California, San Diego
Media Attached
17:30
90m
Poster
Visualization with Refinement Types
SRC
Junrui Liu University of California, Santa Barbara
Media Attached
18:00 - 19:00
PLDI 2022 ReceptionPLDI at Beach North
18:00
60m
Social Event
PLDI 2022 Reception (sponsored by WhatsApp by Meta)social
PLDI

19:00 - 22:00
19:00
3h
Dinner
W@PLDI Dinnersocial
W@PLDI

21:00 - 22:10
Keynote: Emery BergerPLDI at Kon-Tiki
21:00
10m
Other
Welcome to PLDI 2022
PLDI
Işıl Dillig University of Texas at Austin, Ranjit Jhala University of California at San Diego; Amazon Web Services
21:10
60m
Keynote
Getting Your Research Adopted
PLDI
Emery D. Berger University of Massachusetts Amherst
Pre-print Media Attached
21:00 - 21:30
21:00
30m
Social Event
PL Teasocial
PLDI
Rachit Nigam Cornell University
22:40 - 00:00
SecurityPLDI at Kon-Tiki
22:40
20m
Talk
P4BID: Information Flow Control in P4
PLDI
Karuna Grewal , Loris D'Antoni University of Wisconsin-Madison, USA, Justin Hsu Cornell University
DOI
23:00
20m
Talk
ANOSY: Approximated Knowledge Synthesis with Refinement Types for Declassification
PLDI
Sankha Narayan Guria University of Maryland, College Park, Niki Vazou IMDEA Software Institute, Marco Guarnieri IMDEA Software Institute, James Parker Galois, Inc.
DOI Pre-print
23:20
20m
Talk
Hardening Attack Surfaces with Formally Proven Binary Format Parsers
PLDI
Nikhil Swamy Microsoft Research, Tahina Ramananandro Microsoft Research, Aseem Rastogi Microsoft Research, Irina Spiridonova Microsoft Research, Haobin Ni Cornell University, Dmitry Malloy Microsoft, Juan Vazquez Microsoft, Michael Tang Microsoft, Omar Cardona Microsoft, Arti Gupta Microsoft
DOI
23:40
20m
Talk
Modular Information Flow Through Ownership
PLDI
Will Crichton Stanford University, Marco Patrignani University of Trento, Maneesh Agrawala Stanford University, Pat Hanrahan Stanford University, USA
DOI Pre-print
22:40 - 00:00
MemoryPLDI at Toucan
22:40
20m
Talk
Is it Time to Retire Manual Concurrent Memory Reclamation?
PLDI
Daniel Anderson Carnegie Mellon University, Guy E. Blelloch Carnegie Mellon University, Yuanhao Wei Carnegie Mellon University, USA
23:00
20m
Talk
Low-Latency, High-Throughput Garbage CollectionDistinguished Paper Award
PLDI
Wenyu Zhao Australian National University, Steve Blackburn Google and Australian National University, Kathryn S McKinley Google
DOI
23:20
20m
Talk
Mako: A Low-Pause, High-Throughput Evacuating Collector for Memory-Disaggregated Datacenters
PLDI
Haoran Ma University of California, Los Angeles, Shi Liu UCLA, Chenxi Wang UCLA, Yifan Qiao UCLA, Michael D. Bond Ohio State University, Steve Blackburn Google and Australian National University, Miryung Kim University of California at Los Angeles, USA, Guoqing Harry Xu University of California at Los Angeles
DOI
23:40
20m
Talk
PaC-trees: Supporting Parallel and Compressed Purely-Functional Collections
PLDI
Laxman Dhulipala Carnegie Mellon University, Guy E. Blelloch Carnegie Mellon University, Yan Gu UC Riverside, Yihan Sun University of California, Riverside
DOI

Thu 16 Jun

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

01:30 - 02:50
Synthesis I PLDI at Kon-Tiki
01:30
20m
Talk
WebRobot: Web Robotic Process Automation using Interactive Programming-by-Demonstration
PLDI
Rui Dong University of Michigan, Zhicheng Huang University of Michigan, Ian Iong Lam University of Michigan, Yan Chen University of Michigan, Xinyu Wang University of Michigan
DOI Pre-print
01:50
20m
Talk
Synthesizing Analytical SQL Queries from Computation DemonstrationDistinguished Paper Award
PLDI
Xiangyu Zhou University of Washington, Rastislav Bodík University of Washington, Alvin Cheung University of California, Berkeley, Chenglong Wang University of Washington, USA
DOI
02:10
20m
Talk
Type-Directed Program Synthesis for RESTful APIs
PLDI
Zheng Guo University of California, San Diego, David Cao University of California, San Diego, Davin Tjong University of California, San Diego, Jean Yang Akita Software, Cole Schlesinger Akita Software, Nadia Polikarpova University of California at San Diego
DOI
02:30
20m
Talk
Visualization Question Answering Using Introspective Program SynthesisDistinguished Paper Award
PLDI
Yanju Chen University of California, Santa Barbara, Xifeng Yan University of California, Santa Barbara, Yu Feng University of California, Santa Barbara
DOI
01:30 - 02:50
CompilationPLDI at Toucan
01:30
20m
Talk
Finding Typing Compiler BugsDistinguished Paper Award
PLDI
Stefanos Chaliasos Imperial College London, Thodoris Sotiropoulos Athens University of Economics and Business, Diomidis Spinellis Athens University of Economics and Business & Delft University of Technology, Arthur Gervais Imperial College London, Ben Livshits Imperial College London, UK, Dimitris Mitropoulos University of Athens
DOI
01:50
20m
Talk
IRDL: An IR Definition Language for SSA Compilers
PLDI
Mathieu Fehr University of Edinburgh, Jeff Niu University of Waterloo, River Riddle Google, Mehdi Amini Google, Zhendong Su ETH Zurich, Tobias Grosser University of Edinburgh
DOI
02:10
20m
Talk
Sequential Reasoning for Optimizing Compilers Under Weak Memory Concurrency
PLDI
Minki Cho Seoul National University, Sung-Hwan Lee Seoul National University, Dongjae Lee Seoul National University, Chung-Kil Hur Seoul National University, Ori Lahav Tel Aviv University
DOI Pre-print
02:30
20m
Talk
Deoptless: Speculation with Dispatched On-Stack Replacement and Specialized Continuations
PLDI
Olivier Flückiger Northeastern University, Jan Ječmen Czech Technical University, Sebastián Krynski Czech Technical University, Jan Vitek Northeastern University; Czech Technical University
DOI Pre-print
02:30 - 03:00
02:30
30m
Social Event
PL Teasocial
PLDI
Rachit Nigam Cornell University
03:30 - 04:55
Synthesis IIPLDI at Kon-Tiki
03:30
20m
Talk
Can Reactive Synthesis and Syntax-Guided Synthesis Be Friends?
PLDI
Wonhyuk Choi Meta; Columbia University, Bernd Finkbeiner CISPA Helmholtz Center for Information Security, Ruzica Piskac Yale University, Mark Santolucito Barnard College, Columbia University, USA
DOI Pre-print
03:50
20m
Talk
Recursion Synthesis with Unrealizability Witnesses
PLDI
Azadeh Farzan University of Toronto, Danya Lette University of Toronto, Victor Nicolet University of Toronto
DOI
04:10
20m
Talk
TF-Coder: Program Synthesis for Tensor Manipulations (TOPLAS)
PLDI
Kensen Shi Google Brain, David Bieber Google Brain, Rishabh Singh Google Brain
Link to publication DOI Authorizer link Pre-print
04:30
20m
Talk
“Synthesizing Input Grammars”: A Replication Study
PLDI
Bachir Bendrissou CISPA Helmholtz Center for Information Security, Rahul Gopinath University of Sydney, Andreas Zeller CISPA Helmholtz Center for Information Security
DOI Pre-print
04:50
5m
Talk
Response by authors of "Synthesizing Input Grammars"
PLDI
Osbert Bastani University of Pennsylvania
03:30 - 04:50
TensorsPLDI at Toucan
03:30
20m
Talk
Autoscheduling for Sparse Tensor Algebra with an Asymptotic Cost Model
PLDI
Peter Ahrens MIT CSAIL, Fredrik Kjolstad Stanford University, Saman Amarasinghe MIT CSAIL
DOI
03:50
20m
Talk
DISTAL: The Distributed Tensor Algebra Compiler
PLDI
Rohan Yadav Stanford University, Alex Aiken Stanford Univeristy, Fredrik Kjolstad Stanford University
DOI
04:10
20m
Talk
All you need is Superword-Level Parallelism: Systematic Control-Flow Vectorization with SLP
PLDI
Yishen Chen Massachusetts Institute of Technology, Charith Mendis University of Illinois at Urbana-Champaign, Saman Amarasinghe Massachusetts Institute of Technology
DOI
04:30
20m
Talk
Warping Cache Simulation of Polyhedral Programs
PLDI
Canberk Morelli Saarland University, Jan Reineke Saarland University
DOI
09:00 - 10:10
Keynote: Margo SeltzerPLDI at Kon-Tiki +12h
Chair(s): Ranjit Jhala University of California at San Diego; Amazon Web Services
09:00
10m
Other
The PLDI Song
PLDI
John Wickerson Imperial College London, Alastair F. Donaldson Imperial College London
09:10
60m
Keynote
Imposter Syndrome, Stupid Questions, and Eight (+/-2) Problems I Need your Help With
PLDI
Margo Seltzer University of British Columbia
10:10 - 10:40
PL Tea (Thu AM)PLDI at Boardroom
10:10
30m
Social Event
PL Teasocial
PLDI
Rachit Nigam Cornell University
10:30 - 11:50
Student Research Competition (SRC) Finals SessionSRC at Rousseau East
10:40 - 12:00
Synthesis ISIGPLAN Track at Cockatoo
Chair(s): Xinyu Wang University of Michigan
10:40
20m
Talk
(PLDI 2021) DreamCoder: Bootstrapping inductive program synthesis with wake-sleep library learning
SIGPLAN Track
Kevin Ellis Cornell University, Lionel Wong Massachusetts Institute of Technology, Maxwell Nye Massachusetts Institute of Technology, Mathias Sablé-Meyer PSL University; Collège de France; NeuroSpin, Lucas Morales Massachusetts Institute of Technology, Luke Hewitt Massachusetts Institute of Technology, Luc Cary Massachusetts Institute of Technology, Armando Solar-Lezama Massachusetts Institute of Technology, Joshua B. Tenenbaum MIT
11:00
20m
Talk
(POPL 2021) egg: Fast and Extensible Equality Saturation
SIGPLAN Track
Max Willsey University of Washington, Chandrakana Nandi Certora, inc., Yisu Remy Wang University of Washington, Oliver Flatt University of Utah, Zachary Tatlock University of Washington, Pavel Panchekha University of Utah
11:20
20m
Talk
(POPL 2022) Relational E-Matching
SIGPLAN Track
Yihong Zhang University of Washington, Yisu Remy Wang University of Washington, Max Willsey University of Washington, Zachary Tatlock University of Washington
11:40
20m
Talk
(OOPSLA 2020) Just-in-Time Learning for Bottom-up Enumerative Synthesis
SIGPLAN Track
Shraddha Barke University of California at San Diego, Hila Peleg Technion, Nadia Polikarpova University of California at San Diego
10:40 - 12:00
DistributionPLDI at Kon-Tiki +12h
Chair(s): Constantin Enea Ecole Polytechnique / LIX / CNRS
10:40
20m
Talk
Certified Mergeable Replicated Data Types
PLDI
Vimala Soundarapandian IIT Madras, Adharsh Kamath NITK Surathkal, Kartik Nagar IIT Madras, KC Sivaramakrishnan IIT Madras and Tarides
DOI Pre-print
11:00
20m
Talk
Hamband: RDMA Replicated Data Types
PLDI
Farzin Houshmand University of California, Riverside, Javad Saberlatibari University of California Riverside, Mohsen Lesani University of California at Riverside
DOI
11:20
20m
Talk
RunTime-Assisted Convergence in Replicated Data Types
PLDI
Gowtham Kaki University of Colorado Boulder, Prasanth Prahladan University of Colorado Boulder, Nicholas V. Lewchenko University of Colorado Boulder
DOI
11:40
20m
Talk
Adore: Atomic Distributed Objects with Certified Reconfiguration
PLDI
Wolf Honore Yale University, Ji-Yong Shin Northeastern University, Jieung Kim Yale University, USA, Zhong Shao Yale University
DOI Pre-print
10:40 - 12:00
Parsing & VerificationSIGPLAN Track at Macaw
Chair(s): Jay P. Lim Yale University
10:40
20m
Talk
(ICFP 2021) Formal Verification of a Concurrent Bounded Queue in a Weak Memory Model
SIGPLAN Track
Glen Mével Inria, Université Paris-Saclay, CNRS, ENS Paris-Saclay, Laboratoire des méthodes formelles, Jacques-Henri Jourdan Université Paris-Saclay, CNRS, ENS Paris-Saclay, Laboratoire Méthodes Formelles
11:00
20m
Talk
(PLDI 2020) Zippy LL(1) Parsing with Derivatives
SIGPLAN Track
Romain Edelmann EPFL, Switzerland, Jad Hamza EPFL, Switzerland, Viktor Kunčak EPFL, Switzerland
11:20
20m
Talk
(PLDI 2021) CoStar: A Verified ALL(*) Parser
SIGPLAN Track
Sam Lasser Tufts University, Chris Casinghino Draper Laboratory, Kathleen Fisher Tufts University, Cody Roux Draper
11:40
20m
Talk
(PLDI 2021) Transfinite Iris: Resolving an Existential Dilemma of Step-Indexed Separation Logic
SIGPLAN Track
Simon Spies MPI-SWS & Saarland University, Lennard Gäher MPI-SWS & Saarland University, Daniel Gratzer Aarhus University, Joseph Tassarotti Boston College, Robbert Krebbers Radboud University Nijmegen, Derek Dreyer MPI-SWS, Lars Birkedal Aarhus University
10:40 - 12:00
AnalysisPLDI at Toucan +12h
Chair(s): Xiaokang Qiu Purdue University, USA
10:40
20m
Talk
CycleQ: an efficient basis for cyclic equational reasoning
PLDI
Eddie Jones University of Bristol, C.-H. Luke Ong University of Oxford, Steven Ramsay University of Bristol
DOI
11:00
20m
Talk
Finding the Dwarf: Recovering Precise Types from WebAssembly Binaries
PLDI
Daniel Lehmann University of Stuttgart, Michael Pradel University of Stuttgart
DOI Pre-print
11:20
20m
Talk
Abstract Interpretation Repair
PLDI
Roberto Bruni University of Pisa, Roberto Giacobazzi University of Verona, Roberta Gori University of Pisa, Francesco Ranzato University of Padova
DOI Pre-print
11:40
20m
Talk
Differential Cost Analysis with Simultaneous Potentials and Anti-potentials
PLDI
Đorđe Žikelić IST Austria, Pauline Bolignano Amazon, Bor-Yuh Evan Chang University of Colorado Boulder & Amazon, Franco Raimondi Amazon & Middlesex University
DOI Pre-print
12:00 - 13:00
Thursday LunchPLDI at Beach North
12:00
60m
Lunch
Lunchsocial
PLDI

13:30 - 14:50
Synthesis IISIGPLAN Track at Cockatoo
Chair(s): Mohsen Lesani University of California at Riverside
13:30
20m
Talk
(PLDI 2021) Phased Synthesis of Divide and Conquer Programs
SIGPLAN Track
Azadeh Farzan University of Toronto, Victor Nicolet University of Toronto
13:50
20m
Talk
(OOPSLA 2021) LooPy: interactive program synthesis with control structures
SIGPLAN Track
Kasra Ferdowsi University of California at San Diego, Shraddha Barke , Hila Peleg Technion, Sorin Lerner University of California at San Diego, Nadia Polikarpova University of California at San Diego
Link to publication DOI Authorizer link Pre-print
14:10
20m
Talk
(OOPSLA 2020) Feedback-Driven Semi-Supervised Synthesis of Program Transformations
SIGPLAN Track
Xiang Gao Beihang University, China, Shraddha Barke University of California at San Diego, Arjun Radhakrishna Microsoft, Gustavo Soares Microsoft, Sumit Gulwani Microsoft, Alan Leung Microsoft, Nachiappan Nagappan Facebook, Ashish Tiwari Microsoft
14:30
20m
Talk
(PLDI 2021) Proof Repair Across Type Equivalences
SIGPLAN Track
Talia Ringer University of Illinois at Urbana-Champaign, RanDair Porter University of Washington, Nathaniel Yazdani University of Washington, Seattle, John Leo Halfaya Research, Dan Grossman University of Washington
Link to publication DOI Authorizer link Pre-print
13:30 - 14:50
ConcurrencyPLDI at Kon-Tiki +12h
Chair(s): Mike Dodds Galois, Inc.
13:30
20m
Talk
A Flexible Type System for Fearless Concurrency
PLDI
Mae Milano University of California, Berkeley, Julia Turcotti University of California, Berkeley, Andrew Myers Cornell University
DOI
13:50
20m
Talk
A Study of Real-world Data Races in Golang
PLDI
Milind Chabbi Uber Technologies Inc., Murali Krishna Ramanathan Uber Technologies Inc.
DOI
14:10
20m
Talk
Checking Robustness to Weak Persistency Models
PLDI
Hamed Gorjiara University of California, Irvine, Weiyu Luo University of California, Irvine, Alex Lee University of California, Irvine, Guoqing Harry Xu University of California at Los Angeles, Brian Demsky University of California, Irvine
DOI
14:30
20m
Talk
Sound Sequentialization for Concurrent Program Verification
PLDI
Azadeh Farzan University of Toronto, Dominik Klumpp University of Freiburg, Andreas Podelski University of Freiburg, Germany
DOI File Attached
13:30 - 14:50
NumbersPLDI at Toucan +12h
Chair(s): Chandrakana Nandi Certora, inc.
13:30
20m
Talk
Choosing Mathematical Function Implementations for Speed and Accuracy
PLDI
Ian Briggs University of Utah, Pavel Panchekha University of Utah
DOI
13:50
20m
Talk
Guaranteed bounds for posterior inference in universal probabilistic programming
PLDI
Raven Beutner CISPA Helmholtz Center for Information Security, Germany, C.-H. Luke Ong University of Oxford, Fabian Zaiser University of Oxford
DOI Pre-print
14:10
20m
Talk
Progressive Polynomial Approximations for Fast Correctly Rounded Math Libraries
PLDI
Mridul Aanjaneya Rutgers University, Jay P. Lim Yale University, Santosh Nagarakatte Rutgers University
Link to publication DOI Pre-print
14:30
20m
Talk
Karp: A Language for NP Reductions
PLDI
Chenhao Zhang Northwestern University, Jason D. Hartline Northwestern University, Christos Dimoulas PLT @ Northwestern University
DOI
14:50 - 15:30
PL Tea (Thu PM)PLDI at Boardroom
14:50
40m
Social Event
PL Teasocial
PLDI
Rachit Nigam Cornell University
15:30 - 16:50
TestingSIGPLAN Track at Cockatoo
Chair(s): Yu Feng University of California, Santa Barbara
15:30
20m
Talk
(OOPSLA 2020) A Model for Detecting Faults in Build Specifications
SIGPLAN Track
Thodoris Sotiropoulos Athens University of Economics and Business, Stefanos Chaliasos Imperial College London, Dimitris Mitropoulos University of Athens, Diomidis Spinellis Athens University of Economics and Business & Delft University of Technology
15:50
20m
Talk
(OOPSLA 2020) Unifying Execution of Imperative Generators and Declarative Specifications
SIGPLAN Track
Pengyu Nie University of Texas at Austin, Marinela Parovic University of Texas at Austin, Zhiqiang Zang University of Texas at Austin, Sarfraz Khurshid University of Texas at Austin, Aleksandar Milicevic Microsoft, Milos Gligoric University of Texas at Austin
16:10
20m
Talk
(PLDI 2021) Logical Bytecode Reduction
SIGPLAN Track
Christian Gram Kalhauge Technical University of Denmark, Jens Palsberg University of California, Los Angeles (UCLA)
16:30
20m
Talk
(PLDI 2021) Quantum abstract interpretation
SIGPLAN Track
Nengkun Yu UTS, Jens Palsberg University of California, Los Angeles (UCLA)
Link to publication DOI Authorizer link Pre-print
15:30 - 16:50
SemanticsPLDI at Kon-Tiki +12h
Chair(s): Nate Foster Cornell University
15:30
20m
Talk
A Typed Continuation-Passing Translation for Lexical Effect Handlers
PLDI
Philipp Schuster University of Tübingen, Jonathan Immanuel Brachthäuser University of Tübingen, Marius Müller University of Tübingen, Klaus Ostermann University of Tuebingen
DOI
15:50
20m
Talk
Deep and Shallow Types for Gradual Languages
PLDI
Ben Greenman Brown University
DOI
16:10
20m
Talk
Kleene Algebra Modulo Theories: A Framework for Concrete KATsDistinguished Paper Award
PLDI
Michael Greenberg Stevens Institute of Technology, Ryan Beckett Microsoft Research, USA, Eric Campbell Cornell University
DOI Pre-print
16:30
20m
Talk
Semantic Soundness for Language Interoperability
PLDI
Daniel Patterson Northeastern University, Noble Mushtak Northeastern University, Andrew Wagner Northeastern University, Amal Ahmed Northeastern University (USA)
DOI
15:30 - 16:50
StorageSIGPLAN Track at Macaw
Chair(s): Albert Cohen Google
15:30
20m
Talk
(PLDI 2020) Automatic Generation of Efficient Sparse Tensor Format Conversion Routines
SIGPLAN Track
Stephen Chou Massachusetts Institute of Technology, Fredrik Kjolstad Stanford University, Saman Amarasinghe MIT CSAIL
15:50
20m
Talk
(PLDI 2020) NVTraverse: In NVRAM Data Structures, the Destination is More Important than the Journey
SIGPLAN Track
Naama Ben-David Carnegie Mellon University, USA, Guy E. Blelloch Carnegie Mellon University, Michal Friedman Technion, Israel, Erez Petrank Technion, Israel, Yuanhao Wei Carnegie Mellon University, USA
16:10
20m
Talk
(PLDI 2021) Mirror: Making Lock-Free Data Structures Persistent
SIGPLAN Track
Michal Friedman Technion, Israel, Erez Petrank Technion, Israel, Pedro Ramalhete Cisco Systems
16:30
20m
Talk
(POPL 2021) Provably Space Efficient Parallel Functional Programming
SIGPLAN Track
Jatin Arora Carnegie Mellon University, Sam Westrick Carnegie Mellon University, Umut A. Acar Carnegie Mellon University
15:30 - 16:50
QuantumPLDI at Toucan +12h
Chair(s): Sara Achour MIT
15:30
20m
Talk
Quartz: Superoptimization of Quantum Circuits
PLDI
Mingkuan Xu Carnegie Mellon University, Zikun Li University of California, Los Angeles (UCLA), Oded Padon VMware Research, Sina Lin Microsoft, Jessica Pointing University of Oxford, Auguste Hirth University of California, Los Angeles (UCLA), Henry Ma University of California, Los Angeles (UCLA), Jens Palsberg University of California, Los Angeles (UCLA), Alex Aiken Stanford Univeristy, Umut A. Acar Carnegie Mellon University, Zhihao Jia Carnegie Mellon University
DOI
15:50
20m
Talk
Giallar: Push-button Verification for the Qiskit Quantum Compiler
PLDI
Runzhou Tao Columbia University, Yunong Shi Amazon, Jianan Yao Columbia University, Xupeng Li Columbia University, Ali Javadi-Abhari IBM, Andrew Cross IBM T.J Watson Research Center, Frederic T. Chong University of Chicago, Ronghui Gu Columbia University
DOI
16:10
20m
Talk
Algebraic Reasoning of Quantum Programs via Non-Idempotent Kleene Algebra
PLDI
Yuxiang Peng University of Maryland, Mingsheng Ying Tsinghua University, Xiaodi Wu Department of Computer Science, Institute for Advanced Computer Studies, and Joint Center for Quantum Information and Computer Science, University of Maryland, MD
DOI
16:30
20m
Talk
PyLSE: A Pulse-Transfer Level Language for Superconductor Electronics
PLDI
Michael Christensen University of California at Santa Barbara, Georgios Tzimpragos UC Santa Barbara, Harlan Kringen UC Santa Barbara, Jennifer Volk UC Santa Barbara, Timothy Sherwood UC Santa Barbara, Ben Hardekopf UC Santa Barbara
DOI
21:00 - 22:10
Keynote: Margo SeltzerPLDI at Kon-Tiki
21:00
10m
Other
The PLDI Song
PLDI
John Wickerson Imperial College London, Alastair F. Donaldson Imperial College London
21:10
60m
Keynote
Imposter Syndrome, Stupid Questions, and Eight (+/-2) Problems I Need your Help With
PLDI
Margo Seltzer University of British Columbia
21:00 - 21:30
21:00
30m
Social Event
PL Teasocial
PLDI
Rachit Nigam Cornell University
22:40 - 00:00
DistributionPLDI at Kon-Tiki
22:40
20m
Talk
Certified Mergeable Replicated Data Types
PLDI
Vimala Soundarapandian IIT Madras, Adharsh Kamath NITK Surathkal, Kartik Nagar IIT Madras, KC Sivaramakrishnan IIT Madras and Tarides
DOI Pre-print
23:00
20m
Talk
Hamband: RDMA Replicated Data Types
PLDI
Farzin Houshmand University of California, Riverside, Javad Saberlatibari University of California Riverside, Mohsen Lesani University of California at Riverside
DOI
23:20
20m
Talk
RunTime-Assisted Convergence in Replicated Data Types
PLDI
Gowtham Kaki University of Colorado Boulder, Prasanth Prahladan University of Colorado Boulder, Nicholas V. Lewchenko University of Colorado Boulder
DOI
23:40
20m
Talk
Adore: Atomic Distributed Objects with Certified Reconfiguration
PLDI
Wolf Honore Yale University, Ji-Yong Shin Northeastern University, Jieung Kim Yale University, USA, Zhong Shao Yale University
DOI Pre-print
22:40 - 00:00
AnalysisPLDI at Toucan
22:40
20m
Talk
CycleQ: an efficient basis for cyclic equational reasoning
PLDI
Eddie Jones University of Bristol, C.-H. Luke Ong University of Oxford, Steven Ramsay University of Bristol
DOI
23:00
20m
Talk
Finding the Dwarf: Recovering Precise Types from WebAssembly Binaries
PLDI
Daniel Lehmann University of Stuttgart, Michael Pradel University of Stuttgart
DOI Pre-print
23:20
20m
Talk
Abstract Interpretation Repair
PLDI
Roberto Bruni University of Pisa, Roberto Giacobazzi University of Verona, Roberta Gori University of Pisa, Francesco Ranzato University of Padova
DOI Pre-print
23:40
20m
Talk
Differential Cost Analysis with Simultaneous Potentials and Anti-potentials
PLDI
Đorđe Žikelić IST Austria, Pauline Bolignano Amazon, Bor-Yuh Evan Chang University of Colorado Boulder & Amazon, Franco Raimondi Amazon & Middlesex University
DOI Pre-print

Fri 17 Jun

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

01:30 - 02:50
ConcurrencyPLDI at Kon-Tiki
01:30
20m
Talk
A Flexible Type System for Fearless Concurrency
PLDI
Mae Milano University of California, Berkeley, Julia Turcotti University of California, Berkeley, Andrew Myers Cornell University
DOI
01:50
20m
Talk
A Study of Real-world Data Races in Golang
PLDI
Milind Chabbi Uber Technologies Inc., Murali Krishna Ramanathan Uber Technologies Inc.
DOI
02:10
20m
Talk
Checking Robustness to Weak Persistency Models
PLDI
Hamed Gorjiara University of California, Irvine, Weiyu Luo University of California, Irvine, Alex Lee University of California, Irvine, Guoqing Harry Xu University of California at Los Angeles, Brian Demsky University of California, Irvine
DOI
02:30
20m
Talk
Sound Sequentialization for Concurrent Program Verification
PLDI
Azadeh Farzan University of Toronto, Dominik Klumpp University of Freiburg, Andreas Podelski University of Freiburg, Germany
DOI File Attached
01:30 - 02:50
NumbersPLDI at Toucan
01:30
20m
Talk
Choosing Mathematical Function Implementations for Speed and Accuracy
PLDI
Ian Briggs University of Utah, Pavel Panchekha University of Utah
DOI
01:50
20m
Talk
Guaranteed bounds for posterior inference in universal probabilistic programming
PLDI
Raven Beutner CISPA Helmholtz Center for Information Security, Germany, C.-H. Luke Ong University of Oxford, Fabian Zaiser University of Oxford
DOI Pre-print
02:10
20m
Talk
Progressive Polynomial Approximations for Fast Correctly Rounded Math Libraries
PLDI
Mridul Aanjaneya Rutgers University, Jay P. Lim Yale University, Santosh Nagarakatte Rutgers University
Link to publication DOI Pre-print
02:30
20m
Talk
Karp: A Language for NP Reductions
PLDI
Chenhao Zhang Northwestern University, Jason D. Hartline Northwestern University, Christos Dimoulas PLT @ Northwestern University
DOI
02:30 - 03:00
02:30
30m
Social Event
PL Teasocial
PLDI
Rachit Nigam Cornell University
03:30 - 04:50
SemanticsPLDI at Kon-Tiki
03:30
20m
Talk
A Typed Continuation-Passing Translation for Lexical Effect Handlers
PLDI
Philipp Schuster University of Tübingen, Jonathan Immanuel Brachthäuser University of Tübingen, Marius Müller University of Tübingen, Klaus Ostermann University of Tuebingen
DOI
03:50
20m
Talk
Deep and Shallow Types for Gradual Languages
PLDI
Ben Greenman Brown University
DOI
04:10
20m
Talk
Kleene Algebra Modulo Theories: A Framework for Concrete KATsDistinguished Paper Award
PLDI
Michael Greenberg Stevens Institute of Technology, Ryan Beckett Microsoft Research, USA, Eric Campbell Cornell University
DOI Pre-print
04:30
20m
Talk
Semantic Soundness for Language Interoperability
PLDI
Daniel Patterson Northeastern University, Noble Mushtak Northeastern University, Andrew Wagner Northeastern University, Amal Ahmed Northeastern University (USA)
DOI
03:30 - 04:50
QuantumPLDI at Toucan
03:30
20m
Talk
Quartz: Superoptimization of Quantum Circuits
PLDI
Mingkuan Xu Carnegie Mellon University, Zikun Li University of California, Los Angeles (UCLA), Oded Padon VMware Research, Sina Lin Microsoft, Jessica Pointing University of Oxford, Auguste Hirth University of California, Los Angeles (UCLA), Henry Ma University of California, Los Angeles (UCLA), Jens Palsberg University of California, Los Angeles (UCLA), Alex Aiken Stanford Univeristy, Umut A. Acar Carnegie Mellon University, Zhihao Jia Carnegie Mellon University
DOI
03:50
20m
Talk
Giallar: Push-button Verification for the Qiskit Quantum Compiler
PLDI
Runzhou Tao Columbia University, Yunong Shi Amazon, Jianan Yao Columbia University, Xupeng Li Columbia University, Ali Javadi-Abhari IBM, Andrew Cross IBM T.J Watson Research Center, Frederic T. Chong University of Chicago, Ronghui Gu Columbia University
DOI
04:10
20m
Talk
Algebraic Reasoning of Quantum Programs via Non-Idempotent Kleene Algebra
PLDI
Yuxiang Peng University of Maryland, Mingsheng Ying Tsinghua University, Xiaodi Wu Department of Computer Science, Institute for Advanced Computer Studies, and Joint Center for Quantum Information and Computer Science, University of Maryland, MD
DOI
04:30
20m
Talk
PyLSE: A Pulse-Transfer Level Language for Superconductor Electronics
PLDI
Michael Christensen University of California at Santa Barbara, Georgios Tzimpragos UC Santa Barbara, Harlan Kringen UC Santa Barbara, Jennifer Volk UC Santa Barbara, Timothy Sherwood UC Santa Barbara, Ben Hardekopf UC Santa Barbara
DOI
09:00 - 10:00
Business MeetingPLDI at Kon-Tiki +12h
09:00
60m
Meeting
Business Meeting
PLDI
Işıl Dillig University of Texas at Austin, Ranjit Jhala University of California at San Diego; Amazon Web Services, Steve Blackburn Google and Australian National University
10:10 - 10:40
PL Tea (Fri AM)PLDI at Boardroom
10:10
30m
Social Event
PL Teasocial
PLDI
Rachit Nigam Cornell University
10:40 - 12:00
ProbabilitySIGPLAN Track at Cockatoo
Chair(s): Eric Atkinson MIT CSAIL
10:40
20m
Talk
(OOPSLA 2020) Scaling Exact Inference for Discrete Probabilistic Programs
SIGPLAN Track
Steven Holtzen Northeastern University, Guy Van den Broeck University of California at Los Angeles, Todd Millstein University of California at Los Angeles
11:00
20m
Talk
(POPL 2021) A Pre-Expectation Calculus for Probabilistic Sensitivity
SIGPLAN Track
Alejandro Aguirre IMDEA Software Institute and T.U. of Madrid (UPM), Gilles Barthe MPI-SP, Germany / IMDEA Software Institute, Spain, Justin Hsu Cornell University, Benjamin Lucien Kaminski Saarland University and University College London, Joost-Pieter Katoen RWTH Aachen University, Christoph Matheja Technical University of Denmark
11:20
20m
Talk
(PLDI 2021) On Probabilistic Termination of Functional Programs with Continuous Distributions
SIGPLAN Track
Raven Beutner CISPA Helmholtz Center for Information Security, Germany, C.-H. Luke Ong University of Oxford
11:40
20m
Talk
(POPL 2021) Paradoxes of probabilistic programming
SIGPLAN Track
Jules Jacobs Radboud University
10:40 - 12:00
Hardware IPLDI at Kon-Tiki +12h
Chair(s): Clément Pit-Claudel EPFL, AWS
10:40
20m
Talk
Bind the Gap: Compiling Real Software to Hardware FFT Accelerators
PLDI
Jackson Woodruff University of Edinburgh, Jordi Armengol-Estapé University of Edinburgh, Sam Ainsworth University of Edinburgh, UK, Michael F. P. O'Boyle University of Edinburgh
DOI
11:00
20m
Talk
Exocompilation for Productive Programming of Hardware Accelerators
PLDI
Yuka Ikarashi MIT, Gilbert Bernstein University of California at Berkeley, Alex Reinking UC Berkeley, Hasan Genc UC Berkeley, Jonathan Ragan-Kelley MIT
DOI
11:20
20m
Talk
PDL: A High-Level Hardware Design Language for Pipelined Processors
PLDI
Drew Zagieboylo Cornell University, Charles Sherk Cornell University, G. Edward Suh Cornell University / Facebook, Andrew Myers Cornell University
DOI
11:40
20m
Talk
WARio: Efficient Code Generation for Intermittent Computing
PLDI
Vito Kortbeek Delft University of Technology, Souradip Ghosh Carnegie Mellon University, Josiah Hester Northwestern University, Simone Campanoni Northwestern University, USA, Przemysław Pawełczak Delft University of Technology
DOI Pre-print
10:40 - 12:00
CompilationSIGPLAN Track at Macaw
Chair(s): Deian Stefan University of California at San Diego
10:40
20m
Talk
(OOPSLA 2020) Counterexample-Guided Correlation Algorithm for Translation Validation
SIGPLAN Track
Shubhani Gupta , Abhishek Rose IIT Delhi, Sorav Bansal IIT Delhi and CompilerAI Labs
11:00
20m
Talk
(OOPSLA 2021) Formal verification of high-level synthesis
SIGPLAN Track
Yann Herklotz Imperial College London, James D. Pollard Imperial College London, Nadesh Ramanathan Imperial College London, John Wickerson Imperial College London
Link to publication DOI Authorizer link Pre-print
11:20
20m
Talk
(OOPSLA 2021) Well-typed programs can go wrong: a study of typing-related bugs in JVM compilers
SIGPLAN Track
Stefanos Chaliasos Imperial College London, Thodoris Sotiropoulos Athens University of Economics and Business, Georgios-Petros Drosos Athens University of Economics and Business, Charalambos Ioannis Mitropoulos Technical University of Crete, Dimitris Mitropoulos University of Athens, Diomidis Spinellis Athens University of Economics and Business & Delft University of Technology
Link to publication DOI Authorizer link Pre-print
11:40
20m
Talk
(POPL 2021) Formally Verified Speculation and Deoptimization in a JIT Compiler
SIGPLAN Track
Aurèle Barrière Univ Rennes, IRISA, Sandrine Blazy Univ Rennes, IRISA, Olivier Flückiger Northeastern University, David Pichardie Meta, Jan Vitek Northeastern University; Czech Technical University
10:40 - 12:00
Hardware IIPLDI at Toucan +12h
Chair(s): Anders Miltner Simon Fraser University
10:40
20m
Talk
Software-Hardware Codesign for Efficient In-Memory Regular Pattern Matchingvirtual
PLDI
Konstantinos Mamouras Rice University, Kaiyuan Yang Rice University, Lingkun Kong Rice University, Qixuan Yu Rice University, Agnishom Chattopadhyay Rice University, Alexis Le Glaunec Rice University, Yi Huang Rice University
Link to publication DOI
12:00 - 13:00
Friday LunchPLDI at Beach North
12:00
60m
Lunch
Lunchsocial
PLDI

13:30 - 14:50
Special EffectsSIGPLAN Track at Cockatoo
Chair(s): Steven Holtzen Northeastern University
13:30
20m
Talk
(POPL 2022) Twist: Sound Reasoning for Purity and Entanglement in Quantum Programs
SIGPLAN Track
Charles Yuan Massachusetts Institute of Technology, Christopher McNally Massachusetts Institute of Technology, Michael Carbin Massachusetts Institute of Technology
Link to publication DOI Authorizer link Pre-print
13:50
20m
Talk
(ICFP 2020) Compiling effect handlers in capability-passing style
SIGPLAN Track
Philipp Schuster University of Tübingen, Jonathan Immanuel Brachthäuser University of Tübingen, Klaus Ostermann University of Tuebingen
Link to publication DOI Authorizer link Pre-print
14:10
20m
Talk
(POPL 2021) Intensional Datatype Refinement
SIGPLAN Track
Eddie Jones University of Bristol, Steven Ramsay University of Bristol
14:30
20m
Talk
(POPL 2021) A Verified Optimizer for Quantum Circuits
SIGPLAN Track
Kesha Hietala University of Maryland, Robert Rand University of Chicago, Shih-Han Hung University of Maryland, USA, Xiaodi Wu Department of Computer Science, Institute for Advanced Computer Studies, and Joint Center for Quantum Information and Computer Science, University of Maryland, MD, Michael Hicks University of Maryland at College Park
13:30 - 14:50
Verification IPLDI at Kon-Tiki +12h
Chair(s): Ralf Jung MPI-SWS
13:30
20m
Talk
Compass: Strong and Compositional Library Specifications in Relaxed Memory Separation Logic
PLDI
Hoang-Hai Dang MPI-SWS, Jaehwang Jung KAIST, South Korea, Jaemin Choi KAIST, Duc-Than Nguyen University of Illinois at Chicago, William Mansky University of Illinois at Chicago, Jeehoon Kang KAIST, Derek Dreyer MPI-SWS
DOI
13:50
20m
Talk
Diaframe: Automated Verification of Fine-Grained Concurrent Programs in Iris
PLDI
Ike Mulder Radboud University Nijmegen, Robbert Krebbers Radboud University Nijmegen, Herman Geuvers Radboud University Nijmegen, Netherlands
Link to publication DOI Pre-print
14:10
20m
Talk
Islaris: Verification of Machine Code Against Authoritative ISA Semantics
PLDI
Michael Sammler MPI-SWS, Angus Hammond University of Cambridge, Rodolphe Lepigre MPI-SWS, Brian Campbell University of Edinburgh, Jean Pichon-Pharabod Aarhus University, Derek Dreyer MPI-SWS, Deepak Garg MPI-SWS, Peter Sewell University of Cambridge
DOI
14:30
20m
Talk
RustHornBelt: A Semantic Foundation for Functional Verification of Rust Programs with Unsafe CodeDistinguished Paper Award
PLDI
Yusuke Matsushita The University of Tokyo, Xavier Denis Université Paris-Saclay, CNRS, ENS Paris-Saclay, INRIA, Laboratoire Méthodes Formelles, Jacques-Henri Jourdan Université Paris-Saclay, CNRS, ENS Paris-Saclay, Laboratoire Méthodes Formelles, Derek Dreyer MPI-SWS
DOI
13:30 - 14:50
MelangeSIGPLAN Track at Macaw
Chair(s): Rachit Nigam Cornell University
13:30
20m
Talk
(OOPSLA 2020) Automatic and Efficient Variability-Aware Lifting of Functional Programs
SIGPLAN Track
Ramy Shahin University of Toronto, Marsha Chechik University of Toronto
13:50
20m
Talk
(OOPSLA 2021) Safer at Any Speed: Automatic Context-Aware Safety Enhancement for Rust
SIGPLAN Track
Natalie Popescu Princeton University, Ziyang Xu Princeton University, Sotiris Apostolakis Google, David I. August Princeton University, Amit Levy
Link to publication DOI Authorizer link Pre-print
14:10
20m
Talk
(OOPSLA 2021) The semantics of shared memory in Intel CPU/FPGA systems
SIGPLAN Track
Dan Iorga Imperial College London, Alastair F. Donaldson Imperial College London, Tyler Sorensen University of California at Santa Cruz, John Wickerson Imperial College London
Link to publication DOI Authorizer link Pre-print
14:30
20m
Talk
(PLDI 2020) Efficient Handling of String-Number Conversion
SIGPLAN Track
Parosh Aziz Abdulla Uppsala University, Sweden, Mohamed Faouzi Atig Uppsala University, Sweden, Yu-Fang Chen Academia Sinica, Taiwan, Bui Phi Diep Uppsala University, Sweden, Julian Dolby IBM Research, USA, Petr Janků Brno University of Technology, Czechia, Hsin-Hung Lin Academia Sinica, Taiwan, Lukáš Holík Brno University of Technology, Wei-Cheng Wu University of Southern California, USA
13:30 - 14:50
Verification & OptimizationPLDI at Toucan +12h
Chair(s): Charith Mendis University of Illinois at Urbana-Champaign
13:30
20m
Talk
Efficient Approximations for Cache-conscious Data Placementvirtual
PLDI
Ali Ahmadi Sharif University of Technology, Majid Daliri University of Tehran, Amir Kafshdar Goharshady Hong Kong University of Science and Technology, Andreas Pavlogiannis Aarhus University
DOI
13:50
20m
Talk
FreeTensor: A Free-form DSL with Holistic Optimizations for Irregular Tensor Programsvirtual
PLDI
Shizhi Tang Tsinghua University, Jidong Zhai Tsinghua University, Haojie Wang , Lin Jiang Tsinghua University, Liyan Zheng Tsinghua University, Zhenhao Yuan Tsinghua University, Chen Zhang Tsinghua University
DOI Pre-print
14:10
20m
Talk
Lasagne: A Static Binary Translator for Weak Memory Model Architecturesvirtual
PLDI
Rodrigo C. O. Rocha University of Edinburgh, UK, Dennis Sprokholt TU Delft, Martin Fink TU Munich, Redha Gouicem TU Munich, Tom Spink University of St Andrews, Soham Chakraborty TU Delft, Pramod Bhatotia TU Munich / University of Edinburgh
DOI
14:30
20m
Talk
Verifying Optimizations of Concurrent Programs in the Promising Semanticsvirtual
PLDI
Junpeng Zha Nanjing University, Hongjin Liang Nanjing University, Xinyu Feng Nanjing University
DOI Pre-print
14:50 - 15:30
PL Tea (Fri PM)PLDI at Boardroom
14:50
40m
Social Event
PL Teasocial
PLDI
Rachit Nigam Cornell University
15:30 - 16:50
RewritingSIGPLAN Track at Cockatoo
Chair(s): Chandrakana Nandi Certora, inc.
15:30
20m
Talk
(ICFP 2020) Achieving high-performance the functional way: a functional pearl on expressing high-performance optimizations as rewrite strategies
SIGPLAN Track
Bastian Hagedorn NVIDIA, Johannes Lenfers University of Münster, Thomas Koehler University of Glasgow, Xueying Qin University of Glasgow, United Kingdom, Sergei Gorlatch University of Münster, Germany, Michel Steuwer University of Edinburgh
Link to publication DOI Authorizer link Pre-print
15:50
20m
Talk
(PLDI 2020) Optimizing Homomorphic Evaluation Circuits by Program Synthesis and Term Rewriting
SIGPLAN Track
DongKwon Lee Seoul National University, South Korea, Woosuk Lee Hanyang University, Hakjoo Oh Korea University, Kwangkeun Yi Seoul National University
16:10
20m
Talk
(ICFP 2021) Grafs: Declarative Graph Analytics
SIGPLAN Track
Farzin Houshmand University of California, Riverside, Mohsen Lesani University of California at Riverside, Keval Vora Simon Fraser University
16:30
20m
Talk
(POPL 2022) Verified Tensor-Program Optimization Via High-level Scheduling Rewrites
SIGPLAN Track
Amanda Liu Massachusetts Institute of Technology, Gilbert Bernstein University of California at Berkeley, Adam Chlipala MIT CSAIL, Jonathan Ragan-Kelley MIT
15:30 - 16:50
Verification IIPLDI at Kon-Tiki +12h
Chair(s): Thomas Wahl GrammaTech, Inc.
15:30
20m
Talk
Relational Compilation for Performance-Critical Applications
PLDI
Clément Pit-Claudel EPFL, AWS, Jade Philipoom MIT CSAIL, Dustin Jamner MIT CSAIL, Andres Erbsen MIT CSAIL, Adam Chlipala MIT CSAIL
Link to publication DOI Pre-print
15:50
20m
Talk
Formally Verified Lifting of C-compiled x86-64 Binaries
PLDI
Freek Verbeek Open University of The Netherlands & Virginia Tech, Joshua A. Bockenek Virginia Tech, Zhoulai Fu University of California, Davis, Binoy Ravindran Virginia Tech
DOI
16:10
20m
Talk
Leapfrog: Certified Equivalence for Protocol Parsers
PLDI
Ryan Doenges Cornell University, Tobias Kappé ILLC, University of Amsterdam, John Sarracino Cornell University, Nate Foster Cornell University, Greg Morrisett Cornell Tech
DOI Pre-print
16:30
20m
Talk
Computing Correctly with Inductive Relations
PLDI
Zoe Paraskevopoulou Northeastern University, Aaron Eline University of Maryland, Leonidas Lampropoulos University of Maryland
DOI
15:30 - 16:50
Refinement TypesSIGPLAN Track at Macaw
Chair(s): Sorav Bansal IIT Delhi and CompilerAI Labs
15:30
20m
Talk
(OOPSLA 2020) Verifying Replicated Data Types with Typeclass Refinements in Liquid Haskell
SIGPLAN Track
Yiyun Liu University of Maryland at College Park, James Parker Galois, Inc., Patrick Redmond University of California at Santa Cruz, Lindsey Kuper University of California at Santa Cruz, Michael Hicks University of Maryland at College Park, Niki Vazou IMDEA Software Institute
15:50
20m
Talk
(PLDI 2021) RefinedC: Automating the Foundational Verification of C Code with Refined Ownership Types
SIGPLAN Track
Michael Sammler MPI-SWS, Rodolphe Lepigre MPI-SWS, Robbert Krebbers Radboud University Nijmegen, Kayvan Memarian University of Cambridge, Derek Dreyer MPI-SWS, Deepak Garg MPI-SWS
Link to publication DOI Authorizer link Pre-print
16:10
20m
Talk
(POPL 2021) Data Flow Refinement Type Inference
SIGPLAN Track
Zvonimir Pavlinovic Google, USA, Yusen Su University of Waterloo, Thomas Wies New York University
16:30
20m
Talk
(PLDI 2021) RbSyn: type- and effect-guided program synthesis
SIGPLAN Track
Sankha Narayan Guria University of Maryland, College Park, Jeffrey S. Foster Tufts University, David Van Horn University of Maryland
Link to publication DOI Authorizer link Pre-print
15:30 - 16:50
Testing & SynthesisPLDI at Toucan +12h
Chair(s): Caroline Lemieux University of British Columbia
15:30
20m
Talk
Interpreter-guided Differential JIT Compiler Unit Testingvirtual
PLDI
Guillermo Polito Univ. Lille, CNRS, Inria, Centrale Lille, UMR 9189 CRIStAL, Pharo Consortium, Stéphane Ducasse Inria, Pablo Tesone Univ. Lille, Inria, CNRS, Centrale Lille, UMR 9189 CRIStAL, Pharo Consortium
DOI
15:50
20m
Talk
Landmarks and Regions: A Robust Approach to Data Extractionvirtual
PLDI
Suresh Parthasarathy Microsoft Research, Lincy Pattanaik Microsoft Research, Anirudh Khatry Microsoft Research, Arun Iyer Microsoft Research, Arjun Radhakrishna Microsoft, Sriram Rajamani Microsoft Research, Mohammad Raza Microsoft
DOI
16:10
20m
Talk
Odin: On-Demand Instrumentation with On-the-Fly Recompilationvirtual
PLDI
Mingzhe Wang Tsinghua University, Jie Liang Tsinghua University, Chijin Zhou Tsinghua University, Zhiyong Wu Tsinghua University, Xinyi Xu Tsinghua University, Yu Jiang Tsinghua University
DOI
16:30
20m
Talk
Quickstrom: Property-based acceptance testing with LTL specificationsvirtual
PLDI
Liam O'Connor University of Edinburgh, Oskar Wickström Monoid Consulting
DOI
21:00 - 22:00
Business MeetingPLDI at Kon-Tiki
21:00
60m
Meeting
Business Meeting
PLDI
Işıl Dillig University of Texas at Austin, Ranjit Jhala University of California at San Diego; Amazon Web Services, Steve Blackburn Google and Australian National University
21:00 - 21:30
PLTea Virtual Friday 1PLDI at PLTea (Virtual see event for Zoom)
21:00
30m
Social Event
PL Teasocial
PLDI
Rachit Nigam Cornell University
22:40 - 00:00
Hardware IPLDI at Kon-Tiki
22:40
20m
Talk
Bind the Gap: Compiling Real Software to Hardware FFT Accelerators
PLDI
Jackson Woodruff University of Edinburgh, Jordi Armengol-Estapé University of Edinburgh, Sam Ainsworth University of Edinburgh, UK, Michael F. P. O'Boyle University of Edinburgh
DOI
23:00
20m
Talk
Exocompilation for Productive Programming of Hardware Accelerators
PLDI
Yuka Ikarashi MIT, Gilbert Bernstein University of California at Berkeley, Alex Reinking UC Berkeley, Hasan Genc UC Berkeley, Jonathan Ragan-Kelley MIT
DOI
23:20
20m
Talk
PDL: A High-Level Hardware Design Language for Pipelined Processors
PLDI
Drew Zagieboylo Cornell University, Charles Sherk Cornell University, G. Edward Suh Cornell University / Facebook, Andrew Myers Cornell University
DOI
23:40
20m
Talk
WARio: Efficient Code Generation for Intermittent Computing
PLDI
Vito Kortbeek Delft University of Technology, Souradip Ghosh Carnegie Mellon University, Josiah Hester Northwestern University, Simone Campanoni Northwestern University, USA, Przemysław Pawełczak Delft University of Technology
DOI Pre-print
22:40 - 00:00
Hardware IIPLDI at Toucan
22:40
20m
Talk
Software-Hardware Codesign for Efficient In-Memory Regular Pattern Matchingvirtual
PLDI
Konstantinos Mamouras Rice University, Kaiyuan Yang Rice University, Lingkun Kong Rice University, Qixuan Yu Rice University, Agnishom Chattopadhyay Rice University, Alexis Le Glaunec Rice University, Yi Huang Rice University
Link to publication DOI

Sat 18 Jun

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

01:30 - 02:50
Verification IPLDI at Kon-Tiki
01:30
20m
Talk
Compass: Strong and Compositional Library Specifications in Relaxed Memory Separation Logic
PLDI
Hoang-Hai Dang MPI-SWS, Jaehwang Jung KAIST, South Korea, Jaemin Choi KAIST, Duc-Than Nguyen University of Illinois at Chicago, William Mansky University of Illinois at Chicago, Jeehoon Kang KAIST, Derek Dreyer MPI-SWS
DOI
01:50
20m
Talk
Diaframe: Automated Verification of Fine-Grained Concurrent Programs in Iris
PLDI
Ike Mulder Radboud University Nijmegen, Robbert Krebbers Radboud University Nijmegen, Herman Geuvers Radboud University Nijmegen, Netherlands
Link to publication DOI Pre-print
02:10
20m
Talk
Islaris: Verification of Machine Code Against Authoritative ISA Semantics
PLDI
Michael Sammler MPI-SWS, Angus Hammond University of Cambridge, Rodolphe Lepigre MPI-SWS, Brian Campbell University of Edinburgh, Jean Pichon-Pharabod Aarhus University, Derek Dreyer MPI-SWS, Deepak Garg MPI-SWS, Peter Sewell University of Cambridge
DOI
02:30
20m
Talk
RustHornBelt: A Semantic Foundation for Functional Verification of Rust Programs with Unsafe CodeDistinguished Paper Award
PLDI
Yusuke Matsushita The University of Tokyo, Xavier Denis Université Paris-Saclay, CNRS, ENS Paris-Saclay, INRIA, Laboratoire Méthodes Formelles, Jacques-Henri Jourdan Université Paris-Saclay, CNRS, ENS Paris-Saclay, Laboratoire Méthodes Formelles, Derek Dreyer MPI-SWS
DOI
01:30 - 02:50
Verification & OptimizationPLDI at Toucan
01:30
20m
Talk
Efficient Approximations for Cache-conscious Data Placementvirtual
PLDI
Ali Ahmadi Sharif University of Technology, Majid Daliri University of Tehran, Amir Kafshdar Goharshady Hong Kong University of Science and Technology, Andreas Pavlogiannis Aarhus University
DOI
01:50
20m
Talk
FreeTensor: A Free-form DSL with Holistic Optimizations for Irregular Tensor Programsvirtual
PLDI
Shizhi Tang Tsinghua University, Jidong Zhai Tsinghua University, Haojie Wang , Lin Jiang Tsinghua University, Liyan Zheng Tsinghua University, Zhenhao Yuan Tsinghua University, Chen Zhang Tsinghua University
DOI Pre-print
02:10
20m
Talk
Lasagne: A Static Binary Translator for Weak Memory Model Architecturesvirtual
PLDI
Rodrigo C. O. Rocha University of Edinburgh, UK, Dennis Sprokholt TU Delft, Martin Fink TU Munich, Redha Gouicem TU Munich, Tom Spink University of St Andrews, Soham Chakraborty TU Delft, Pramod Bhatotia TU Munich / University of Edinburgh
DOI
02:30
20m
Talk
Verifying Optimizations of Concurrent Programs in the Promising Semanticsvirtual
PLDI
Junpeng Zha Nanjing University, Hongjin Liang Nanjing University, Xinyu Feng Nanjing University
DOI Pre-print
02:30 - 03:00
02:30
30m
Social Event
PL Teasocial
PLDI
Rachit Nigam Cornell University
03:30 - 04:50
Verification IIPLDI at Kon-Tiki
03:30
20m
Talk
Relational Compilation for Performance-Critical Applications
PLDI
Clément Pit-Claudel EPFL, AWS, Jade Philipoom MIT CSAIL, Dustin Jamner MIT CSAIL, Andres Erbsen MIT CSAIL, Adam Chlipala MIT CSAIL
Link to publication DOI Pre-print
03:50
20m
Talk
Formally Verified Lifting of C-compiled x86-64 Binaries
PLDI
Freek Verbeek Open University of The Netherlands & Virginia Tech, Joshua A. Bockenek Virginia Tech, Zhoulai Fu University of California, Davis, Binoy Ravindran Virginia Tech
DOI
04:10
20m
Talk
Leapfrog: Certified Equivalence for Protocol Parsers
PLDI
Ryan Doenges Cornell University, Tobias Kappé ILLC, University of Amsterdam, John Sarracino Cornell University, Nate Foster Cornell University, Greg Morrisett Cornell Tech
DOI Pre-print
04:30
20m
Talk
Computing Correctly with Inductive Relations
PLDI
Zoe Paraskevopoulou Northeastern University, Aaron Eline University of Maryland, Leonidas Lampropoulos University of Maryland
DOI
03:30 - 04:50
Testing & SynthesisPLDI at Toucan
03:30
20m
Talk
Interpreter-guided Differential JIT Compiler Unit Testingvirtual
PLDI
Guillermo Polito Univ. Lille, CNRS, Inria, Centrale Lille, UMR 9189 CRIStAL, Pharo Consortium, Stéphane Ducasse Inria, Pablo Tesone Univ. Lille, Inria, CNRS, Centrale Lille, UMR 9189 CRIStAL, Pharo Consortium
DOI
03:50
20m
Talk
Landmarks and Regions: A Robust Approach to Data Extractionvirtual
PLDI
Suresh Parthasarathy Microsoft Research, Lincy Pattanaik Microsoft Research, Anirudh Khatry Microsoft Research, Arun Iyer Microsoft Research, Arjun Radhakrishna Microsoft, Sriram Rajamani Microsoft Research, Mohammad Raza Microsoft
DOI
04:10
20m
Talk
Odin: On-Demand Instrumentation with On-the-Fly Recompilationvirtual
PLDI
Mingzhe Wang Tsinghua University, Jie Liang Tsinghua University, Chijin Zhou Tsinghua University, Zhiyong Wu Tsinghua University, Xinyi Xu Tsinghua University, Yu Jiang Tsinghua University
DOI
04:30
20m
Talk
Quickstrom: Property-based acceptance testing with LTL specificationsvirtual
PLDI
Liam O'Connor University of Edinburgh, Oskar Wickström Monoid Consulting
DOI