Sparse 2024
Mon 24 - Fri 28 June 2024 Copenhagen, Denmark
co-located with PLDI 2024
PLDI 2024 (series) / Sparse 2024 (series) / Radisson Blu Scandinavia, Copenhagen /

Room information: Finland / Norway

VenueRadisson Blu Scandinavia, Copenhagen
Room nameFinland / Norway
Room InformationNo extra information available
Program

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

Wed 26 Jun

Displayed time zone: Windhoek change

10:40 - 12:20
Probabilistic ProgrammingPLDI Research Papers at Finland / Norway
Chair(s): Jeremy G. Siek Indiana University, USA
10:40
20m
Talk
Bit Blasting Probabilistic Programs
PLDI Research Papers
Poorva Garg University of California, Los Angeles, Steven Holtzen Northeastern University, Guy Van den Broeck University of California at Los Angeles, Todd Millstein University of California at Los Angeles
DOI
11:00
20m
Talk
Compiling Probabilistic Programs for Variable Elimination with Information Flow
PLDI Research Papers
Jianlin Li University of Waterloo, Eric Wang University of Waterloo, Yizhou Zhang University of Waterloo
DOI
11:20
20m
Talk
Equivalence and Similarity Refutation for Probabilistic Programs
PLDI Research Papers
Krishnendu Chatterjee IST Austria, Ehsan Kafshdar Goharshady IST Austria, Petr Novotný Masaryk University, Đorđe Žikelić Singapore Management University, Singapore
DOI
11:40
20m
Talk
GenSQL: A Probabilistic Programming System for Querying Generative Models of Database Tables
PLDI Research Papers
Mathieu Huot MIT, Matin Ghavami Massachusetts Institute of Technology, Alexander K. Lew Massachusetts Institute of Technology, Ulrich Schaechtle Digital Garage, Cameron Freer Massachusetts Institute of Technology, Zane Shelby Digital Garage, Martin Rinard MIT, Feras Saad Carnegie Mellon University, Vikash K. Mansinghka Massachusetts Institute of Technology
DOI
12:00
20m
Talk
Probabilistic Programming with Programmable Variational Inference
PLDI Research Papers
McCoy Reynolds Becker MIT, Alexander K. Lew Massachusetts Institute of Technology, Xiaoyan Wang Massachusetts Institute of Technology, Matin Ghavami Massachusetts Institute of Technology, Mathieu Huot MIT, Martin Rinard MIT, Vikash K. Mansinghka Massachusetts Institute of Technology
DOI
13:40 - 15:20
Pot Pourri 1PLDI Research Papers at Finland / Norway
Chair(s): Steve Blackburn Google and Australian National University
13:40
20m
Talk
Static Posterior Inference of Bayesian Probabilistic Programming via Polynomial Solving
PLDI Research Papers
Peixin Wang University of Oxford, Tengshun Yang SKLCS, Institute of Software, Chinese Academy of Sciences & University of Chinese Academy of Sciences, Hongfei Fu Shanghai Jiao Tong University, Guanyan Li University of Oxford, C.-H. Luke Ong NTU
DOI
14:00
20m
Talk
Consolidating Smart Contracts with Behavioral Contracts
PLDI Research Papers
Guannan Wei Purdue University, Danning Xie Purdue University, Wuqi Zhang The Hong Kong University of Science and Technology, Yongwei Yuan Purdue University, Zhuo Zhang Purdue University
DOI
14:20
20m
Talk
NetBlocks: Staging Layouts for High-Performance Custom Host Network Stacks
PLDI Research Papers
Ajay Brahmakshatriya Massachusetts Institute of Technology, Christopher Rinard Massachusetts Institute of Technology, Manya Ghobadi Massachusetts Institute of Technology, Saman Amarasinghe Massachusetts Institute of Technology
DOI
14:40
20m
Talk
KATch: A Fast Symbolic Verifier for NetKAT
PLDI Research Papers
Mark Moeller Cornell University, Jules Jacobs Cornell University, Olivier Savary Bélanger Galois, Inc., David Darais Galois, Cole Schlesinger Galois, Steffen Smolka Google, Nate Foster Cornell University and Jane Street, Alexandra Silva Cornell University
DOI
16:00 - 17:20
Security and CryptographyPLDI Research Papers at Finland / Norway
Chair(s): Klaus v. Gleissenthall Vrije Universiteit Amsterdam, Netherlands
16:00
20m
Talk
A Tensor Compiler with Automatic Data Packing for Simple and Efficient Fully Homomorphic Encryption
PLDI Research Papers
Nikola Samardzic Massachusetts Institute of Technology, Aleksandar Krastev Massachusetts Institute of Technology, Simon Langowski Massachusetts Institute of Technology, Srinivas Devadas Massachusetts Institute of Technology, Daniel Sanchez MIT
DOI
16:20
20m
Talk
Quantitative Robustness for Vulnerability Assessment
PLDI Research Papers
Guillaume Girol CEA, List, Université Paris Saclay, Guilhem Lacombe CEA LIST and Université Paris-Saclay, Sébastien Bardin CEA LIST, University Paris-Saclay
DOI
16:40
20m
Talk
Quest Complete: The Holy Grail of Gradual Security
PLDI Research Papers
Tianyu Chen Indiana University, Jeremy G. Siek Indiana University, USA
DOI Pre-print
17:00
20m
Talk
Foundational Integration Verification of a Cryptographic Server
PLDI Research Papers
Andres Erbsen Google, Jade Philipoom Google, Germany, Dustin Jamner MIT CSAIL, Ashley Lin Massachusetts Institute of Technology, Samuel Gruetter Massachusetts Institute of Technology, Clément Pit-Claudel EPFL, Adam Chlipala Massachusetts Institute of Technology
DOI

