SPLASH 2022
Mon 5 - Sat 10 December 2022 Auckland, New Zealand
VenueUniversity of Auckland
Room nameAMRF Auditorium
Room number505-011
Capacity300
Program

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

Mon 5 Dec

Displayed time zone: Auckland, Wellington change

09:00 - 10:00
Keynote 1SAS at AMRF Auditorium
Chair(s): Gagandeep Singh University of Illinois at Urbana-Champaign, Caterina Urban Inria & École Normale Supérieure | Université PSL
09:00
60m
Keynote
Commercial-Grade Static Analyzers in DatalogIn PersonKeynote
SAS
Bernhard Scholz University of Sydney
10:30 - 12:00
Model Checking and VerificationSAS at AMRF Auditorium
Chair(s): Arlen Cox IDA
10:30
30m
Talk
Parameterized Recursive Refinement Types for Automated Program Verification
SAS
Ryoya Mukai The University of Tokyo, Naoki Kobayashi University of Tokyo, Japan, Ryosuke Sato University of Tokyo, Japan
11:00
30m
Talk
Efficient Modular SMT-Based Model Checking of Pointer ProgramsVirtual
SAS
Isabel Garcia-Contreras University of Waterloo, Arie Gurfinkel University of Waterloo, Jorge A. Navas Certora, inc.
11:30
30m
Talk
Case Study on Verification-Witness Validators: Where We Are and Where We Go
SAS
Dirk Beyer LMU Munich, Jan Strejcek Masaryk University
Link to publication DOI Media Attached
13:30 - 15:00
Numerical Static AnalysesSAS at AMRF Auditorium
Chair(s): Isabella Mastroeni University of Verona, Italy
13:30
30m
Talk
CLEVEREST: Accelerating CEGAR-based Neural Network Verification via Adversarial AttacksVirtual
SAS
Zhe Zhao ShanghaiTech University, Yedi Zhang ShanghaiTech University, Guangke Chen ShanghaiTech University, Fu Song ShanghaiTech University, Taolue Chen Birkbeck University of London, Jiaxiang Liu Shenzhen University
14:00
30m
Talk
Boosting Robustness Verification of Semantic Feature Neighborhoods
SAS
Anan Kabaha Technion, Israel Institute of Technology, Dana Drachsler Cohen Technion
14:30
30m
Talk
Lifting Numeric Relational Domains to Algebraic Data Types
SAS
Santiago Bautista Univ Rennes, Inria, CNRS, IRISA, Thomas P. Jensen INRIA Rennes, Benoît Montagu Inria
Pre-print File Attached
15:30 - 17:00
Keynote 2, Radhia Cousot Award, PC Chairs ReportSAS at AMRF Auditorium
Chair(s): Gagandeep Singh University of Illinois at Urbana-Champaign, Caterina Urban Inria & École Normale Supérieure | Université PSL
15:30
60m
Keynote
Logical Reasoning in Reinforcement Learning: A Boon or Bane? KeynoteVirtual
SAS
Suguman Bansal Rice University, USA
16:30
10m
Awards
Radhia Cousot Award
SAS
Caterina Urban Inria & École Normale Supérieure | Université PSL, Gagandeep Singh University of Illinois at Urbana-Champaign
16:40
20m
Day closing
PC Chairs Report
SAS
Caterina Urban Inria & École Normale Supérieure | Université PSL, Gagandeep Singh University of Illinois at Urbana-Champaign

Tue 6 Dec

Displayed time zone: Auckland, Wellington change

