SPLASH 2022 (series) /
KeynotesSPLASH 2022
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
Dates
Tracks
Plenary
Thu 8 DecDisplayed time zone: Auckland, Wellington change
Thu 8 Dec
Displayed time zone: Auckland, Wellington change
09:00 - 10:00 | |||
09:00 60mKeynote | Myths and Mythconceptions: What does it mean to be a programming language, anyhow?Keynote Keynotes DOI | ||
10:00 - 10:30 | |||
10:00 30mCoffee break | Coffee break Catering and Social Events | ||
10:30 - 12:00 | |||
10:30 30mTalk | A Fast In-Place Interpreter for WebAssembly OOPSLA Ben L. Titzer Carnegie Mellon University DOI | ||
11:00 30mTalk | 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 30mTalk | The Road Not Taken: Exploring Alias Analysis Based Optimizations Missed by the Compiler OOPSLA DOI | ||
10:30 - 12:00 | |||
10:30 30mResearch paper | Complexity-guided container replacement synthesis 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 30mTalk | 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 30mTalk | Specification-Guided Component-Based Synthesis from Effectful Libraries OOPSLA DOI | ||
10:30 - 12:00 | |||
10:30 30mResearch paper | C to checked C by 3c OOPSLA Aravind Machiry Purdue University, John Kastner Amazon, Matt McCutchen , Aaron Eline Amazon, Kyle Headley Amazon, MIchael Hicks Amazon DOI | ||
11:00 30mTalk | Solo: A Lightweight Static Analysis for Differential Privacy OOPSLA DOI | ||
11:30 30mTalk | 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 90mLunch | Lunch Catering and Social Events | ||
14:00 - 15:00 | |||
14:00 60mKeynote | The State Of Debugging in 2022KeynoteSupported by Google Keynotes DOI | ||
15:00 - 15:30 | |||
15:00 30mCoffee break | Coffee break Catering and Social Events | ||
15:30 - 17:00 | |||
15:30 30mTalk | 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 30mTalk | 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 30mTalk | 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 | |||
15:30 30mTalk | Compilation of Dynamic Sparse Tensor Algebra OOPSLA Stephen Chou Massachusetts Institute of Technology, Saman Amarasinghe Massachusetts Institute of Technology DOI | ||
16:00 30mTalk | 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 30mTalk | 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 | |||
15:30 30mTalk | Checking Equivalence in a Non-strict Language OOPSLA DOI | ||
16:00 30mTalk | 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 30mResearch 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 DecDisplayed time zone: Auckland, Wellington change
Fri 9 Dec
Displayed time zone: Auckland, Wellington change
09:00 - 10:00 | |||
09:00 60mKeynote | Improving the Quality of Creative Practices with Pattern LanguagesKeynote Keynotes DOI | ||
10:00 - 10:30 | |||
10:00 30mCoffee break | Coffee break Catering and Social Events | ||
10:30 - 12:00 | |||
10:30 30mTalk | 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 30mResearch 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 30mTalk | 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 | |||
10:30 30mTalk | 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 30mTalk | 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 30mResearch 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 | |||
10:30 30mResearch paper | Le Temps des Cerises: Efficient Temporal Stack Safety on Capability Machines using Directed Capabilities OOPSLA DOI | ||
11:00 30mResearch 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 30mResearch paper | Purity of an ST monad: full abstraction by semantically typed back-translation OOPSLA 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 30mResearch paper | Finding real bugs in big programs with incorrectness logic 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 30mTalk | Fractional Resources in Unbounded Separation Logic OOPSLA Thibault Dardinier ETH Zurich, Peter Müller ETH Zurich, Alexander J. Summers University of British Columbia DOI | ||
14:30 30mTalk | Proving Hypersafety Compositionally OOPSLA DOI Pre-print | ||
13:30 - 15:00 | |||
13:30 30mResearch paper | Bugs in Quantum computing platforms: an empirical study OOPSLA DOI | ||
14:00 30mTalk | Tower: Data Structures in Quantum Superposition OOPSLA Charles Yuan Massachusetts Institute of Technology, Michael Carbin Massachusetts Institute of Technology DOI | ||
14:30 30mTalk | 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 | |||
13:30 30mTalk | AnICA: Analyzing Inconsistencies in Microarchitectural Code Analyzers OOPSLA DOI | ||
14:00 30mTalk | 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 | |||
15:30 30mTalk | 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 30mTalk | 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 30mResearch paper | Linear types for large-scale systems verification 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 | |||
15:30 30mResearch 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 30mTalk | First-class Names for Effect Handlers OOPSLA Ningning Xie University of Cambridge / University of Toronto, Youyou Cong Tokyo Institute of Technology, Kazuki Ikemori Tokyo Institute of Technology, Daan Leijen Microsoft Research DOI | ||
16:30 30mTalk | 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 30mTalk | 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 30mTalk | 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 30mTalk | This Is the Moment for Probabilistic Loops OOPSLA DOI | ||
Sat 10 DecDisplayed time zone: Auckland, Wellington change
Sat 10 Dec
Displayed time zone: Auckland, Wellington change
09:00 - 10:00 | |||
09:00 60mKeynote | (I Can't Get No) VerificationKeynote Keynotes DOI | ||
10:00 - 10:30 | |||
10:00 30mCoffee 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 30mTalk | A Concurrent Program Logic with a Future and History OOPSLA DOI | ||
11:00 30mTalk | CAAT: Consistency as a Theory OOPSLA Thomas Haas TU Braunschweig, Roland Meyer TU Braunschweig, Hernán Ponce de León Huawei Dresden Research Center DOI | ||
11:30 30mTalk | Implementing and Verifying Release-Acquire Transactional Memory in C11 OOPSLA DOI | ||
10:30 - 12:00 | |||
10:30 30mTalk | 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 30mTalk | 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 30mResearch 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 | |||
10:30 30mTalk | 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 30mTalk | 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 30mResearch 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 30mTalk | 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 30mTalk | Satisfiability Modulo Fuzzing: A Synergistic Combination of SMT Solving and Fuzzing OOPSLA DOI | ||
14:30 30mTalk | Synthesizing Code Quality Rules from Examples OOPSLA DOI | ||
13:30 - 15:00 | |||
13:30 30mResearch 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 30mTalk | Concurrent Size OOPSLA DOI | ||
14:30 30mTalk | 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 | |||
13:30 30mResearch 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 30mResearch 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 30mTalk | Wildcards Need Witness Protection OOPSLA Kevin Bierhoff Google DOI | ||
15:30 - 17:00 | |||
15:30 30mResearch 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 30mTalk | 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 30mTalk | 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 | |||
16:00 30mTalk | 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 30mTalk | The Essence of Online Data Processing OOPSLA DOI | ||