Thu 27 Jun

Displayed time zone: Windhoek change

10:40 - 12:20
Formally VerifiedPLDI Research Papers at Finland / Norway
Chair(s): Peter Müller ETH Zurich
10:40
20m
Talk
The Functional Essence of Imperative Binary Search Trees
PLDI Research Papers
Anton Lorenzen University of Edinburgh, Daan Leijen Microsoft Research, Wouter Swierstra Utrecht University, Netherlands, Sam Lindley University of Edinburgh
DOI Pre-print
11:00
20m
Talk
Quiver: Guided Abductive Inference of Separation Logic Specifications in Coq
PLDI Research Papers
Simon Spies MPI-SWS, Lennard Gäher MPI-SWS, Michael Sammler MPI-SWS, Derek Dreyer MPI-SWS
DOI Pre-print
11:20
20m
Talk
Maximum Consensus Floating Point Solutions for Infeasible Low-Dimensional Linear Programs with Convex Hull as the Intermediate Representation
PLDI Research Papers
Mridul Aanjaneya Rutgers University, Santosh Nagarakatte Rutgers University
DOI Pre-print
11:40
20m
Talk
Live Verification in an Interactive Proof Assistant
PLDI Research Papers
Samuel Gruetter Massachusetts Institute of Technology, Viktor Fukala Massachusetts Institute of Technology, Adam Chlipala Massachusetts Institute of Technology
DOI
12:00
20m
Talk
Predictable Verification using Intrinsic Definitions
PLDI Research Papers
Adithya Murali University of Illinois at Urbana-Champaign, Cody Rivera University of Illinois at Urbana-Champaign, P. Madhusudan University of Illinois at Urbana-Champaign
DOI
13:40 - 14:40
Formal Verification 2PLDI Research Papers at Finland / Norway
Chair(s): Clément Pit-Claudel EPFL
13:40
20m
Talk
Mechanised Hypersafety Proofs about Structured Data
PLDI Research Papers
Vladimir Gladshtein National University of Singapore, Qiyuan Zhao National University of Singapore, Willow Ahrens Massachusetts Institute of Technology, Saman Amarasinghe Massachusetts Institute of Technology, Ilya Sergey National University of Singapore
DOI Pre-print
14:00
20m
Talk
Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties
PLDI Research Papers
Thibault Dardinier ETH Zurich, Peter Müller ETH Zurich
DOI
14:20
20m
Talk
A HAT Trick: Automatically Verifying Representation Invariants using Symbolic Finite Automata
PLDI Research Papers
Zhe Zhou Purdue University, Qianchuan Ye Purdue University, Benjamin Delaware Purdue University, Suresh Jagannathan Purdue University
DOI
15:20 - 17:00
FinalsPLDI SRC at Finland / Norway
15:20
1h40m
Other
SRC Finals
PLDI SRC