09:00 - 10:00
Keynote 3SAS at AMRF Auditorium
Chair(s): Gagandeep Singh University of Illinois at Urbana-Champaign, Caterina Urban Inria & École Normale Supérieure | Université PSL
09:00
60m
Keynote
Towards Efficient Reasoning of Quantum ProgramsKeynote
SAS
Nengkun Yu Stony Brook University, USA
10:30 - 12:00
SecuritySAS at AMRF Auditorium
Chair(s): Emanuele D’Osualdo MPI-SWS
10:30
30m
Talk
SecWasm: Information Flow Control for WebAssemblyVirtual
SAS
Iulia Bastys Chalmers University of Technology, Maximilian Algehed Chalmers University of Technology, Sweden, Alexander Sjösten TU Wien, Andrei Sabelfeld Chalmers University of Technology
11:00
30m
Talk
Adversarial Logic
SAS
Julien Vanegue Bloomberg
11:30
30m
Talk
Property-driven code obfuscations - Reinterpreting Jones-optimality in Abstract Interpretation
SAS
Roberto Giacobazzi University of Verona, Isabella Mastroeni University of Verona, Italy
13:30 - 15:00
Logic and CompletenessSAS at AMRF Auditorium
Chair(s): Roberto Giacobazzi University of Verona
13:30
30m
Talk
Invariant Inference With Provable Complexity From the Monotone Theory
SAS
Yotam M. Y. Feldman Tel Aviv University, Sharon Shoham Tel Aviv University
14:00
30m
Talk
Local Completeness Logic on Kleene Algebra with Tests
SAS
Marco Milanese Dipartimento di Matematica, University of Padova, Italy, Francesco Ranzato University of Padova
14:30
30m
Talk
Deciding program properties via complete abstractions on bounded domains
SAS
Roberto Bruni University of Pisa, Roberta Gori University of Pisa, Nicolas Manini IMDEA Software Institute
15:30 - 17:00
Invariant and Program SynthesisSAS at AMRF Auditorium
Chair(s): Subhajit Roy IIT Kanpur
15:30
30m
Talk
Bootstrapping Library-Based Synthesis
SAS
Kangjing Huang Purdue University, USA, Xiaokang Qiu Purdue University, USA
16:00
30m
Talk
Automated Synthesis of Asynchronizations
SAS
Sidi Mohamed Beillahi University of Toronto, Ahmed Bouajjani IRIF, Université Paris Diderot, Constantin Enea Ecole Polytechnique / LIX / CNRS, Shuvendu K. Lahiri Microsoft Research
16:30
30m
Talk
Solving Invariant Generation for Unsolvable Loops
SAS
Daneshvar Amrollahi Stanford University, Ezio Bartocci TU Wien, George Kenison TU Wien, Laura Kovács TU Wien, Marcel Moosbrugger TU Wien, Miroslav Stankovič TU Wien

Wed 7 Dec

Displayed time zone: Auckland, Wellington change

10:30 - 12:00
Compilers and OptimizationsSAS at AMRF Auditorium
10:30
30m
Talk
Semantic Foundations for Cost Analysis of Pipeline-Optimized ProgramsVirtual
SAS
Solène Mirliaz ENS Rennes / IRISA / Inria, David Pichardie Meta, Gilles Barthe MPI-SP, Germany / IMDEA Software Institute, Spain, Adrien Koutsos INRIA Paris, Peter Schwabe Max Planck Institute for Security and Privacy
11:00
30m
Talk
Principles of Staged Static+Dynamic Partial Analysis
SAS
Aditya Anand IIT Mandi, Manas Thakur IIT Bombay
11:30
30m
Talk
Fast and incremental computation of weak control closure
SAS
Abu Naser Masud Malardalen University
13:30 - 15:00
DLS Talks 1DLS at AMRF Auditorium
Chair(s): Stefan Marr University of Kent
13:30
10m
Talk
Chair's Welcome and Most Notable Paper Award
DLS

