SPLASH 2022
Mon 5 - Sat 10 December 2022 Auckland, New Zealand

SPLASH 2022 features keynotes by recognized experts in the field. This year we are honoured to have the following four in person keynote speakers who will travel to Auckland and deliver exciting talks:

Keynote Talks

Title
(I Can't Get No) VerificationKeynote
Keynotes
DOI
Improving the Quality of Creative Practices with Pattern LanguagesKeynote
Keynotes
DOI
Myths and Mythconceptions: What does it mean to be a programming language, anyhow?Keynote
Keynotes
DOI
The State Of Debugging in 2022KeynoteSupported by Google
Keynotes
DOI
Dates
Tracks
Plenary
You're viewing the program in a time zone which is different from your device's time zone change time zone

Thu 8 Dec

Displayed time zone: Auckland, Wellington change

09:00 - 10:00
SPLASH KeynoteKeynotes at AMRF Auditorium
Chair(s): Robert Biddle Carleton University
09:00
60m
Keynote
Myths and Mythconceptions: What does it mean to be a programming language, anyhow?Keynote
Keynotes
K: Mary Shaw Carnegie Mellon University
DOI
10:00 - 10:30
10:00
30m
Coffee break
Coffee break
Catering and Social Events

10:30 - 12:00
RuntimeOOPSLA at AMRF Auditorium
Chair(s): Stefan Marr University of Kent
10:30
30m
Talk
A Fast In-Place Interpreter for WebAssemblyDistinguished Paper
OOPSLA
Ben L. Titzer Carnegie Mellon University
DOI
11:00
30m
Talk
Optimal Heap Limits for Reducing Browser Memory Use
OOPSLA
Marisa Kirisame University of Utah, Pranav Shenoy University of Utah, Pavel Panchekha University of Utah
DOI
11:30
30m
Talk
The Road Not Taken: Exploring Alias Analysis Based Optimizations Missed by the Compiler
OOPSLA
Khushboo Chitre IIIT Delhi, Piyus Kedia IIIT Delhi, Rahul Purandare IIIT Delhi
DOI
10:30 - 12:00
Synthesis IOOPSLA at Lecture Theatre 2
Chair(s): Hakjoo Oh Korea University
10:30
30m
Research paper
Complexity-guided container replacement synthesisDistinguished Paper
OOPSLA
Chengpeng Wang Hong Kong University of Science and Technology, Peisen Yao Hong Kong University of Science and Technology, Wensheng Tang Hong Kong University of Science and Technology, Qingkai Shi Ant Group, Charles Zhang Hong Kong University of Science and Technology
DOI
11:00
30m
Talk
Katara: Synthesizing CRDTs with Verified Lifting
OOPSLA
Shadaj Laddad University of California at Berkeley, Conor Power University of California at Berkeley, Mae Milano University of California at Berkeley, Alvin Cheung University of California at Berkeley, Joseph M. Hellerstein University of California at Berkeley
DOI
11:30
30m
Talk
Specification-Guided Component-Based Synthesis from Effectful Libraries
OOPSLA
Ashish Mishra Purdue University, Suresh Jagannathan Purdue University
DOI
10:30 - 12:00
AssuranceOOPSLA at Seminar Room G007
Chair(s): Amal Ahmed Northeastern University, USA
10:30
30m
Research paper
C to checked C by 3cDistinguished Paper
OOPSLA
Aravind Machiry Purdue University, John Kastner Amazon, Matt McCutchen , Aaron Eline Amazon, Kyle Headley Amazon, MIchael Hicks Amazon
DOI
11:00
30m
Talk
Solo: A Lightweight Static Analysis for Differential Privacy
OOPSLA
Chike Abuah University of Vermont, David Darais Galois, Joseph P. Near University of Vermont
DOI
11:30
30m
Talk
MLstruct: Principal Type Inference in a Boolean Algebra of Structural Types
OOPSLA
Lionel Parreaux Hong Kong University of Science and Technology, Chun Yin Chau The Hong Kong University of Science and Technology
DOI Pre-print Media Attached File Attached
12:00 - 13:30
12:00
90m
Lunch
Lunch
Catering and Social Events

14:00 - 15:00
SPLASH KeynoteKeynotes at AMRF Auditorium
Chair(s): Jonathan Aldrich Carnegie Mellon University
14:00
60m
Keynote
The State Of Debugging in 2022KeynoteSupported by Google
Keynotes
K: Robert O'Callahan Google Research
DOI
15:00 - 15:30
15:00
30m
Coffee break
Coffee break
Catering and Social Events

15:30 - 17:00
TypesOOPSLA at AMRF Auditorium
Chair(s): Zhong Shao Yale University
15:30
30m
Talk
A Bunch of Sessions: A Propositions-as-Sessions Interpretation of Bunched Implications in Channel-Based Concurrency
OOPSLA
Daniel Frumin University of Groningen, Emanuele D’Osualdo MPI-SWS, Bas van den Heuvel University of Groningen, Jorge A. Pérez University of Groningen
DOI Pre-print
16:00
30m
Talk
A case for DOT: Theoretical Foundations for Objects with Pattern Matching and GADT-Style Reasoning
OOPSLA
Aleksander Boruch-Gruszecki EPFL, Radosław Waśko University of Warsaw, Yichen Xu Beijing University of Posts and Telecommunications, Lionel Parreaux Hong Kong University of Science and Technology
DOI
16:30
30m
Talk
Coeffects for Sharing and Mutation
OOPSLA
Riccardo Bianchini University of Genoa, Francesco Dagnino University of Genoa, Paola Giannini University of Eastern Piedmont, Elena Zucca University of Genoa, Marco Servetto Victoria University of Wellington
DOI
15:30 - 17:00
CompileOOPSLA at Lecture Theatre 2
Chair(s): Stefan Marr University of Kent
15:30
30m
Talk
Compilation of Dynamic Sparse Tensor Algebra
OOPSLA
Stephen Chou Massachusetts Institute of Technology, Saman Amarasinghe Massachusetts Institute of Technology
DOI
16:00
30m
Talk
Incremental Type-Checking for Free: Using Scope Graphs to Derive Incremental Type-Checkers
OOPSLA
Aron Zwaan Delft University of Technology, Hendrik van Antwerpen Delft University of Technology, Eelco Visser Delft University of Technology
DOI
16:30
30m
Talk
UniRec: A Unimodular-Like Framework for Nested Recursions and Loops
OOPSLA
Kirshanthan Sundararajah Purdue University, Charitha Saumya Purdue University, Milind Kulkarni Purdue University
DOI
15:30 - 17:00
VerificationOOPSLA at Seminar Room G007
Chair(s): Dominique Devriese KU Leuven
15:30
30m
Talk
Checking Equivalence in a Non-strict Language
OOPSLA
John C. Kolesar Yale University, Ruzica Piskac Yale University, William T. Hallahan Yale University
DOI
16:00
30m
Talk
Necessity Specifications for Robustness
OOPSLA
Julian Mackay Victoria University of Wellington, Susan Eisenbach Imperial College London, James Noble Research & Programming, Sophia Drossopoulou Meta and Imperial College London
DOI
16:30
30m
Research paper
Quantitative strongest post: a calculus for reasoning about the flow of quantitative information
OOPSLA
Linpeng Zhang University College London, Benjamin Lucien Kaminski Saarland University and University College London
DOI

Fri 9 Dec

Displayed time zone: Auckland, Wellington change

09:00 - 10:00
SPLASH KeynoteKeynotes at AMRF Auditorium
Chair(s): Jeremy Singer University of Glasgow
09:00
60m
Keynote
Improving the Quality of Creative Practices with Pattern LanguagesKeynote
Keynotes
K: Takashi Iba Keio University
DOI
10:00 - 10:30
10:00
30m
Coffee break
Coffee break
Catering and Social Events

10:30 - 12:00
BlockchainOOPSLA at AMRF Auditorium
Chair(s): Zhong Shao Yale University
10:30
30m
Talk
A Study of Inline Assembly in Solidity Smart Contracts
OOPSLA
Stefanos Chaliasos Imperial College London, Arthur Gervais Imperial College London, Ben Livshits Imperial College London
DOI
11:00
30m
Research paper
Elipmoc: advanced decompilation of Ethereum smart contracts
OOPSLA
Neville Grech University of Malta, Sifis Lagouvardos University of Athens, Ilias Tsatiris University of Athens, Yannis Smaragdakis University of Athens
DOI
11:30
30m
Talk
SigVM: Enabling Event-Driven Execution for Truly Decentralized Smart Contracts
OOPSLA
Zihan Zhao University of Toronto, Sidi Mohamed Beillahi University of Toronto, Ryan Song University of Toronto, Yuxi Cai University of Toronto, Andreas Veneris University of Toronto, Fan Long University of Toronto
DOI
10:30 - 12:00
Synthesis IIOOPSLA at Lecture Theatre 2
Chair(s): Loris D'Antoni University of Wisconsin-Madison
10:30
30m
Talk
Neural Architecture Search using Property Guided Synthesis
OOPSLA
Charles Jin Massachusetts Institute of Technology, Phitchaya Mangpo Phothilimthana Google Research, Sudip Roy Cohere.ai
DOI
11:00
30m
Talk
Synthesizing Axiomatizations using Logic Learning
OOPSLA
Paul Krogmeier University of Illinois at Urbana-Champaign, Zhengyao Lin Carnegie Mellon University, Adithya Murali University of Illinois at Urbana-Champaign, P. Madhusudan University of Illinois at Urbana-Champaign
DOI
11:30
30m
Research paper
Synthesizing fine-grained synchronization protocols for implicit monitors
OOPSLA
Kostas Ferles Veridise Inc., Benjamin Sepanski The University of Texas at Austin, Rahul Krishnan University of Wisconsin-Madison, James Bornholt University of Texas at Austin, Işıl Dillig University of Texas at Austin
DOI
10:30 - 12:00
Semantics and SecurityOOPSLA at Seminar Room G007
Chair(s): Derek Dreyer MPI-SWS
10:30
30m
Research paper
Le Temps des Cerises: Efficient Temporal Stack Safety on Capability Machines using Directed CapabilitiesDistinguished Paper
OOPSLA
Aina Linn Georges Aarhus University, Alix Trieu ANSSI, Lars Birkedal Aarhus University
DOI
11:00
30m
Research paper
Plausible sealing for gradual parametricity
OOPSLA
Elizabeth Labrada University of Chile, Matías Toro University of Chile, Éric Tanter University of Chile, Dominique Devriese KU Leuven
DOI
11:30
30m
Research paper
Purity of an ST monad: full abstraction by semantically typed back-translation
OOPSLA
Koen Jacobs KU Leuven, Dominique Devriese KU Leuven, Amin Timany Aarhus University
DOI
13:30 - 15:00
Logic and Verification IOOPSLA at AMRF Auditorium
Chair(s): Benjamin Lucien Kaminski Saarland University and University College London
13:30
30m
Research paper
Finding real bugs in big programs with incorrectness logicDistinguished Paper
OOPSLA
Quang Loc Le University College London, Azalea Raad Imperial College London, Jules Villard Meta, Josh Berdine Meta, Derek Dreyer MPI-SWS, Peter W. O'Hearn Meta; University College London
DOI
14:00
30m
Talk
Fractional Resources in Unbounded Separation LogicDistinguished Paper
OOPSLA
Thibault Dardinier ETH Zurich, Peter Müller ETH Zurich, Alexander J. Summers University of British Columbia
DOI
14:30
30m
Talk
Proving Hypersafety Compositionally
OOPSLA
Emanuele D’Osualdo MPI-SWS, Azadeh Farzan University of Toronto, Derek Dreyer MPI-SWS
DOI Pre-print
13:30 - 15:00
QuantumOOPSLA at Lecture Theatre 2
Chair(s): Jan Vitek Northeastern University
13:30
30m
Research paper
Bugs in Quantum computing platforms: an empirical study
OOPSLA
Matteo Paltenghi University of Stuttgart, Germany, Michael Pradel University of Stuttgart
DOI
14:00
30m
Talk
Tower: Data Structures in Quantum Superposition
OOPSLA
Charles Yuan Massachusetts Institute of Technology, Michael Carbin Massachusetts Institute of Technology
DOI
14:30
30m
Talk
Verified Compilation of Quantum Oracles
OOPSLA
Liyi Li University of Maryland, Finn Voichick University of Maryland, Kesha Hietala University of Maryland, Yuxiang Peng University of Maryland, Xiaodi Wu University of Maryland, Michael Hicks University of Maryland; Amazon
DOI
13:30 - 14:30
DebuggingOOPSLA at Seminar Room G007
Chair(s): Neville Grech University of Malta
13:30
30m
Talk
AnICA: Analyzing Inconsistencies in Microarchitectural Code Analyzers
OOPSLA
Fabian Ritter Saarland University, Germany, Sebastian Hack Saarland University, Germany
DOI
14:00
30m
Talk
Seq2Parse: Neurosymbolic Parse Error Repair
OOPSLA
Georgios Sakkas University of California at San Diego, Madeline Endres University of Michigan, Philip Guo University of California at San Diego, Westley Weimer University of Michigan, Ranjit Jhala University of California at San Diego
DOI
15:30 - 17:00
Systems and VerificationOOPSLA at AMRF Auditorium
Chair(s): Suresh Jagannathan Purdue University
15:30
30m
Talk
BFF: Foundational and Automated Verification of Bitfield-Manipulating Programs
OOPSLA
Fengmin Zhu MPI-SWS, Michael Sammler MPI-SWS, Rodolphe Lepigre MPI-SWS, Derek Dreyer MPI-SWS, Deepak Garg MPI-SWS
DOI
16:00
30m
Talk
Compositional Virtual Timelines: Verifying Dynamic-Priority Partitions with Algorithmic Temporal Isolation
OOPSLA
Mengqi Liu Yale University, Zhong Shao Yale University, Hao Chen Yale University, Man-Ki Yoon Yale University, Jung-Eun Kim Yale University
DOI
16:30
30m
Research paper
Linear types for large-scale systems verificationDistinguished Paper
OOPSLA
Jialin Li , Andrea Lattuada ETH Zurich, Yi Zhou Carnegie Mellon University, Jonathan Cameron Carnegie Mellon University, Jon Howell VMWare Research, Bryan Parno Carnegie Mellon University, USA, Chris Hawblitzel Microsoft Research
DOI
15:30 - 17:00
EffectsOOPSLA at Lecture Theatre 2
Chair(s): Peter Thiemann University of Freiburg, Germany
15:30
30m
Research paper
Effects, capabilities, and boxes: from scope-based reasoning to type-based reasoning and back
OOPSLA
Jonathan Immanuel Brachthäuser University of Tübingen, Philipp Schuster University of Tübingen, Edward Lee University of Waterloo, Aleksander Boruch-Gruszecki EPFL
DOI
16:00
30m
Talk
First-class Names for Effect Handlers
OOPSLA
Ningning Xie University of Toronto, Youyou Cong Tokyo Institute of Technology, Kazuki Ikemori Tokyo Institute of Technology, Daan Leijen Microsoft Research
DOI
16:30
30m
Talk
High-Level Effect Handlers in C++
OOPSLA
Dan Ghica Huawei, Sam Lindley University of Edinburgh, Marcos Maronas Bravo Huawei, Maciej Piróg Huawei
DOI
15:30 - 17:00
ProbabilisticOOPSLA at Seminar Room G007
Chair(s): Benjamin Lucien Kaminski Saarland University and University College London
15:30
30m
Talk
Semi-symbolic Inference for Efficient Streaming Probabilistic Programming
OOPSLA
Eric Atkinson Massachusetts Institute of Technology, Charles Yuan Massachusetts Institute of Technology, Guillaume Baudart Inria, Louis Mandel IBM Research, Michael Carbin Massachusetts Institute of Technology
DOI
16:00
30m
Talk
Symbolic Execution for Randomized Programs
OOPSLA
Zachary Susag Cornell University, Sumit Lahiri IIT Kanpur, Justin Hsu Cornell University, Subhajit Roy IIT Kanpur
DOI
16:30
30m
Talk
This Is the Moment for Probabilistic Loops
OOPSLA
DOI

Sat 10 Dec

Displayed time zone: Auckland, Wellington change

09:00 - 10:00
SPLASH KeynoteKeynotes at AMRF Auditorium
Chair(s): Jan Vitek Northeastern University
09:00
60m
Keynote
(I Can't Get No) VerificationKeynote
Keynotes
K: Atsushi Igarashi Kyoto University
DOI
10:00 - 10:30
10:00
30m
Coffee break
Coffee break
Catering and Social Events

10:30 - 12:00
Logic and ConcurrencyOOPSLA at AMRF Auditorium
Chair(s): Mohsen Lesani University of California at Riverside
10:30
30m
Talk
A Concurrent Program Logic with a Future and History
OOPSLA
Roland Meyer TU Braunschweig, Thomas Wies New York University, Sebastian Wolff New York University
DOI
11:00
30m
Talk
CAAT: Consistency as a TheoryDistinguished Paper
OOPSLA
Thomas Haas TU Braunschweig, Roland Meyer TU Braunschweig, Hernán Ponce de León Huawei Dresden Research Center
DOI
11:30
30m
Talk
Implementing and Verifying Release-Acquire Transactional Memory in C11
OOPSLA
Sadegh Dalvandi University of Surrey, Brijesh Dongol University of Surrey
DOI
10:30 - 12:00
ProofsOOPSLA at Lecture Theatre 2
Chair(s): Atsushi Igarashi Kyoto University
10:30
30m
Talk
Data-Driven Lemma Synthesis for Interactive Proofs
OOPSLA
Aishwarya Sivaraman University of California at Los Angeles, Alex Sanchez-Stern University of Massachusetts at Amherst, Bretton Chen University of California at Los Angeles, Sorin Lerner University of California at San Diego, Todd Millstein University of California at Los Angeles
DOI
11:00
30m
Talk
Intrinsically-Typed Definitional Interpreters à la Carte
OOPSLA
Cas van der Rest Delft University of Technology, Casper Bach Poulsen Delft University of Technology, Arjen Rouvoet Delft University of Technology, Eelco Visser Delft University of Technology, Peter D. Mosses Swansea University and Delft University of Technology
DOI
11:30
30m
Research paper
Proof transfer for fast certification of multiple approximate neural networks
OOPSLA
Shubham Ugare University of Illinois at Urbana-Champaign, Gagandeep Singh University of Illinois at Urbana-Champaign, Sasa Misailovic University of Illinois at Urbana-Champaign
DOI
10:30 - 12:00
DSLsOOPSLA at Seminar Room G007
Chair(s): Robert Bruce Findler Northwestern University
10:30
30m
Talk
Can Guided Decomposition Help End-Users Write Larger Block-Based Programs? A Mobile Robot Experiment
OOPSLA
Nico Ritschel University of British Columbia, Felipe Fronchetti Virginia Commonwealth University, Reid Holmes University of British Columbia, Ronald Garcia University of British Columbia, David C. Shepherd Virginia Commonwealth University
DOI
11:00
30m
Talk
Compositional Embeddings of Domain-Specific Languages
OOPSLA
Yaozhu Sun University of Hong Kong, Utkarsh Dhandhania University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong
DOI Pre-print
11:30
30m
Research paper
Language-parametric static semantic code completion
OOPSLA
Daniel A. A. Pelsmaeker Delft University of Technology, Netherlands, Hendrik van Antwerpen Delft University of Technology, Casper Bach Poulsen Delft University of Technology, Eelco Visser Delft University of Technology
DOI
13:30 - 15:00
Testing and MaintenanceOOPSLA at AMRF Auditorium
Chair(s): Işıl Dillig University of Texas at Austin
13:30
30m
Talk
Overwatch: Learning Patterns in Code Edit Sequences
OOPSLA
Yuhao Zhang University of Wisconsin-Madison, Yasharth Bajpai Microsoft, Priyanshu Gupta Microsoft, Ameya Ketkar Uber, Miltiadis Allamanis Microsoft Research, Titus Barik Microsoft, Sumit Gulwani Microsoft, Arjun Radhakrishna Microsoft, Mohammad Raza Microsoft, Gustavo Soares Microsoft, Ashish Tiwari Microsoft
DOI
14:00
30m
Talk
Satisfiability Modulo Fuzzing: A Synergistic Combination of SMT Solving and Fuzzing
OOPSLA
Sujit Kumar Muduli IIT Kanpur, Subhajit Roy IIT Kanpur
DOI
14:30
30m
Talk
Synthesizing Code Quality Rules from Examples
OOPSLA
DOI
13:30 - 15:00
ConcurrencyOOPSLA at Lecture Theatre 2
Chair(s): Suresh Jagannathan Purdue University
13:30
30m
Research paper
C4: verified transactional objects
OOPSLA
Mohsen Lesani University of California at Riverside, Li-yao Xia University of Pennsylvania, Anders Kaseorg Massachusetts Institute of Technology, Christian J. Bell MIT CSAIL, Adam Chlipala Massachusetts Institute of Technology, Benjamin C. Pierce University of Pennsylvania, Steve Zdancewic University of Pennsylvania
DOI
14:00
30m
Talk
Concurrent Size
OOPSLA
Gal Sela Technion, Erez Petrank Technion
DOI
14:30
30m
Talk
Veracity: Declarative Multicore Programming with Commutativity
OOPSLA
Adam Chen Stevens Institute of Technology, Parisa Fathololumi Stevens Institute of Technology, Eric Koskinen Stevens Institute of Technology, Jared Pincus Stevens Institute of Technology
DOI
13:30 - 15:00
Logic and Verification IIOOPSLA at Seminar Room G007
Chair(s): Atsushi Igarashi Kyoto University
13:30
30m
Research paper
On incorrectness logic for Quantum programs
OOPSLA
Peng Yan University of Technology Sydney, Hanru Jiang Yanqi Lake Beijing Institute of Mathematical Sciences and Applications, China, Nengkun Yu Stony Brook University, USA
DOI
14:00
30m
Research paper
Weighted programming: a programming paradigm for specifying mathematical models
OOPSLA
Kevin Batz RWTH Aachen University, Adrian Gallus RWTH Aachen University, Benjamin Lucien Kaminski Saarland University and University College London, Joost-Pieter Katoen RWTH Aachen University, Tobias Winkler RWTH Aachen University
DOI
14:30
30m
Talk
Wildcards Need Witness ProtectionDistinguished Paper
OOPSLA
DOI
15:30 - 17:00
Synthesis IIIOOPSLA at Lecture Theatre 2
Chair(s): Ilya Sergey National University of Singapore
15:30
30m
Research paper
Automated transpilation of imperative to functional code using neural-guided program synthesis
OOPSLA
Benjamin Mariano University of Texas at Austin, Yanju Chen University of California at Santa Barbara, Yu Feng University of California at Santa Barbara, Greg Durrett University of Texas at Austin, Işıl Dillig University of Texas at Austin
DOI
16:00
30m
Talk
Synthesis-Powered Optimization of Smart Contracts via Data Type Refactoring
OOPSLA
Yanju Chen University of California at Santa Barbara, Yuepeng Wang Simon Fraser University, Maruth Goyal University of Texas at Austin, James Dong Stanford University, Yu Feng University of California at Santa Barbara, Işıl Dillig University of Texas at Austin
DOI
16:30
30m
Talk
Synthesizing Abstract Transformers
OOPSLA
Pankaj Kumar Kalita IIT Kanpur, Sujit Kumar Muduli IIT Kanpur, Loris D'Antoni University of Wisconsin-Madison, Thomas Reps University of Wisconsin-Madison, Subhajit Roy IIT Kanpur
DOI
16:00 - 17:00
DataOOPSLA at AMRF Auditorium
Chair(s): Amal Ahmed Northeastern University, USA
16:00
30m
Talk
Indexing the Extended Dyck-CFL Reachability for Context-Sensitive Program AnalysisVirtual
OOPSLA
Qingkai Shi Ant Group, Yongchao WANG Hong Kong University of Science and Technology, Peisen Yao Hong Kong University of Science and Technology, Charles Zhang Hong Kong University of Science and Technology
DOI
16:30
30m
Talk
The Essence of Online Data Processing
OOPSLA
Philip Dexter SUNY Binghamton, Yu David Liu SUNY Binghamton, Kenneth Chiu SUNY Binghamton
DOI