Fri 28 Jun

Displayed time zone: Windhoek change

10:40 - 12:20
SynthesisPLDI Research Papers at Finland / Norway
10:40
20m
Talk
From Batch to Stream: Automatic Generation of Online Algorithms
PLDI Research Papers
Ziteng Wang University of Texas at Austin, Shankara Pailoor University of Texas at Austin, Aaryan Prakash University of Texas at Austin, Yuepeng Wang Simon Fraser University, Işıl Dillig University of Texas at Austin
DOI
11:00
20m
Talk
[TOPLAS] Decomposition-Based Synthesis for Applying D&C-Like Algorithmic Paradigms
PLDI Research Papers
Ruyi Ji Peking University, Yuwei Zhao Peking University, Yingfei Xiong Peking University, Di Wang Peking University, Lu Zhang Peking University, Zhenjiang Hu Peking University
11:20
20m
Talk
Superfusion: Eliminating Intermediate Data Structures via Inductive Synthesis
PLDI Research Papers
Ruyi Ji Peking University, Yuwei Zhao Peking University, Nadia Polikarpova University of California at San Diego, Yingfei Xiong Peking University, Zhenjiang Hu Peking University
DOI
11:40
20m
Talk
Recursive Program Synthesis using ParamorphismsRemote
PLDI Research Papers
Qiantan Hong Stanford University, Alex Aiken Stanford University
DOI
12:00
20m
Talk
Reward-Guided Synthesis of Intelligent Agents with Control StructuresRemote
PLDI Research Papers
Guofeng Cui Rutgers University, Yuning Wang Rutgers University, Wenjie Qiu Rutgers University, He Zhu Rutgers University, USA
DOI
13:40 - 15:20
Pot Pourri 2PLDI Research Papers at Finland / Norway
Chair(s): Caleb Stanford University of California, Davis
13:40
20m
Talk
Falcon: A Fused Approach to Path-Sensitive Sparse Data Dependence Analysis
PLDI Research Papers
Peisen Yao Zhejiang University, Jinguo Zhou Ant Group, Xiao Xiao Ant Group, Qingkai Shi Nanjing University, Rongxin Wu School of Informatics, Xiamen University, Charles Zhang The Hong Kong University of Science and Technology
DOI
14:00
20m
Talk
A Proof Recipe for Linearizability in Relaxed Memory Separation Logic
PLDI Research Papers
Sunho Park KAIST, Jaewoo Kim KAIST, Ike Mulder Radboud University Nijmegen, Jaehwang Jung KAIST, Janggun Lee KAIST, Robbert Krebbers Radboud University Nijmegen, Jeehoon Kang KAIST
DOI
14:20
20m
Talk
Compositional Semantics for Shared-Variable Concurrency
PLDI Research Papers
Mikhail Svyatlovskiy Tel Aviv University, Shai Mermelstein Tel Aviv University, Ori Lahav Tel Aviv University
DOI
14:40
20m
Talk
Input-Relational Verification of Deep Neural Networks
PLDI Research Papers
Debangshu Banerjee University of Illinois at Urbana-Champaign, Changming Xu University of Illinois at Urbana-Champaign, Gagandeep Singh University of Illinois at Urbana-Champaign
DOI
15:00
20m
Talk
Automated Verification of Fundamental Algebraic Laws
PLDI Research Papers
George Zakhour University of St. Gallen, Pascal Weisenburger University of St. Gallen, Guido Salvaneschi University of St. Gallen
DOI

Wed 26 Jun

Displayed time zone: Windhoek change

Room9:003010:003011:003012:003013:003014:003015:003016:003017:0030
Finland / Norway

PLDI Research Papers

PLDI Research Papers

Probabilistic Programming

PLDI Research Papers

Pot Pourri 1

PLDI Research Papers

Security and Cryptography

Thu 27 Jun

Displayed time zone: Windhoek change

Room9:003010:003011:003012:003013:003014:003015:003016:0030
Finland / Norway

PLDI Research Papers

PLDI Research Papers

Formally Verified

PLDI Research Papers

Formal Verification 2

PLDI SRC

Finals