13:40
40m
Talk
Invited Talk: A decade of Self-Optimizing Interpreters in GraalVMVirtual
DLS
Christian Wimmer Oracle Labs
14:20
40m
Talk
Invited Talk: Live Programming over TCP? Bringing Squeak/Smalltalk Liveness to Godot via React/SVirtual
DLS
Tom Beckmann University of Potsdam; Hasso Plattner Institute, Leonard Geier University of Potsdam; Hasso Plattner Institute, Robert Hirschfeld University of Potsdam; Hasso Plattner Institute
15:30 - 17:00
DLS Talks 2DLS at AMRF Auditorium
Chair(s): James Noble Research & Programming
15:30
30m
Talk
Execution vs. Parse-Based Language Servers: Tradeoffs and Opportunities for Language-Agnostic Tooling for Dynamic Languages
DLS
Stefan Marr University of Kent, Humphrey Burchell University of Kent, Fabio Niephaus Oracle Labs, Potsdam
DOI Pre-print
16:00
30m
Talk
Who You Gonna Call: Analyzing the Run-time Call-Site Behavior of Ruby Applications
DLS
Sophie Kaleba University of Kent, Octave Larose University of Kent, Richard Jones University of Kent, Stefan Marr University of Kent
DOI Pre-print
16:30
30m
Talk
Dynamic Pattern Matching with Python
DLS
Tobias Kohn University of Cambridge, UK, Guido van Rossum Python Software Foundation, Brandt Bucher Research Affiliates, LLC, Talin , Ivan Levkivskyi Dropbox Ireland
DOI Pre-print
17:30 - 19:30
17:30
15m
Poster
Termination of Recursive Functions by Lexicographic Orders of Linear Combinations
Student Research Competition
DOI
17:45
15m
Poster
Automated Verification for Real-Time Systems using Implicit Clocks and an Extended Antimirov Algorithm
Student Research Competition
Yahui Song National University of Singapore, Wei-Ngan Chin National University of Singapore
DOI
18:00
15m
Poster
CodeSpider: Automatic Code Querying with Multi-modal Conjunctive Query Synthesis
Student Research Competition
Chengpeng Wang Hong Kong University of Science and Technology
DOI
18:15
15m
Poster
LoRe: Local-First Reactive Programming with Verified Safety Guarantees
Student Research Competition
Julian Haas TU Darmstadt
DOI
18:30
15m
Poster
Foundationally Sound Annotation Verifier via Control Flow Splitting
Student Research Competition
Litao Zhou Shanghai Jiao Tong University
DOI
18:45
15m
Poster
Using Mutations to Analyze Formal Specifications
Student Research Competition
Siraphob Phipathananunth Vanderbilt University
DOI
19:00
15m
Poster
ARENA: Enhancing Abstract Refinement for Neural Network Verification
Student Research Competition
Yuyi Zhong National University of Singapore, Quang-Trung Ta National University of Singapore, Siau-Cheng Khoo National University of Singapore
DOI
19:15
15m
Poster
Qiwi: A Beginner Friendly Quantum Language
Student Research Competition
Abhinandan Pal IIIT Kalyani, Anubhab Ghosh IIIT Kalyani
DOI

Thu 8 Dec

Displayed time zone: Auckland, Wellington change

08:45 - 09:00
Opening and WelcomeOpening and Welcome at AMRF Auditorium
Chair(s): Kelly Blincoe University of Auckland, Alex Potanin Australian National University
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: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
13:45 - 14:00
SPLASH AwardsAwards at AMRF Auditorium
13:45
15m
Awards
SPLASH AwardsAwards
Awards

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: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

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: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
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
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

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: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
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
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

Mon 5 Dec

Displayed time zone: Auckland, Wellington change

Tue 6 Dec

Displayed time zone: Auckland, Wellington change

Wed 7 Dec

Displayed time zone: Auckland, Wellington change

Room9:003010:003011:003012:003013:003014:003015:003016:003017:003018:003019:0030
AMRF Auditorium

Thu 8 Dec

Displayed time zone: Auckland, Wellington change

Fri 9 Dec

Displayed time zone: Auckland, Wellington change

Sat 10 Dec

Displayed time zone: Auckland, Wellington change

Wed 7 Dec

Displayed time zone: Auckland, Wellington change

Room10:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:0015304518:0015304519:00153045
AMRF Auditorium