Fri 28 Jun

Displayed time zone: Windhoek change

Room9:003010:003011:003012:003013:003014:003015:0030
Finland / Norway

PLDI Research Papers

PLDI Research Papers

Synthesis

PLDI Research Papers

Pot Pourri 2

Wed 26 Jun

Displayed time zone: Windhoek change

Room10:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:00153045
Finland / Norway
PLDI Research Papers
Bit Blasting Probabilistic Programs
10:40 - 11:00
PLDI Research Papers
Compiling Probabilistic Programs for Variable Elimination with Informat ...
11:00 - 11:20
PLDI Research Papers
Equivalence and Similarity Refutation for Probabilistic Programs
11:20 - 11:40
PLDI Research Papers
GenSQL: A Probabilistic Programming System for Querying Generative Mode ...
11:40 - 12:00
PLDI Research Papers
Probabilistic Programming with Programmable Variational Inference
12:00 - 12:20
PLDI Research Papers
Static Posterior Inference of Bayesian Probabilistic Programming via Po ...
13:40 - 14:00
PLDI Research Papers
Consolidating Smart Contracts with Behavioral Contracts
14:00 - 14:20
PLDI Research Papers
NetBlocks: Staging Layouts for High-Performance Custom Host Network Stacks
14:20 - 14:40
PLDI Research Papers
KATch: A Fast Symbolic Verifier for NetKAT
14:40 - 15:00
PLDI Research Papers
A Tensor Compiler with Automatic Data Packing for Simple and Efficient ...
16:00 - 16:20
PLDI Research Papers
Quantitative Robustness for Vulnerability Assessment
16:20 - 16:40
PLDI Research Papers
Quest Complete: The Holy Grail of Gradual Security
16:40 - 17:00
PLDI Research Papers
Foundational Integration Verification of a Cryptographic Server
17:00 - 17:20

Thu 27 Jun

Displayed time zone: Windhoek change

Room10:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:00153045
Finland / Norway
PLDI Research Papers
The Functional Essence of Imperative Binary Search Trees
10:40 - 11:00
PLDI Research Papers
Quiver: Guided Abductive Inference of Separation Logic Specifications i ...
11:00 - 11:20
PLDI Research Papers
Maximum Consensus Floating Point Solutions for Infeasible Low-Dimension ...
11:20 - 11:40
PLDI Research Papers
Live Verification in an Interactive Proof Assistant
11:40 - 12:00
PLDI Research Papers
Predictable Verification using Intrinsic Definitions
12:00 - 12:20
PLDI Research Papers
Mechanised Hypersafety Proofs about Structured Data
13:40 - 14:00
PLDI Research Papers
Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties
14:00 - 14:20
PLDI Research Papers
A HAT Trick: Automatically Verifying Representation Invariants using Sy ...
14:20 - 14:40
PLDI SRC
SRC Finals
15:20 - 17:00

Fri 28 Jun

Displayed time zone: Windhoek change

Room10:0015304511:0015304512:0015304513:0015304514:0015304515:00153045
Finland / Norway
PLDI Research Papers
From Batch to Stream: Automatic Generation of Online Algorithms
10:40 - 11:00
PLDI Research Papers
[TOPLAS] Decomposition-Based Synthesis for Applying D&C-Like Algorithmi ...
11:00 - 11:20
PLDI Research Papers
Superfusion: Eliminating Intermediate Data Structures via Inductive Syn ...
11:20 - 11:40
PLDI Research PapersRemote
Recursive Program Synthesis using Paramorphisms
11:40 - 12:00
PLDI Research PapersRemote
Reward-Guided Synthesis of Intelligent Agents with Control Structures
12:00 - 12:20
PLDI Research Papers
Falcon: A Fused Approach to Path-Sensitive Sparse Data Dependence Analysis
13:40 - 14:00
PLDI Research Papers
A Proof Recipe for Linearizability in Relaxed Memory Separation Logic
14:00 - 14:20
PLDI Research Papers
Compositional Semantics for Shared-Variable Concurrency
14:20 - 14:40
PLDI Research Papers
Input-Relational Verification of Deep Neural Networks
14:40 - 15:00
PLDI Research Papers
Automated Verification of Fundamental Algebraic Laws
15:00 - 15:20