SPLASH 2025 - OOPSLA - SPLASH 2025

SPLASH 2025 - OOPSLA - SPLASH 2025
SPLASH 2025
Sun 12 - Sat 18 October 2025
Singapore
co-located with
ICFP/SPLASH 2025
Attending
Venue (Sunday Workshops): NUS School of Computing
Venue (FARM Performance): Yong Siew Toh Conservatory
Venue (Main Conference): Marina Bay Sands Convention Centre
Hotels: Concorde Hotel Singapore
Hotels: Wyndham Singapore Hotel
Hotels: Rendezvous Hotel Singapore
ICFP/SPLASH 2025
Code of Conduct
Call for Sponsorship
Registration
Travel Information
Explore Singapore
Outdoor Activities
Information for Presenters at National University of Singapore
Information for Presenters at Marina Bay Sands
Information for Session Chairs
Information for Attendees
ICFP/SPLASH Live Streams
Program
ICFP/SPLASH Program
Your Program
Filter by Day
Sun 12 Oct
Mon 13 Oct
Tue 14 Oct
Wed 15 Oct
Thu 16 Oct
Fri 17 Oct
Sat 18 Oct
Tracks
SPLASH 2025
Doctoral Symposium
FARM
OOPSLA
OOPSLA Artifacts
Onward! Essays
Onward! Papers
Posters
SPLASH Keynotes
SPLASH-E
Student Research Competition
ICFP/SPLASH 2025
Tutorials
Volunteers
Workshops
Co-hosted Conferences
ICFP
ICFP
ICFP
Artifacts
ICFP
Keynotes
ICFP
Papers
ICFP
Student Research Competition
ICFP
JFP First Papers
ICFP
Diversity, Equity, and Inclusion
MPLR
Workshops
Erlang
FARM
FUNARCH
HATRA
HOPE
IWACO
LMPL
miniKanren
ML Family Workshop
OCaml
OlivierFest
PAINT
PLMW @ ICFP/SPLASH
PROPL
REBASE
Scheme
Sponsor Invited Talks
The Scala Workshop
The Scala Workshop
- Where Are We With Scala's Capabilities?
- Simpler Scala Builds with Functional and Object-Oriented Programming
TyDe
VMIL
WebAssembly Workshop
@ ICFP/SPLASH
Co-hosted Symposia
Haskell
SAS
SAS
SAS
Artifact
Organization
SPLASH 2025 Committees
Organizing Committee
Steering Committee
Track Committees
Doctoral Symposium
FARM
Organizing Committee
Program Committee
OOPSLA
OOPSLA Review Committee
External Review / Artifact Evaluation Committee
OOPSLA Artifacts
Onward! Essays
Program Committee
Onward! Steering Committee
Onward! Papers
Program Committee
Steering Committee
Posters
SPLASH-E
Program Commitee
Steering Committee
Student Research Competition
Competition Judges
Review Committee
ICFP/SPLASH
Volunteers
Workshops
Contributors
People Index
Co-hosted Conferences
ICFP
Organizing Committee
Steering Committee
Distinguished Papers Committee
ICFP Artifacts
ICFP Papers
ICFP Student Research Competition
MPLR
Program Committee
Steering Committee
Workshops
Erlang
Organizing Committee
Program Committee
FARM
Organizing Committee
FUNARCH
Program Committee
HATRA
Organizing Committee
Program Committee
HOPE
Program Committee
IWACO
Organizing Committee
LMPL
Organizing Committee
Keynote Speaker
Program Committee
miniKanren
Organizing Committee
Program Committee
ML Family Workshop
Program Committee
OCaml
Program Committee
OlivierFest
Program Committee
PAINT
Organizing Committee
Program Committee
PLMW @ ICFP/SPLASH
Program Committee
PROPL
Program Committee
Organising Committee
REBASE
Organizing Committee
Scheme
Organizing Committee
Program Committee
Sponsor Invited Talks
Organizing Committee
The Scala Workshop
Organizing Committee
Program Committee
TyDe
Organising Committee
Program Committee
VMIL
Organizing Committee
Program Committee
WebAssembly Workshop
Organizers
Program Committee
Co-hosted Symposia
Haskell
Program Committee
SAS
SAS 2025
Program Committee
SAS 2025
Steering Committee
SAS Artifact
Series
Series
SPLASH 2026
SPLASH 2025
SPLASH 2024
SPLASH 2023
SPLASH 2022
SPLASH 2021
SPLASH 2020
SPLASH 2019
SPLASH 2018
SPLASH 2017
SPLASH 2016
SPLASH 2015
SPLASH 2014
SPLASH 2013
SPLASH 2012
SPLASH 2011
SPLASH 2010
OOPSLA 2009
OOPSLA 2008
OOPSLA 2007
OOPSLA 2006
OOPSLA 2005
OOPSLA 2004
OOPSLA 2003
OOPSLA 2002
OOPSLA 2001
OOPSLA 2000
SPLASH 2025
Singapore
Gardens by the Bay
Marina Bay and Merlion
Lau Pa Sat
Hawker Centre
ArtScience Museum
Singapore Botanic Gardens
The Rain Vortex at Jewel Changi Airport
Little India
Flower Dome
Resorts World Sentosa
National University of Singapore
ICFP/SPLASH 2025
series
) /
SPLASH 2025
series
) /
OOPSLA
SPLASH 2025
About
Program
Accepted Papers
Call for Papers
Post-event Survey Results
ICFP/SPLASH 2025
post-event survey results are available here
. We thank all the participants for their feedback!
Distinguished Reviewer Awards
This year, we had an exceptional Review Committee with over 100 RC members and 8 Associate Chairs. Nevertheless, several people in our group of AEs and chairs explicitly called out the following reviewers’ conscientiousness, effort, quality, and dedication as going well above and beyond the call of duty. Huge congratulations to the following distinguished reviewers:
Richard A. Eisenberg, Jane Street
Karine Even-Mendoza, King’s College London
Emily First, University of California, San Diego
Ben Hardekopf, University of California, Santa Barbara
Lindsey Kuper, University of California, Santa Cruz
Stefan Marr, University of Kent
Caleb Stanford, University of California, Davis
Dates
Tracks
Plenary
Program Display Configuration
Close
You're viewing the program in a time zone which is different from your device's time zone
change time zone
Thu 16 Oct
Displayed time zone:
Perth
change
09:00 - 10:00
Thursday SPLASH Keynote
SPLASH Keynotes
at
Orchid Plenary Ballroom
Chair(s):
Sukyoung Ryu
KAIST
09:00
60m
Keynote
Automating maintenance of the Linux kernel: a perspective over 20 years
SPLASH Keynotes
K:
Julia Lawall
Inria
10:00 - 10:30
Coffee break
ICFP/SPLASH Catering
at
Orchid Dining Hall
10:00
30m
Coffee break
Break
ICFP/SPLASH Catering
10:30 - 12:15
Runtime
OOPSLA
at
Orchid East
Chair(s):
Stefan Marr
Johannes Kepler University Linz
10:30
15m
Talk
Unveiling Heisenbugs with Diversified Execution
OOPSLA
Arjun Ramesh
Carnegie Mellon University
Tianshu Huang
Carnegie Mellon University
Jaspreet Riar
Carnegie Mellon University
Ben L. Titzer
Carnegie Mellon University
Anthony Rowe
Carnegie Mellon University
10:45
15m
Talk
TailTracer: Continuous Tail Tracing for Production Use
OOPSLA
Tianyi Liu
Nanjing University
Yi Li
Nanyang Technological University
Yiyu Zhang
Nanjing University
Zhuangda Wang
Xiamen University
Rongxin Wu
Xiamen University
Xuandong Li
Nanjing University
Zhiqiang Zuo
Nanjing University
11:00
15m
Talk
Heap-Snapshot Matching and Ordering using CAHPs: A Context-Augmented Heap-Path Representation for Exact and Partial Path Matching using Prefix Trees
OOPSLA
Matteo Basso
Università della Svizzera italiana (USI)
Aleksandar Prokopec
Oracle Labs
Andrea Rosà
USI Lugano
Walter Binder
USI Lugano
11:15
15m
Talk
Float Self-Tagging
OOPSLA
Olivier Melançon
Université de Montréal
Manuel Serrano
Inria; Université Côte d’Azur
Marc Feeley
Université de Montréal
Pre-print
11:30
15m
Talk
HEMVM: a Heterogeneous Blockchain Framework for Interoperable Virtual Machines
OOPSLA
Vladyslav Nekriach
University Of Toronto
Sidi Mohamed Beillahi
University of Toronto
Chenxing Li
Shanghai Tree-Graph Blockchain Research Institute
Peilun Li
Shanghai Tree-Graph Blockchain Research Institute
Ming Wu
Shanghai Tree-Graph Blockchain Research Institute
Andreas Veneris
University of Toronto
Fan Long
University of Toronto
11:45
15m
Talk
Advancing Performance via a Systematic Application of Research and Industrial Best Practice
OOPSLA
Wenyu Zhao
Australian National University
Stephen M. Blackburn
Google; Australian National University
Kathryn S McKinley
Google
Man Cao
Google
Sara S. Hamouda
Canva
10:30 - 12:15
Code
OOPSLA
at
Orchid Plenary Ballroom
Chair(s):
Jiasi Shen
The Hong Kong University of Science and Technology
10:30
15m
Talk
ABC: Towards a Universal Code Styler through Model Merging
OOPSLA
Yitong Chen
School of Computer Science and Engineering, College of Software Engineering, School of Artificial Intelligence, Southeast University
Zhiqiang Gao
School of Computer Science and Engineering, College of Software Engineering, School of Artifical Intelligence, Southeast University
Chuanqi Shi
School of Computer Science and Engineering, College of Software Engineering, School of Artifical Intelligence, Southeast University
Baixuan Li
School of Computer Science and Engineering, College of Software Engineering, School of Artifical Intelligence, Southeast University
Miao Gao
School of Computer Science and Engineering, College of Software Engineering, School of Artifical Intelligence, Southeast University
10:45
15m
Talk
Binary Cryptographic Function Identification via Similarity Analysis with Path-insensitive Emulation
OOPSLA
Yikun Hu
Shanghai Jiao Tong University
Yituo He
Shanghai Jiao Tong University
Wenyu He
Shanghai Jiao Tong University
Haoran Li
Shanghai Jiao Tong University
Yubo Zhao
Shanghai Jiao Tong University
Shuai Wang
Hong Kong University of Science and Technology
Dawu Gu
Shanghai Jiao Tong University
11:00
15m
Talk
Boosting Program Reduction with the Missing Piece of Syntax-Guided Transformations
OOPSLA
Zhenyang Xu
University of Waterloo
Yongqiang Tian
Monash University
Mengxiao Zhang
Chengnian Sun
University of Waterloo
11:15
15m
Talk
Code Style Sheets: CSS for Code
OOPSLA
Sam Cohen
University of Chicago
Ravi Chugh
University of Chicago
11:30
15m
Talk
Enhancing APR with PRISM: A Semantic-Based Approach to Overfitting Patch Detection
OOPSLA
Dowon Song
Korea University
Hakjoo Oh
Korea University
11:45
15m
Talk
PAFL: Enhancing Fault Localizers by Leveraging Project-Specific Fault Patterns
OOPSLA
Donguk Kim
Doha Hwang
Samsung
Minseok Jeon
DGIST
Hakjoo Oh
Korea University
12:00
15m
Talk
Stencil-Lifting: Hierarchical Recursive Lifting System for Extracting Summary of Stencil Kernel in Legacy Codes
OOPSLA
Mingyi Li
Institute of Computing Technology, CAS
Junmin Xiao
Siyan Chen
Institute of Computing Technology, Chinese Academy of Sciences
Hui Ma
Institute of Computing Technology, Chinese Academy of Sciences
Xi Chen
Institute of Computing Technology, Chinese Academy of Sciences
Peihua Bao
University of Chinese Academy of Sciences
Liang Yuan
Chinese Academy of Sciences
Guangming Tan
Chinese Academy of Sciences(CAS)
10:30 - 12:15
Theory
OOPSLA
at
Orchid West
Chair(s):
Lionel Parreaux
HKUST (The Hong Kong University of Science and Technology)
10:30
15m
Talk
Automated Discovery of Tactic Libraries for Interactive Theorem Proving
OOPSLA
Yutong Xin
The University of Texas at Austin
Jimmy Xin
The University of Texas at Austin
Gabriel Poesia
Stanford University
Noah D. Goodman
Stanford University
Jocelyn Qiaochu Chen
New York University, University of Alberta
Işıl Dillig
University of Texas at Austin
10:45
15m
Talk
Choreographic Quick Changes: First-Class Location (Set) Polymorphism
OOPSLA
Ashley Samuelson
University of Wisconsin-Madison
Andrew K. Hirsch
University at Buffalo, SUNY
Ethan Cecchetti
University of Wisconsin-Madison
11:00
15m
Talk
Divide and Conquer: A Compositional Approach to Game-Theoretic Security
OOPSLA
Ivana Bocevska
TU Wien
Anja Petković Komel
Argot Collective
Laura Kovács
TU Wien
Sophie Rain
Argot Collective
Michael Rawson
University of Southampton
11:15
15m
Talk
Efficient Decrease-And-Conquer Linearizability Monitoring
OOPSLA
Zheng Han Lee
National University of Singapore, Singapore
Umang Mathur
National University of Singapore
Link to publication
DOI
Pre-print
11:30
15m
Talk
Liberating Merges via Apartness and Guarded Subtyping
OOPSLA
Han Xu
Princeton University
Xuejing Huang
IRIF
Bruno C. d. S. Oliveira
University of Hong Kong
11:45
15m
Talk
The Simple Essence of Monomorphization
OOPSLA
Matthew Lutze
Aarhus University
Philipp Schuster
University of Tübingen
Jonathan Immanuel Brachthäuser
University of Tübingen
12:00
15m
Talk
What's in the Box: Ergonomic and Expressive Capture Tracking over Generic Data Structures
OOPSLA
Yichen Xu
EPFL
Oliver Bračevac
EPFL, LAMP
Nguyen Pham
EPFL, LAMP
Martin Odersky
EPFL
Pre-print
12:15 - 13:45
Lunch
ICFP/SPLASH Catering
at
Orchid Dining Hall
12:15
90m
Lunch
Lunch
ICFP/SPLASH Catering
13:45 - 15:30
Compilation 1
OOPSLA
at
Orchid East
Chair(s):
Hidehiko Masuhara
Institute of Science Tokyo
13:45
15m
Talk
Bridging the Gap between Real-World and Formal Binary Lifting through Filtered-Simulation
OOPSLA
Jihee Park
KAIST
Insu Yun
KAIST
Sukyoung Ryu
KAIST
Link to publication
DOI
14:00
15m
Talk
Compiling Classical Sequent Calculus to Stock Hardware: The Duality of Compilation
OOPSLA
Philipp Schuster
University of Tübingen
Marius Müller
University of Tübingen
Klaus Ostermann
University of Tübingen
Jonathan Immanuel Brachthäuser
University of Tübingen
14:15
15m
Talk
HybridPersist: A Compiler Support for User-Friendly and Efficient PM Programming
OOPSLA
Yiyu Zhang
Nanjing University
Yongzhi Wang
Xidian University
Yanfeng Gao
Nanjing University
Xuandong Li
Nanjing University
Zhiqiang Zuo
Nanjing University
14:30
15m
Talk
JavART: a Lightweight Rule-Based JIT Compiler Using Translation Rules Extracted from a Learning Approach
OOPSLA
Hanzhang Wang
Fudan University, China
Wei Peng
Fudan University
Wenwen Wang
University of Georgia
Yunping Lu
Fudan University
Pen-Chung Yew
University of Minnesota at Twin Cities
Weihua Zhang
Fudan University
14:45
15m
Talk
Mind the Abstraction Gap: Bringing Equality Saturation to Real-World ML Compilers
OOPSLA
Arya Vohra
University of Chicago
Leo Seojun Lee
University of Oxford
Jakub Bachurski
University of Cambridge
Oleksandr Zinenko
Brium
Phitchaya Mangpo Phothilimthana
OpenAI
Albert Cohen
Google DeepMind
William S. Moses
University of Illinois Urbana-Champaign
15:00
15m
Talk
Scaling Optimization Over Uncertainty via Compilation
OOPSLA
Minsung Cho
John Gouwar
Northeastern University
Steven Holtzen
Northeastern University
15:15
15m
Talk
Tracing Just-in-time Compilation for Effects and Handlers
OOPSLA
Marcial Gaißert
University of Tübingen
CF Bolz-Tereick
Heinrich-Heine-Universität Düsseldorf
Jonathan Immanuel Brachthäuser
University of Tübingen
Pre-print
13:45 - 15:30
Systems
OOPSLA
at
Orchid Plenary Ballroom
Chair(s):
Matthew Flatt
University of Utah
13:45
15m
Talk
A Unifying Approach to Product Constructions for Quantitative Temporal Inference
OOPSLA
Kazuki Watanabe
National Institute of Informatics; SOKENDAI
Sebastian Junges
Radboud University
Jurriaan Rot
Radboud University Nijmegen
Ichiro Hasuo
National Institute of Informatics, Japan
14:00
15m
Talk
Contract System Metatheories à la Carte: A Transition-System View of Contracts
OOPSLA
Shu-Hung You
Institute of Information Science, Academia Sinica, Taiwan
Christos Dimoulas
Northwestern University
Robert Bruce Findler
Northwestern University
14:15
15m
Talk
Incremental Bidirectional Typing via Order Maintenance
OOPSLA
Thomas J. Porter
University of Michigan
Marisa Kirisame
University of Utah
Ivan Wei
University of Michigan
Pavel Panchekha
University of Utah
Cyrus Omar
University of Michigan
14:30
15m
Talk
The Power of Regular Constraint Propagation
OOPSLA
Matthew Hague
Royal Holloway University of London
Artur Jez
University of Wroclaw
Anthony Widjaja Lin
RPTU Kaiserslautern-Landau and Max-Planck Institute for Software Systems
Oliver Markgraf
RPTU Kaiserslautern-Landau
Philipp Ruemmer
University of Regensburg and Uppsala University
14:45
15m
Talk
Orax: A Feedback-Driven Framework for Efficiently Solving Satisfiability Modulo Theories and Oracles
OOPSLA
Zhineng Zhong
Key Laboratory of High-Confidence Software Technologies (MOE), School of Computer Science, Peking University
Ziqi Zhang
University of Illinois Urbana-Champaign
Hanqin Guan
Peking University
Ding Li
Peking University
15:00
15m
Talk
Software Model Checking via Summary-Guided Search
OOPSLA
Ruijie Fang
University of Texas at Austin
Zachary Kincaid
Princeton University
Thomas Reps
University of Wisconsin-Madison
DOI
Pre-print
13:45 - 15:30
Reasoning
OOPSLA
at
Orchid West
Chair(s):
Adam Chlipala
Massachusetts Institute of Technology
13:45
15m
Talk
Characterizing Implementability of Global Protocols with Infinite States and Data
OOPSLA
Elaine Li
NYU
Felix Stutz
University of Luxembourg, Luxembourg
Thomas Wies
New York University
Damien Zufferey
SonarSource
14:00
15m
Talk
Checking Observational Correctness of Database Systems
OOPSLA
Lauren Pick
The Chinese University of Hong Kong
Amanda Xu
University of Wisconsin-Madison
Ankush Desai
Amazon Web Services
Sanjit A. Seshia
University of California, Berkeley
Aws Albarghouthi
University of Wisconsin-Madison
14:15
15m
Talk
Correct Black-Box Monitors for Distributed Deadlock Detection: Formalisation and Implementation
OOPSLA
Radosław Jan Rowicki
Technical University of Denmark
Adrian Francalanza
University of Malta
Alceste Scalas
Technical University of Denmark
DOI
Pre-print
14:30
15m
Talk
Correct-By-Construction: Certified Individual Fairness through Neural Network Training
OOPSLA
Ruihan Zhang
Singapore Management University (SMU)
Jun Sun
Singapore Management University
14:45
15m
Talk
Modular Reasoning about Global Variables and Their Initialization
OOPSLA
João Pereira
ETH Zurich
Isaac van Bakel
ETH Zurich
Patricia Firlejczyk
ETH Zurich
Marco Eilers
ETH Zurich
Peter Müller
ETH Zurich
15:00
15m
Talk
P³: Reasoning about Patches via Product Programs
OOPSLA
Arindam Sharma
Imperial College London
Daniel Schemmel
Imperial College London
Cristian Cadar
Imperial College London
15:15
15m
Talk
Reasoning about External Calls
OOPSLA
Julian Mackay
Kry10 Ltd
Sophia Drossopoulou
Imperial College London
James Noble
Independent. Wellington, NZ
Susan Eisenbach
Imperial College London
Link to publication
DOI
Pre-print
15:30 - 16:00
Coffee break
ICFP/SPLASH Catering
at
Orchid Dining Hall
15:30
30m
Coffee break
Break
ICFP/SPLASH Catering
16:00 - 17:30
Compilation 2
OOPSLA
at
Orchid East
Chair(s):
Karine Even-Mendoza
King’s College London
16:00
15m
Talk
An Empirical Study of Bugs in the rustc Compiler
OOPSLA
Zixi Liu
Nanjing University
Yang Feng
Nanjing University
Yunbo Ni
The Chinese University of Hong Kong
Shaohua Li
The Chinese University of Hong Kong
Xizhe Yin
Nanjing University
Qingkai Shi
Nanjing University
Baowen Xu
Nanjing University
Zhendong Su
ETH Zurich
16:15
15m
Talk
DESIL: Detecting Silent Bugs in MLIR Compiler Infrastructure
OOPSLA
Chenyao Suo
Tianjin University
Jianrong Wang
Tianjin University
Yongjia Wang
College of Intelligence and Computing, Tianjin University
Jiajun Jiang
Tianjin University
Qingchao Shen
Tianjin University
Junjie Chen
Tianjin University
16:30
15m
Talk
GALA: A High Performance Graph Neural Network Acceleration LAnguage and Compiler
OOPSLA
Damitha Lenadora
University of Illinois at Urbana-Champaign
Nikhil Jayakumar
University of Texas at Austin
Chamika Sudusinghe
University of Illinois at Urbana-Champaign
Charith Mendis
University of Illinois at Urbana-Champaign
16:45
15m
Talk
Non-interference Preserving Optimising Compilation
OOPSLA
Julian Rosemann
Saarland University, Saarland Informatics Campus
Sebastian Hack
Saarland University, Saarland Informatics Campus
Deepak Garg
MPI-SWS
Link to publication
DOI
17:00
15m
Talk
Synchronized Behavior Checking: A Method for Finding Missed Compiler Optimizations
OOPSLA
Yi Zhang
Nanjing University
Yu Wang
Nanjing University
Linzhang Wang
Nanjing University
Ke Wang
Peking University
17:15
15m
Talk
Tabby: A Synthesis-Aided Compiler for High-Performance Zero-Knowledge Proof Circuits
OOPSLA
Junrui Liu
University of California, Santa Barbara
Jiaxin Song
University of Illinois at Urbana-Champaign
Yanning Chen
University of Toronto
Hanzhi Liu
University of California, Santa Barbara & Riema Labs
Hongbo Wen
University of California, Santa Barbara & Riema Labs
Luke Pearson
Polychain Capital
Yanju Chen
University of California, San Diego
Yu Feng
University of California at Santa Barbara
16:00 - 17:30
Parallelism
OOPSLA
at
Orchid Plenary Ballroom
Chair(s):
Tony Hosking
Australian National University
16:00
15m
Talk
Compressed and Parallelized Structured Tensor Algebra
OOPSLA
Mahdi Ghorbani
University of Edinburgh
Emilien Bauer
University of Edinburgh
Tobias Grosser
University of Cambridge
Amir Shaikhha
University of Edinburgh
16:15
15m
Talk
Exploring the Theory and Practice of Concurrency in the Entity-Component-System Pattern
OOPSLA
Patrick Redmond
University of California, Santa Cruz
Jonathan Castello
University of California, Santa Cruz
Jose Calderon
Galois, Inc.
Lindsey Kuper
University of California, Santa Cruz
Pre-print
16:30
15m
Talk
HieraSynth: A Parallel Framework for Complete Super-Optimization with Hierarchical Space Decomposition
OOPSLA
Sirui Lu
OpenAI
Rastislav Bodík
Google Research, Brain Team
16:45
15m
Talk
Lilo: A Higher-Order, Relational Concurrent Separation Logic for Liveness
OOPSLA
Dongjae Lee
Massachusetts Institute of Technology
Janggun Lee
KAIST
Taeyoung Yoon
Seoul National University
Minki Cho
Seoul National University
Jeehoon Kang
FuriosaAI
Chung-Kil Hur
Seoul National University
17:00
15m
Talk
Opportunistically Parallel Lambda Calculus
OOPSLA
Stephen Mell
University of Pennsylvania
Konstantinos Kallas
University of California, Los Angeles
Steve Zdancewic
University of Pennsylvania
Osbert Bastani
University of Pennsylvania
17:15
15m
Talk
Soundness of Predictive Concurrency Analyses
OOPSLA
Shuyang Liu
Doug Lea
State University of New York (SUNY) Oswego
Jens Palsberg
University of California, Los Angeles (UCLA)
Link to publication
16:00 - 17:30
Neural Network
OOPSLA
at
Orchid West
Chair(s):
Jiasi Shen
The Hong Kong University of Science and Technology
16:00
15m
Talk
Convex Hull Approximation for Activation Functions
OOPSLA
Zhongkui Ma
The University of Queensland
Zihan Wang
The University of Queensland and CSIRO's Data61
Guangdong Bai
University of Queensland
16:15
15m
Talk
Cost of Soundness in Mixed-Precision Tuning
OOPSLA
Anastasia Isychev
TU Wien
Debasmita Lohar
Karlsruhe Institute of Technology
Pre-print
16:30
15m
Talk
Finch: Sparse and Structured Tensor Programming with Control Flow
OOPSLA
Willow Ahrens
Massachusetts Institute of Technology
Teodoro F. Collin
MIT CSAIL
Radha Patel
MIT CSAIL
Kyle Deeds
University of Washington
Changwan Hong
Massachusetts Institute of Technology
Saman Amarasinghe
Massachusetts Institute of Technology
16:45
15m
Talk
MetaKernel: Enabling Efficient Encrypted Neural Network Inference Through Unified MVM and Convolution
OOPSLA
Peng Yuan
Ant Group
Yan Liu
Ant Group
Jianxin Lai
Ant Group
Long Li
Ant Group
Tianxiang Sui
Ant Group
Linjie Xiao
Ant Group
Xiaojing Zhang
Ant Group
Qing Zhu
Ant Group
Jingling Xue
University of New South Wales
17:00
15m
Talk
Quantization with Guaranteed Floating-Point Neural Network Classifications
OOPSLA
Anan Kabaha
Technion, Israel Institute of Technology
Dana Drachsler Cohen
Technion
17:15
15m
Talk
The Continuous Tensor Abstraction: Where Indices are Real
OOPSLA
Jaeyeon Won
MIT
Willow Ahrens
Massachusetts Institute of Technology
Teodoro F. Collin
MIT CSAIL
Joel S Emer
MIT/NVIDIA
Saman Amarasinghe
Massachusetts Institute of Technology
18:00 - 20:00
SPLASH Reception
Student Research Competition
ICFP/SPLASH Catering
at
Garden Walk
18:00
2h
Social Event
SPLASH SRC Poster Session
Student Research Competition
Fri 17 Oct
Displayed time zone:
Perth
change
09:00 - 10:00
Friday SPLASH Keynote
SPLASH Keynotes
at
Orchid Plenary Ballroom
Chair(s):
Charles Zhang
The Hong Kong University of Science and Technology
09:00
60m
Keynote
The Quest Toward that Perfect Compiler
SPLASH Keynotes
K:
Zhendong Su
ETH Zurich
10:00 - 10:30
Coffee break
ICFP/SPLASH Catering
at
Orchid Dining Hall
10:00
30m
Coffee break
Break
ICFP/SPLASH Catering
10:30 - 12:15
Analysis 1
OOPSLA
at
Orchid East
Chair(s):
Bor-Yuh Evan Chang
University of Colorado Boulder & Amazon
10:30
15m
Talk
Artemis: Toward Accurate Detection of Server-Side Request Forgeries through LLM-Assisted Inter-Procedural Path-Sensitive Taint Analysis
OOPSLA
Yuchen Ji
ShanghaiTech University
Ting Dai
IBM Research
Zhichao Zhou
School of Information Science and Technology, ShanghaiTech University
Yutian Tang
University of Glasgow, United Kingdom
Jingzhu He
ShanghaiTech University
10:45
15m
Talk
A Sound Static Analysis Approach to I/O API Migration
OOPSLA
Shangyu Li
The Hong Kong University of Science and Technology
Zhaoyang Zhang
The Hong Kong University of Science and Technology
Sizhe Zhong
The Hong Kong University of Science and Technology
Diyu Zhou
Peking University
Jiasi Shen
The Hong Kong University of Science and Technology
DOI
Media Attached
File Attached
11:00
15m
Talk
Automatic Linear Resource Bound Analysis for Rust via Prophecy Potentials
OOPSLA
Qihao Lian
Peking University
Di Wang
Peking University
Pre-print
11:15
15m
Talk
Denotational Foundations for Expected Cost Analysis
OOPSLA
Pedro Henrique Azevedo de Amorim
Cornell University
11:30
15m
Talk
IncIDFA: An Efficient and Generic Algorithm for Incremental Iterative Dataflow Analysis
OOPSLA
Aman Nougrahiya
IIT Madras
V Krishna Nandivada
IIT Madras
11:45
15m
Talk
Revealing Sources of (Memory) Errors via Backward Analysis
OOPSLA
Flavio Ascari
University of Pisa
Roberto Bruni
University of Pisa
Roberta Gori
Diaprtimento di Informatica, Universita' di Pisa, Italy
Francesco Logozzo
Meta
12:00
15m
Talk
Two Approaches to Fast Bytecode Frontend for Static Analysis
OOPSLA
Chenxi Li
Nanjing University, China
Haoran Lin
Nanjing University, China
Tian Tan
Nanjing University
Yue Li
Nanjing University
10:30 - 12:15
Compilation 3
OOPSLA
at
Orchid Plenary Ballroom
Chair(s):
Hidehiko Masuhara
Institute of Science Tokyo
10:30
15m
Talk
Syntactic Completions with Material Obligations
OOPSLA
David Moon
University of Michigan
Andrew Blinn
University of Michigan
Thomas J. Porter
University of Michigan
Cyrus Omar
University of Michigan
DOI
Pre-print
10:45
15m
Talk
REPTILE: Performant Tiling of Recurrences
OOPSLA
Muhammad Usman Tariq
Stanford University
Shiv Sundram
Stanford University
Fredrik Kjolstad
Stanford University
11:00
15m
Talk
SPLAT: A framework for optimised GPU code-generation for SParse reguLar ATtention
OOPSLA
Ahan Gupta
University of Illinois at Urbana-Champaign
Yueming Yuan
University of Illinois Urbana-Champaign
Devansh Jain
University of Illinois at Urbana-Champaign
Yuhao Ge
University of Illinois at Urbana-Champaign
David Aponte
Microsoft
Yanqi Zhou
Google
Charith Mendis
University of Illinois at Urbana-Champaign
11:15
15m
Talk
Statically Analyzing the Dataflow of R Programs
OOPSLA
Florian Sihler
Ulm University
Matthias Tichy
Ulm University
File Attached
11:30
15m
Talk
Static Inference of Regular Grammars for Ad Hoc Parsers
OOPSLA
Michael Schröder
TU Wien
Jürgen Cito
TU Wien
DOI
Pre-print
10:30 - 12:15
SRC Presentations
Student Research Competition
at
Orchid Small
10:30 - 12:15
Calculus
OOPSLA
at
Orchid West
Chair(s):
Limin Jia
Carnegie Mellon University
10:30
15m
Talk
Fast Client-Driven CFL-Reachability via Regularization-Based Graph Simplification
OOPSLA
Chenghang Shi
SKLP, Institute of Computing Technology, CAS
Dongjie He
Chongqing University, China
Haofeng Li
SKLP, Institute of Computing Technology, CAS
Jie Lu
SKLP, Institute of Computing Technology, CAS, China
Lian Li
Institute of Computing Technology at Chinese Academy of Sciences; University of Chinese Academy of Sciences
Jingling Xue
University of New South Wales
10:45
15m
Talk
Flexible and Expressive Typed Path Patterns for GQL
OOPSLA
Wenjia Ye
National University of Singapore
Matías Toro
University of Chile
Tomás Diaz
University of Chile
Bruno C. d. S. Oliveira
University of Hong Kong
Manuel Rigger
National University of Singapore
Claudio Gutierrez
DCC, Universidad de Chile & IMFD
Domagoj Vrgoč
Pontificia Universidad Católica de Chile & IMFD Chile
11:00
15m
Talk
Quantified Underapproximation via Labeled Bunches
OOPSLA
Lang Liu
Illinois Institute of Technology
Farzaneh Derakhshan
Illinois Institute of Technology
Limin Jia
Carnegie Mellon University
Gabriel A. Moreno
Carnegie Mellon University Software Engineering Institute
Mark Klein
Carnegie Mellon University
11:15
15m
Talk
HpC: A Calculus for Hybrid and Mobile Systems
OOPSLA
Xiong Xu
Institute of Software, Chinese Academy of Sciences
Jean-Pierre Talpin
INRIA, France
Shuling Wang
Institute of Software, Chinese Academy of Sciences
Bohua Zhan
Huawei Technologies Co., Ltd.
Xinxin Liu
Institute of software, Chinese academy of sciences
Naijun Zhan
Peking University
11:30
15m
Talk
Notions of Stack-manipulating Computation and Relative Monads
OOPSLA
Yuchen Jiang
University of Michigan
Runze Xue
University of Michigan; University of Cambridge; Indiana University
Max S. New
University of Michigan
12:15 - 13:45
Lunch
ICFP/SPLASH Catering
at
Orchid Dining Hall
12:15
90m
Lunch
Lunch
ICFP/SPLASH Catering
13:45 - 15:30
Analysis 2
OOPSLA
at
Orchid East
Chair(s):
V Krishna Nandivada
IIT Madras
13:45
15m
Talk
ApkDiffer: Accurate and Scalable Cross-Version Diffing Analysis for Android Applications
OOPSLA
Jiarun Dai
Fudan University
Mingyuan Luo
Fudan University
Yuan Zhang
Fudan University
Min Yang
Fudan University
Minghui Yang
OPPO
14:00
15m
Talk
Combining Formal and Informal Information in Bayesian Program Analysis via Soft Evidences
OOPSLA
Tianchi Li
Peking University, China
Xin Zhang
Peking University
14:15
15m
Talk
CoSSJIT: Combining Static Analysis and Speculation in JIT Compilers
OOPSLA
Aditya Anand
Indian Institute of Technology Bombay
Vijay Sundaresan
IBM Canada
Daryl Maier
IBM Canada
Manas Thakur
IIT Bombay
14:30
15m
Talk
On Abstraction Refinement for Bayesian Program Analysis
OOPSLA
Yuanfeng Shi
Peking University
Yifan Zhang
Peking University
Xin Zhang
Peking University
14:45
15m
Talk
Sound and Modular Activity Analysis for Automatic Differentiation in MLIR
OOPSLA
Mai Jacob Peng
McGill University
William S. Moses
University of Illinois Urbana-Champaign
Oleksandr Zinenko
Brium
Christophe Dubach
McGill University
15:00
15m
Talk
Towards a Theoretically-Backed and Practical Framework for Selective Object-Sensitive Pointer Analysis
OOPSLA
Chaoyue Zhang
Nanjing University
Longlong Lu
State Key Laboratory for Novel Software Technology, Nanjing University, China
Yifei Lu
State Key Laboratory for Novel Software Technology, Nanjing University, China
Minxue Pan
Nanjing University
Xuandong Li
Nanjing University
15:15
15m
Talk
Universal Scalability in Declarative Program Analysis (with Choice-Based Combination Pruning)
OOPSLA
Anastasios Antoniadis
University of Athens, Greece
Ilias Tsatiris
Dedaub
Neville Grech
Dedaub Limited
Yannis Smaragdakis
University of Athens
Link to publication
DOI
13:45 - 15:30
Testing 1
OOPSLA
at
Orchid Plenary Ballroom
Chair(s):
Karine Even-Mendoza
King’s College London
13:45
15m
Talk
An Empirical Evaluation of Property-Based Testing in Python
OOPSLA
Savitha Ravi
UC San Diego
Michael Coblenz
University of California, San Diego
Link to publication
14:00
15m
Talk
Fray: An Efficient General-Purpose Concurrency Testing Platform for the JVM
OOPSLA
Ao Li
Carnegie Mellon University
Byeongjee Kang
Carnegie Mellon University
Vasudev Vikram
Carnegie Mellon University
Isabella Laybourn
Carnegie Mellon University
Samvid Dharanikota
Efficient Computer
Shrey Tiwari
Carnegie Mellon University
Rohan Padhye
Carnegie Mellon University
Pre-print
Media Attached
14:15
15m
Talk
Fuzzing C++ Compilers via Type-Driven Mutation
OOPSLA
Bo Wang
Beijing Jiaotong University
Chong Chen
Beijing Jiaotong University
Ming Deng
Beijing Jiaotong University
Junjie Chen
Tianjin University
Xing Zhang
Peking University
Youfang Lin
Beijing Jiaotong University
Dan Hao
Peking University
Jun Sun
Singapore Management University
14:30
15m
Talk
Interleaving Large Language Models for Compiler Testing
OOPSLA
Yunbo Ni
The Chinese University of Hong Kong
Shaohua Li
The Chinese University of Hong Kong
14:45
15m
Talk
Model-guided Fuzzing of Distributed Systems
OOPSLA
Ege Berkay Gulcan
Delft University of Technology
Burcu Kulahcioglu Ozkan
Delft University of Technology
Rupak Majumdar
MPI-SWS
Srinidhi Nagendra
IRIF, Chennai Mathematical Institute
15:00
15m
Talk
Tuning Random Generators: Property-Based Testing as Probabilistic Programming
OOPSLA
Ryan Tjoa
University of Washington; Jane Street
Poorva Garg
University of California, Los Angeles
Harrison Goldstein
University at Buffalo, the State University of New York at Buffalo
Todd Millstein
University of California at Los Angeles
Benjamin C. Pierce
University of Pennsylvania
Guy Van den Broeck
University of California at Los Angeles
DOI
Pre-print
15:15
15m
Talk
Understanding and Improving Flaky Test Classification
OOPSLA
Shanto Rahman
The University of Texas at Austin
Saikat Dutta
Cornell University
August Shi
The University of Texas at Austin
13:45 - 15:30
Semantics
OOPSLA
at
Orchid Small
Chair(s):
Hakjoo Oh
Korea University
13:45
15m
Talk
A complete formal semantics of eBPF instruction set architecture for Solana
OOPSLA
Shenghao Yuan
Zhejiang University
Zhuoruo Zhang
Zhejiang University
Jiayi Lu
Zhejiang University
David Sanan
Singapore Institute of Technology
Rui Chang
Zhejiang University
Yongwang Zhao
Zhejiang University
14:00
15m
Talk
Adequacy for Algebraic Effects Revisited
OOPSLA
Alex Kavvos
University of Bristol
14:15
15m
Talk
A Mechanized Semantics for Dataflow Circuits
OOPSLA
Tony Law
Univ Rennes, Inria, CNRS, IRISA
Delphine Demange
Univ Rennes, Inria, CNRS, IRISA
Sandrine Blazy
University of Rennes
14:30
15m
Talk
Dynamic Wind for Effect Handlers
OOPSLA
David Voigt
University of Tübingen
Philipp Schuster
University of Tübingen
Jonathan Immanuel Brachthäuser
University of Tübingen
Pre-print
14:45
15m
Talk
React-tRace: A Semantics for Understanding React Hooks
OOPSLA
Jay Lee
Seoul National University
Joongwon Ahn
Seoul National University
Kwangkeun Yi
Seoul National University
Link to publication
DOI
15:00
15m
Talk
Semantics of Sets of Programs
OOPSLA
Jinwoo Kim
University of Wisconsin-Madison; Seoul National University
Shaan Nagy
University of Wisconsin-Madison
Thomas Reps
University of Wisconsin-Madison
Loris D'Antoni
University of California at San Diego
15:15
15m
Talk
Zero-Overhead Lexical Effect Handlers
OOPSLA
Cong Ma
University of Waterloo
Zhaoyi Ge
University of Waterloo
Jonghyun Jung
University of Waterloo
Yizhou Zhang
University of Waterloo
13:45 - 15:30
Type 1
OOPSLA
at
Orchid West
Chair(s):
Lionel Parreaux
HKUST (The Hong Kong University of Science and Technology)
13:45
15m
Talk
A Lightweight Type-and-Effect System for Invalidation Safety: Tracking Permanent and Temporary Invalidation With Constraint-Based Subtype Inference
OOPSLA
Cunyuan Gao
HKUST
Lionel Parreaux
HKUST (The Hong Kong University of Science and Technology)
DOI
14:00
15m
Talk
MTP: A Meaning-Typed Language Abstraction for AI-Integrated Programming
OOPSLA
Jayanaka Dantanarayana
University of Michigan
Yiping Kang
University of Michigan
Kugesan Sivasothynathan
Jaseci Labs
Christopher Clarke
University of Michigan
Baichuan Li
University of Michigan
Savini Kashmira
University of Michigan
Krisztian Flautner
University of Michigan
Lingjia Tang
University of Michigan
Jason Mars
University of Michigan
14:15
15m
Talk
Modeling Reachability Types with Logical Relations -- Semantic Type Soundness, Termination, Effect Safety, and Equational Theory
OOPSLA
Yuyan Bao
Augusta University
Songlin Jia
Purdue University, USA
Guannan Wei
Tufts University
Oliver Bračevac
EPFL, LAMP
Tiark Rompf
Purdue University
14:30
15m
Talk
Qualified Types with Boolean Algebras
OOPSLA
Edward Lee
University of Toronto at Scarborough
Jonathan Lindegaard Starup
Ondřej Lhoták
University of Waterloo
Magnus Madsen
Aarhus University
14:45
15m
Talk
RestPi: Path-Sensitive Type Inference for REST APIs
OOPSLA
Mark W. Aldrich
Tufts University
Kyla H. Levin
University of Massachusetts Amherst, USA
Michael Coblenz
University of California, San Diego
Jeffrey S. Foster
Tufts University
15:00
15m
Talk
Type-Outference with Label-Listeners: Foundations for Decidable Type-Consistency for Nominal Object-Oriented Generics
OOPSLA
Ross Tate
Independent Researcher and Consultant
DOI
Pre-print
15:15
15m
Talk
Type-Preserving Flat Closure Optimization
OOPSLA
Adam T. Geller
University of British Columbia
Sean Bocirnea
University of British Columbia
Chester Gould
University of British Columbia
Paulette Koronkevich
University of British Columbia
William J. Bowman
University of British Columbia
DOI
15:30 - 16:00
Coffee break
ICFP/SPLASH Catering
at
Orchid Dining Hall
15:30
30m
Coffee break
Break
ICFP/SPLASH Catering
16:00 - 17:30
Verification 1
OOPSLA
at
Orchid East
Chair(s):
Limin Jia
Carnegie Mellon University
16:00
15m
Talk
A Flow-Sensitive Refinement Type System for Verifying eBPF Programs
OOPSLA
Ameer Hamza
Florida State University
Lucas Zavalia
Florida State University Tallahassee
Arie Gurfinkel
University of Waterloo
Jorge A. Navas
Certora
Grigory Fedyukovich
Florida State University
16:15
15m
Talk
Automatically Verifying Replication-aware Linearizability
OOPSLA
Vimala Soundarapandian
IIT Madras
Kartik Nagar
IIT Madras
Aseem Rastogi
Microsoft Research
KC Sivaramakrishnan
IIT Madras and Tarides
Link to publication
DOI
Media Attached
16:30
15m
Talk
On the Impact of Formal Verification on Software Development
OOPSLA
Eric Mugnier
University of California San Diego
Zhou Yuanyuan
UCSD
Ranjit Jhala
University of California at San Diego
Michael Coblenz
University of California, San Diego
16:45
15m
Talk
Towards Verifying Crash Consistency
OOPSLA
Keonho Lee
University of California, Irvine
Conan Truong
University of California, Irvine
Brian Demsky
University of California at Irvine
17:00
15m
Talk
TraceLinking Implementations with their Verified Designs
OOPSLA
Finn Hackett
University of British Columbia
Ivan Beschastnikh
The University of British Columbia
Pre-print
17:15
15m
Talk
Pyrosome: Verified Compilation for Modular Metatheory
OOPSLA
Dustin Jamner
MIT CSAIL
Gabriel Kammer
MIT
Ritam Nag
MIT
Adam Chlipala
MIT CSAIL
16:00 - 17:30
Testing 2
OOPSLA
at
Orchid Plenary Ballroom
Chair(s):
Owolabi Legunsen
Cornell University
16:00
15m
Talk
Bennet: Randomized Specification Testing for Heap-Manipulating Programs
OOPSLA
Zain K Aamer
University of Pennsylvania
Benjamin C. Pierce
University of Pennsylvania
16:15
15m
Talk
DepFuzz: Efficient Smart Contract Fuzzing with Function Dependence Guidance
OOPSLA
Chenyang Ma
Nanjing University of Science and Technology
Wei Song
Nanjing University of Science and Technology
Jeff Huang
Texas A&M University
DOI
16:30
15m
Talk
Extraction and Mutation at a High Level: Template-Based Fuzzing for JavaScript Engines
OOPSLA
Wai Kin Wong
Hong Kong University of Science and Technology
Dongwei Xiao
Hong Kong University of Science and Technology
Cheuk Tung LAI
VX Research Limited
Yiteng Peng
Hong Kong University of Science and Technology
Daoyuan Wu
Lingnan University
Shuai Wang
Hong Kong University of Science and Technology
16:45
15m
Talk
Finding Compiler Bugs through Cross-Language Code Generator and Differential Testing
OOPSLA
Qiong Feng
Nanjing University of Science and Technology
Xiaotian Ma
Nanjing University of Science and Technology
Ziyuan Feng
Nanjing University of Science and Technology
Marat Akhin
JetBrains
Wei Song
Nanjing University of Science and Technology
Peng Liang
Wuhan University, China
DOI
17:00
15m
Talk
Formalizing Linear Motion G-code for Invariant Checking and Differential Testing of Fabrication Tools
OOPSLA
Yumeng He
University of Utah
Chandrakana Nandi
Certora
Sreepathi Pai
University of Rochester
16:00 - 17:30
Debugging and Validation
OOPSLA
at
Orchid Small
Chair(s):
Stefan Marr
Johannes Kepler University Linz
16:00
15m
Talk
Debugging WebAssembly? Put some Whamm on it!
OOPSLA
Elizabeth Gilbert
Carnegie Mellon University
Matthew Schneider
Carnegie Mellon University
Zixi An
Suhas Thalanki
Carnegie Mellon University
Wavid Bowman
University of Florida
Alexander Bai
New York University
Ben L. Titzer
Carnegie Mellon University
Heather Miller
Carnegie Mellon University and Two Sigma
Link to publication
DOI
Pre-print
16:15
15m
Talk
MIO: Multiverse Debugging in the face of Input/Output
OOPSLA
Tom Lauwaerts
Universiteit Gent, Belgium
Maarten Steevens
Ghent University, Belgium
Christophe Scholliers
Universiteit Gent, Belgium
Link to publication
DOI
Pre-print
16:30
15m
Talk
PReMM: LLM-Based Program Repair for Multi-Method Bugs via Divide and Conquer
OOPSLA
Linna Xie
Nanjing University
Zhong Li
Nanjing University
Yu Pei
Hong Kong Polytechnic University
Zhongzhen Wen
Nanjing University
Kui Liu
Huawei
Tian Zhang
Nanjing University
Xuandong Li
Nanjing University
16:45
15m
Talk
Show Me Why It's Correct: Saving 1/3 of Debugging Time in Program Repair with Interactive Runtime Comparison
OOPSLA
Ruixin Wang
Purdue University
Zhongkai Zhao
National University of Singapore
Le Fang
Purdue University
Nan Jiang
Purdue University
Yiling Lou
University of Illinois at Urbana-Champaign
Lin Tan
Purdue University
Tianyi Zhang
Purdue University
Link to publication
DOI
Pre-print
17:00
15m
Talk
Translation Validation for LLVM's AArch64 Backend
OOPSLA
Ryan Berger
Nvidia
Mitch Briles
University of Utah
Nader Boushehrinejad Moradi
University of Utah
Nicholas Coughlin
Defence Science and Technology Group, Australia
Kait Lam
Defence Science and Technology Group / School of EECS, University of Queensland
Nuno P. Lopes
INESC-ID; Instituto Superior Técnico - University of Lisbon
Stefan Mada
University of Utah
Tanmay Tirpankar
University of Utah
John Regehr
University of Utah
17:15
15m
Talk
Validating SMT Rewriters via Rewrite Space Exploration Supported by Generative Equality Saturation
OOPSLA
Maolin Sun
Nanjing University
Yibiao Yang
Nanjing University
Jiangchang Wu
Nanjing University
Yuming Zhou
Nanjing University
16:00 - 17:30
Languages
OOPSLA
at
Orchid West
Chair(s):
Bruno C. d. S. Oliveira
University of Hong Kong
16:00
15m
Talk
A Domain-Specific Probabilistic Programming Language for Reasoning about Reasoning (or: a memo on memo)
OOPSLA
Kartik Chandra
MIT
Tony Chen
MIT
Joshua B. Tenenbaum
Massachusetts Institute of Technology
Jonathan Ragan-Kelley
Massachusetts Institute of Technology
16:15
15m
Talk
ROSpec: A Domain-Specific Language for ROS-based Robot Software
OOPSLA
Paulo Canelas
Carnegie Mellon University
Bradley Schmerl
School of Computer Science, Carnegie Mellon University
Alcides Fonseca
LASIGE; University of Lisbon
Christopher Steven Timperley
Carnegie Mellon University
DOI
Pre-print
Media Attached
16:30
15m
Talk
Large Language Model powered Symbolic Execution
OOPSLA
Yihe Li
National University of Singapore
Ruijie Meng
National University of Singapore, Singapore
Gregory J. Duck
National University of Singapore
16:45
15m
Talk
Multi-Language Probabilistic Programming
OOPSLA
Sam Stites
Northeastern University
John Li
Northeastern University
Steven Holtzen
Northeastern University
17:00
15m
Talk
Polymorphic Records for Dynamic Languages
OOPSLA
Giuseppe Castagna
CNRS; Université Paris Cité
Loïc Peyrot
IMDEA Software Institute
17:30 - 18:15
SPLASH Organisers Discussion and AMA (and Awards)
OOPSLA
at
Orchid Plenary Ballroom
After a quick awards session, SPLASH Steering Committee Chair (Alex Potanin) and the current OOPSLA RC Co-Chairs (Shriram Krishnamurthi and Sukyoung Ryu) will hold “Ask Me Anything” session seeking feedback from the community on the future of SPLASH, OOPSLA, and other events that form SPLASH:
17:30
10m
Awards
OOPSLA Awards
OOPSLA
Shriram Krishnamurthi
Brown University
Sukyoung Ryu
KAIST
17:40
35m
Meeting
SPLASH Organisers Discussion and AMA
OOPSLA
C:
Alex Potanin
Australian National University
Sat 18 Oct
Displayed time zone:
Perth
change
09:00 - 10:00
Saturday SPLASH Keynote
SPLASH Keynotes
at
Orchid Plenary Ballroom
Chair(s):
Shriram Krishnamurthi
Brown University
09:00
60m
Keynote
Software Stacks for Confidential Computing Hardware
SPLASH Keynotes
K:
Frank Piessens
KU Leuven
10:00 - 10:30
Coffee break
ICFP/SPLASH Catering
at
Orchid Dining Hall
10:00
30m
Coffee break
Break
ICFP/SPLASH Catering
10:30 - 12:15
Type 2
OOPSLA
at
Orchid East
Chair(s):
Richard A. Eisenberg
Jane Street
10:30
15m
Talk
Borrowing From Session Types
OOPSLA
Hannes Saffrich
University of Freiburg
Janek Spaderna
University of Freiburg, Germany
Peter Thiemann
University of Freiburg
Vasco T. Vasconcelos
LASIGE, University of Lisbon
10:45
15m
Talk
Modal Effect Types
OOPSLA
Wenhao Tang
The University of Edinburgh
Leo White
Jane Street
Stephen Dolan
Jane Street
Daniel Hillerström
Category Labs and The University of Edinburgh
Sam Lindley
University of Edinburgh
Anton Lorenzen
University of Edinburgh
11:00
15m
Talk
On Higher-Order Model Checking of Effectful Answer-Type-Polymorphic Programs
OOPSLA
Taro Sekiyama
National Institute of Informatics
Ugo Dal Lago
University of Bologna & INRIA Sophia Antipolis
Hiroshi Unno
Tohoku University
11:15
15m
Talk
Proof Repair across Quotient Type Equivalences
OOPSLA
Cosmo Viola
University of Illinois Urbana-Champaign
Max Fan
Cornell University
Talia Lily Ringer
University of Illinois Urbana-Champaign
11:30
15m
Talk
Structural Information Flow: A Fresh Look at Types for Non-Interference
OOPSLA
Hemant Gouni
Carnegie Mellon University
Frank Pfenning
Carnegie Mellon University, USA
Jonathan Aldrich
Carnegie Mellon University
Pre-print
11:45
15m
Talk
The Simple Essence of Overloading: Making ad-hoc polymorphism more algebraic with flow-based variational type-checking
OOPSLA
Jiří Beneš
University of Tübingen
Jonathan Immanuel Brachthäuser
University of Tübingen
DOI
Pre-print
12:00
15m
Talk
We’ve Got You Covered: Type-Guided Repair of Incomplete Input Generators
OOPSLA
Patrick LaFontaine
Purdue University
Zhe Zhou
Purdue University
Ashish Mishra
IIT Hyderabad
Suresh Jagannathan
Purdue University
Benjamin Delaware
Purdue University
10:30 - 12:15
Synthesis 1
OOPSLA
at
Orchid Plenary Ballroom
Chair(s):
Yingfei Xiong
Peking University
10:30
15m
Talk
Abstraction Refinement-guided Program Synthesis for Robot Learning from Demonstrations
OOPSLA
Guofeng Cui
Rutgers University
Yuning Wang
Rutgers University
Wensen Mao
Rutgers University
Yuanlin Duan
Rutgers University
He Zhu
Rutgers University, USA
10:45
15m
Talk
API-guided Dataset Synthesis to Finetune Large Code Models
OOPSLA
Li Zongjie
Hong Kong University of Science and Technology
Daoyuan Wu
Lingnan University
Shuai Wang
Hong Kong University of Science and Technology
Zhendong Su
ETH Zurich
11:00
15m
Talk
Fast Constraint Synthesis for C++ Function Templates
OOPSLA
Shuo Ding
Georgia Institute of Technology
Qirun Zhang
Georgia Institute of Technology
11:15
15m
Talk
Hambazi: Spatial Coordination Synthesis for Augmented Reality
OOPSLA
Yi-Zhen Tsai
University of California, Riverside
Jiasi Chen
University of Michigan
Mohsen Lesani
University of California at Santa Cruz
11:30
15m
Talk
Inductive Synthesis of Inductive Heap Predicates
OOPSLA
Ziyi Yang
National University of Singapore
Ilya Sergey
National University of Singapore
11:45
15m
Talk
LOUD: Synthesizing Strongest and Weakest Specifications
OOPSLA
Kanghee Park
University of Wisconsin-Madison
Xuanyu Peng
University of California, San Diego
Loris D'Antoni
University of California at San Diego
12:00
15m
Talk
Metamorph: Synthesizing Large Objects from Dafny Specifications
OOPSLA
Aleksandr Fedchin
Tufts University
Alexander Bai
New York University
Jeffrey S. Foster
Tufts University
10:30 - 12:15
Quantum
OOPSLA
at
Orchid Small
Chair(s):
Jens Palsberg
University of California, Los Angeles (UCLA)
10:30
15m
Talk
AccelerQ: Accelerating Quantum Eigensolvers With Machine Learning on Quantum Simulators
OOPSLA
Avner Bensoussan
King's College London
Elena Chachkarova
Kings College London
Karine Even-Mendoza
King’s College London
Sophie Fortz
King's College London
Connor Lenihan
King's College London
10:45
15m
Talk
A Language for Quantifying Quantum Network Behavior
OOPSLA
Anita Buckley
USI Lugano
Pavel Chuprikov
Télécom Paris, Institut Polytechnique de Paris
Rodrigo Otoni
USI Lugano
Robert Soulé
Yale University
Robert Rand
University of Chicago
Patrick Eugster
USI Lugano, Switzerland
11:00
15m
Talk
Compositional Quantum Control Flow with Efficient Compilation in Qunity
OOPSLA
Mikhail Mints
California Institute of Technology
Finn Voichick
University of Maryland
Leonidas Lampropoulos
University of Maryland, College Park
Robert Rand
University of Chicago
11:15
15m
Talk
Dependency-Aware Compilation for Surface Code Quantum Architectures
OOPSLA
Abtin Molavi
University of Wisconsin-Madison
Amanda Xu
University of Wisconsin-Madison
Swamit Tannu
University of Wisconsin-Madison
Aws Albarghouthi
University of Wisconsin-Madison
11:30
15m
Talk
QbC: Quantum Correctness by Construction
OOPSLA
Anurudh Peduri
Ruhr University Bochum
Ina Schaefer
KIT
Michael Walter
Ruhr-Universität Bochum
11:45
15m
Talk
qblaze: An Efficient and Scalable Sparse Quantum Simulator
OOPSLA
Hristo Venev
INSAIT, Sofia University "St. Kliment Ohridski"
Thien Udomsrirungruang
University of Oxford
Dimitar Dimitrov
INSAIT, Sofia University "St. Kliment Ohridski"
Timon Gehr
ETH Zurich
Martin Vechev
ETH Zurich
12:00
15m
Talk
Shaking Up Quantum Simulators with Fuzzing and Rigour
OOPSLA
Vasileios Klimis
Queen Mary University of London
Karine Even-Mendoza
King’s College London
Avner Bensoussan
King's College London
Elena Chachkarova
Kings College London
Sophie Fortz
King's College London
Connor Lenihan
King's College London
10:30 - 12:15
Verification 2
OOPSLA
at
Orchid West
Chair(s):
Sukyoung Ryu
KAIST
10:30
15m
Talk
FO-Complete Program Verification for Heap Logics
OOPSLA
Adithya Murali
University of Illinois at Urbana-Champaign
Hrishikesh Balakrishnan
University of Illinois Urbana-Champaign
Aaron Councilman
Univ of Illinois Urbana-Champaign
P. Madhusudan
University of Illinois at Urbana-Champaign
10:45
15m
Talk
Foundations for Deductive Verification of Continuous Probabilistic Programs: From Lebesgue to Riemann and Back
OOPSLA
Kevin Batz
RWTH Aachen University
Joost-Pieter Katoen
RWTH Aachen University
Francesca Randone
Department of Mathematics, Informatics and Geosciences, University of Trieste, Italy
Tobias Winkler
RWTH Aachen University
11:00
15m
Talk
Guarding the Privacy of Label-Only Access to Neural Network Classifiers via Formal Verification
OOPSLA
Anan Kabaha
Technion, Israel Institute of Technology
Dana Drachsler Cohen
Technion
11:15
15m
Talk
KestRel: Relational Verification Using E-Graphs for Program Alignment
OOPSLA
Robert Dickerson
Purdue University
Prasita Mukherjee
Purdue University
Benjamin Delaware
Purdue University
11:30
15m
Talk
Laurel: Unblocking Automated Verification with Large Language Models
OOPSLA
Eric Mugnier
University of California San Diego
Emmanuel Anaya Gonzalez
UCSD
Nadia Polikarpova
University of California at San Diego
Ranjit Jhala
University of California at San Diego
Zhou Yuanyuan
UCSD
11:45
15m
Talk
Scaling Instruction-Selection Verification against Authoritative ISA Semantics
OOPSLA
Michael McLoughlin
Carnegie Mellon University
Ashley Sheng
Wellesley College
Chris Fallin
F5
Bryan Parno
Carnegie Mellon University
Fraser Brown
CMU
Alexa VanHattum
Wellesley College
DOI
12:00
15m
Talk
Verification of Bit-Flip Attacks against Quantized Neural Networks
OOPSLA
Yedi Zhang
National University of Singapore
Lei Huang
ShanghaiTech University
Pengfei Gao
ByteDance
Fu Song
Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences; Nanjing Institute of Software Technology
Jun Sun
Singapore Management University
Jin Song Dong
National University of Singapore
12:15 - 13:45
Lunch
ICFP/SPLASH Catering
at
Orchid Dining Hall
12:15
90m
Lunch
Lunch
ICFP/SPLASH Catering
13:45 - 15:30
Memory
OOPSLA
at
Orchid East
Chair(s):
Manuel Serrano
Inria; Université Côte d’Azur
13:45
15m
Talk
Compositional Symbolic Execution for the Next 700 Memory Models
OOPSLA
Andreas Lööw
Imperial College London
Seung Hoon Park
Imperial College London
Daniele Nantes-Sobrinho
Imperial College London
Sacha-Élie Ayoun
Imperial College London
Opale Sjöstedt
Imperial College London
Philippa Gardner
Imperial College London
Link to publication
DOI
Pre-print
14:00
15m
Talk
Destination calculus: A linear λ-calculus for purely functional memory writes
OOPSLA
Thomas BAGREL
Tweag, LORIA/INRIA
Arnaud Spiwack
Tweag
Link to publication
DOI
Pre-print
Media Attached
14:15
15m
Talk
Divining Profiler Accuracy: An Approach to Approximate Profiler Accuracy Through Machine Code-Level Slowdown
OOPSLA
Humphrey Burchell
University of Kent
Stefan Marr
Johannes Kepler University Linz
DOI
Pre-print
14:30
15m
Talk
HeapBuffers: Why not just using a binary serialization format for your managed memory?
OOPSLA
Daniele Bonetta
VU Amsterdam
Júnior Löff
Università della Svizzera italiana
Matteo Basso
Università della Svizzera italiana (USI)
Walter Binder
USI Lugano
14:45
15m
Talk
im2im: Automatically Converting In-Memory Image Representations using A Knowledge Graph Approach
OOPSLA
Fei Chen
German Research Center for Artificial Intelligence (DFKI), Saarland University
Sunita Saha
German Research Center for Artificial Intelligence (DFKI), Saarbrücken, Germany
Manuela Schuler
German Research Center for Artificial Intelligence (DFKI), Saarbrücken, Germany; Saarland University, Saarbrücken, Germany
Philipp Slusallek
DFKI, Germany
Tim Dahmen
Aalen University, Aalen, Germany; German Research Center for Artificial Intelligence (DFKI), Saarbrücken, Germany
15:00
15m
Talk
SafeRace: Assessing and Addressing WebGPU Memory Safety in the Presence of Data Races
OOPSLA
Reese Levine
Ashley Lee
University of California, Santa Cruz
Neha Abbas
University of California, Santa Cruz
Kyle Little
University of Utah
Tyler Sorensen
Microsoft Research and University of California at Santa Cruz
15:15
15m
Talk
Symbolic MRD: Dynamic Memory, Undefined Behaviour, and Extrinsic Choice
OOPSLA
Jay Richards
University of Kent
Daniel Wright
University of Surrey
Simon Cooksey
Mark Batty
University of Kent
13:45 - 15:30
Synthesis 2
OOPSLA
at
Orchid Plenary Ballroom
Chair(s):
Jeffrey S. Foster
Tufts University
13:45
15m
Talk
Tunneling Through the Hill: Multi-Way Intersection for Version-Space Algebras in Program Synthesis
OOPSLA
Guanlin Chen
Peking University
Ruyi Ji
Peking University
Shuhao Zhang
Peking University
Yingfei Xiong
Peking University
DOI
14:00
15m
Talk
Language-Parametric Reference Synthesis
OOPSLA
Daniel A. A. Pelsmaeker
Delft University of Technology, Netherlands
Aron Zwaan
Delft University of Technology
Casper Bach
University of Southern Denmark
Arjan J. Mooij
Zürich University of Applied Sciences
14:15
15m
Talk
UTFix: Change Aware Unit Test Repairing using LLM
OOPSLA
Shanto Rahman
The University of Texas at Austin
Sachit Kuhar
Amazon Web Services
Berk Cirisci
Amazon Web Services
Pranav Garg
AWS
Shiqi Wang
AWS AI Labs
Xiaofei Ma
AWS AI Labs
Anoop Deoras
AWS AI Labs
Baishakhi Ray
Columbia University
14:30
15m
Talk
Synthesizing DSLs for Few-Shot Learning
OOPSLA
Paul Krogmeier
University of Illinois at Urbana-Champaign
P. Madhusudan
University of Illinois at Urbana-Champaign
14:45
15m
Talk
Synthesizing Implication Lemmas for Interactive Theorem Proving
OOPSLA
Ana Brendel
University of California Los Angeles
Aishwarya Sivaraman
Meta
Todd Millstein
University of California at Los Angeles
15:00
15m
Talk
Synthesizing Sound and Precise Abstract Transformers for Nonlinear Hyperbolic PDE Solvers
OOPSLA
Jacob Laurel
Georgia Institute of Technology
Ignacio Laguna
Lawrence Livermore National Laboratory
Jan Hueckelheim
Argonne National Laboratory
13:45 - 15:30
Proofs
OOPSLA
at
Orchid Small
Chair(s):
Peter Thiemann
University of Freiburg
13:45
15m
Talk
Adaptive Shielding via Parametric Safety Proofs
OOPSLA
Yao Feng
Tsinghua University
Jun Zhu
Nankai University
André Platzer
Karlsruhe Institute of Technology (KIT)
Jonathan Laurent
Carnegie Mellon University / Karlsruhe Institute of Technology
14:00
15m
Talk
Certified Decision Procedures for Width-Independent Bitvector Predicates
OOPSLA
Siddharth Bhat
University of Cambridge
Leo Stefanesco
University of Cambridge
Chris Hughes
Independent Researcher
Tobias Grosser
University of Cambridge
14:15
15m
Talk
Checking $\delta$-Satisfiability of Reals with Integrals
OOPSLA
Cody Rivera
University of Illinois, Urbana-Champaign
Bishnu Bhusal
University of Missouri
Rohit Chadha
University of Missouri
A. Prasad Sistla
University of Illinois at Chicago
Mahesh Viswanathan
University of Illinois at Urbana-Champaign
14:30
15m
Talk
Coinductive Proofs of Regular Expression Equivalence in Zero Knowledge
OOPSLA
John C. Kolesar
Yale University
Shan Ali
Yale University
Timos Antonopoulos
Yale University
Ruzica Piskac
Yale University
14:45
15m
Talk
Incremental Certified Programming
OOPSLA
Tomás Diaz
University of Chile
Kenji Maillard
Inria – LS2N, Université de Nantes
Nicolas Tabareau
Inria
Éric Tanter
University of Chile
15:00
15m
Talk
Pathological Cases for a Class of Reachability-Based Garbage Collectors
OOPSLA
Matthew Sotoudeh
Stanford University
Link to publication
15:15
15m
Talk
SafeTree: Expressive Tree Policies for Microservices
OOPSLA
Karuna Grewal
Cornell University
Brighten Godfrey
UIUC and Broadcom
Justin Hsu
Cornell University
13:45 - 15:30
Verification 3
OOPSLA
at
Orchid West
Chair(s):
KC Sivaramakrishnan
IIT Madras and Tarides
13:45
15m
Talk
Automated Verification of Soundness of DNN Certifiers
OOPSLA
Avaljot Singh
UIUC
Yasmin Chandini Sarita
UIUC
Charith Mendis
University of Illinois at Urbana-Champaign
Gagandeep Singh
University of Illinois at Urbana-Champaign; VMware Research
14:00
15m
Talk
Bolt-On Strong Consistency: Specification, Implementation, and Verification
OOPSLA
Nicholas V. Lewchenko
University of Colorado Boulder
Gowtham Kaki
University of Colorado at Boulder
Bor-Yuh Evan Chang
University of Colorado Boulder & Amazon
14:15
15m
Talk
Memory-Safety Verification of Open Programs With Angelic Assumptions
OOPSLA
Gourav Takhar
Indian Institute of Technology - Kanpur
Baldip Bijlani
Indian Institute of Technology Kanpur
Prantik Chatterjee
MathWorks
Akash Lal
Microsoft Research
Subhajit Roy
IIT Kanpur
14:30
15m
Talk
Mini-Batch Robustness Verification of Deep Neural Networks
OOPSLA
Saar Tzour-Shaday
Technion – Israel Institute of Technology
Dana Drachsler Cohen
Technion
14:45
15m
Talk
Revamping Verilog Semantics for Foundational Verification
OOPSLA
Joonwon Choi
Amazon Web Services
Jaewoo Kim
KAIST
Jeehoon Kang
FuriosaAI
15:00
15m
Talk
Scalable Equivalence Checking and Verification of Shallow Quantum Circuits
OOPSLA
Nengkun Yu
Stony Brook University, USA
Xuan Du Trinh
Stony Brook University
Thomas Reps
University of Wisconsin-Madison
15:15
15m
Talk
Structural temporal logic for mechanized program verification
OOPSLA
Lef Ioannidis
University of Pennsylvania
Yannick Zakowski
Inria
Steve Zdancewic
University of Pennsylvania
Sebastian Angel
University of Pennsylvania
15:30 - 16:00
Coffee break
ICFP/SPLASH Catering
at
Orchid Dining Hall
15:30
30m
Coffee break
Break
ICFP/SPLASH Catering
16:00 - 17:30
Abstraction
OOPSLA
at
Orchid East
Chair(s):
Steve Blackburn
Google and Australian National University
16:00
15m
Talk
Abstract Interpretation of Temporal Safety Effects of Higher Order Programs
OOPSLA
Mihai Nicola
Stevens Institute of Technology
Chaitanya Agarwal
New York University
Eric Koskinen
Stevens Institute of Technology
Thomas Wies
New York University
16:15
15m
Talk
A Hoare Logic For Symmetry Properties
OOPSLA
Vaibhav Mehta
Cornell University
Justin Hsu
Cornell University
16:30
15m
Talk
Efficient Abstract Interpretation via Selective Widening
OOPSLA
Jiawei Wang
UNSW
Xiao Cheng
Macquarie University
Yulei Sui
University of New South Wales
16:45
15m
Talk
Encode the $\forall\exists$ Relational Hoare Logic into Standard Hoare Logic
OOPSLA
Shushu Wu
Shanghai Jiao Tong University
Xiwei Wu
Shanghai Jiao Tong University
Qinxiang Cao
Shanghai Jiao Tong University
17:00
15m
Talk
Structural Abstraction and Refinement for Probabilistic Programs
OOPSLA
Guanyan Li
University of Oxford
Juanen Li
Beijing Normal University
Zhilei Han
Tsinghua University
Peixin Wang
East China Normal University
Hongfei Fu
Shanghai Jiao Tong University
Fei He
Tsinghua University
17:15
15m
Talk
Work Packets: A New Abstraction for GC Software Engineering, Optimization, and Innovation
OOPSLA
Wenyu Zhao
Australian National University
Stephen M. Blackburn
Google; Australian National University
Kathryn S McKinley
Google
16:00 - 17:30
Rust
OOPSLA
at
Orchid Plenary Ballroom
Chair(s):
Alexander J. Summers
University of British Columbia
16:00
15m
Talk
A Refinement Methodology for Distributed Programs in Rust
OOPSLA
Aurea Bílá
ETH Zurich
João Pereira
ETH Zurich
Peter Müller
ETH Zurich
DOI
16:15
15m
Talk
AutoVerus: Automated Proof Generation for Rust Code
OOPSLA
Chenyuan Yang
University of Illinois Urbana-Champaign
Xuheng Li
Columbia University
Md Rakib Hossain Misu
University of California Irvine
Jianan Yao
University of Toronto
Weidong Cui
Microsoft Research
Yeyun Gong
Microsoft Research
Chris Hawblitzel
Microsoft Research
Shuvendu K. Lahiri
Microsoft Research
Jacob R. Lorch
Microsoft Research, n.n.
Shuai Lu
Microsoft Research
Fan Yang
Microsoft Research Asia
Ziqiao Zhou
Microsoft Research
Shan Lu
Microsoft; University of Chicago
16:30
15m
Talk
Carapace: Static–Dynamic Information Flow Control in Rust
OOPSLA
Vincent James Beardsley
Chris Xiong
Ohio State University
Ada Lamba
Ohio State University
Michael D. Bond
Ohio State University
16:45
15m
Talk
From Linearity to Borrowing
OOPSLA
Andrew Wagner
Northeastern University
Olek Gierczak
Northeastern University
Brianna Marshall
Northeastern University
John Li
Northeastern University
Amal Ahmed
Northeastern University, USA
DOI
Pre-print
17:00
15m
Talk
Garbage Collection for Rust: The Finalizer Frontier
OOPSLA
Jacob Hughes
King's College London
Laurence Tratt
King's College London
DOI
Pre-print
17:15
15m
Talk
Place Capability Graphs: A General-Purpose Model of Rust’s Ownership and Borrowing Guarantees
OOPSLA
Zachary Grannan
University of British Columbia
Aurea Bílá
ETH Zurich
Jonáš Fiala
ETH Zürich
Jasper Geer
University of British Columbia
Markus de Medeiros
New York University
Peter Müller
ETH Zurich
Alexander J. Summers
University of British Columbia
16:00 - 17:30
TOPLAS and Remote
OOPSLA
at
Orchid Small
Chair(s):
Charles Zhang
The Hong Kong University of Science and Technology
16:00
15m
Talk
(TOPLAS) Polynomial Bounds of CFLOBDDs against BDDs
OOPSLA
Xusheng Zhi
University of Wisconsin-Madison
Thomas Reps
University of Wisconsin-Madison
DOI
16:15
15m
Talk
(TOPLAS) Type-Safe Compilation of Dynamic Inheritance via Merging
OOPSLA
Yaozhu Sun
National Institute of Informatics
Xuejing Huang
IRIF
Bruno C. d. S. Oliveira
University of Hong Kong
16:30
15m
Talk
Detecting and explaining (in-)equivalence of context-free grammars
OOPSLA
Marko Schmellenkamp
Ruhr University Bochum
Thomas Zeume
Ruhr University Bochum
Sven Argo
Ruhr University Bochum
Sandra Kiefer
University of Oxford
Cedric Siems
Ruhr University Bochum
Fynn Stebel
Ruhr University Bochum
16:45
15m
Talk
Modal Abstractions for Virtualizing Memory Addresses
OOPSLA
Ismail Kuru
Drexel University
Colin Gordon
Drexel University
17:00
15m
Talk
Agora: Trust Less and Open More in Verification for Confidential Computing
OOPSLA
Hongbo Chen
Indiana University Bloomington
Quan Zhou
Penn State University
Sen Yang
Yale University
Dang Sixuan
Duke University
Xing Han
The Hong Kong University of Science and Technology
Danfeng Zhang
Duke University
Fan Zhang
Yale University
XiaoFeng Wang
Nanyang Technological University
17:15
15m
Talk
QED in Context: An Observation Study of Proof Assistant Users
OOPSLA
Jessica Shi
University of Pennsylvania
Cassia Torczon
University of Pennsylvania
Harrison Goldstein
University at Buffalo, the State University of New York at Buffalo
Benjamin C. Pierce
University of Pennsylvania
Andrew Head
University of Pennsylvania
16:00 - 17:30
Verification 4
OOPSLA
at
Orchid West
Chair(s):
Jieung Kim
Yonsei University
16:00
15m
Talk
Products of Recursive Programs for Hypersafety Verification
OOPSLA
Ruotong Cheng
University of Toronto
Azadeh Farzan
University of Toronto
16:15
15m
Talk
Embedding Quantum Program Verification into Dafny
OOPSLA
Feifei Cheng
Iowa State University
Sushen Vangeepuram
Iowa State University
Henry Allard
Iowa State University
Seyed Mohammad Reza Jafari
Iowa State University
Alex Potanin
Australian National University
Liyi Li
Iowa State University
16:30
15m
Talk
Faster Explicit-Trace Monitoring-Oriented Programming for Runtime Verification of Software Tests
OOPSLA
Kevin Guan
Cornell University
Marcelo d'Amorim
North Carolina State University
Owolabi Legunsen
Cornell University
16:45
15m
Talk
Interactive Bit Vector Reasoning using Verified Bitblasting
OOPSLA
Henrik Böving
Lean FRO
Siddharth Bhat
University of Cambridge
Alex Keizer
University of Cambridge
Luisa Cicolini
University of Cambridge
Leon Frenot
ENS Lyon
Abdalrhman Mohamed
Stanford University
Leo Stefanesco
University of Cambridge
Harun Khan
Stanford University
Josh Clune
Carnegie Mellon University
Clark Barrett
Stanford University
Tobias Grosser
University of Cambridge
Unscheduled Events
Not scheduled
Talk
Counterexample-Guided Inference of Modular Specifications
OOPSLA
William Hallahan
Binghamton
Ranjit Jhala
University of California at San Diego
Ruzica Piskac
Yale University
Not scheduled
Talk
Integrating Resource Analyses via Resource Decomposition
OOPSLA
Long Pham
Carnegie Mellon University
Yue Niu
National Institute of Informatics
Nathan Glover
Carnegie Mellon University
Feras A. Saad
Carnegie Mellon University
Jan Hoffmann
Carnegie Mellon University
Not scheduled
Talk
The Simulation Semantics of Synthesisable Verilog
OOPSLA
Andreas Lööw
Imperial College London
Pre-print
Not scheduled
Talk
Flix: A Design for Language-Integrated Datalog
OOPSLA
Magnus Madsen
Aarhus University
Ondřej Lhoták
University of Waterloo
Not scheduled
Talk
Complete the Cycle: Reachability Types with Expressive Cyclic References
OOPSLA
Haotian Deng
Purdue University
Siyuan He
Purdue University
Songlin Jia
Purdue University, USA
Yuyan Bao
Augusta University
Tiark Rompf
Purdue University
Not scheduled
Talk
Probabilistic Inference for Datalog with Correlated Inputs
OOPSLA
Jingbo Wang
Purdue University
Shashin Halalingaiah
UT Austin, IIT Madras
Weiyi Chen
Purdue University
Chao Wang
University of Southern California
Işıl Dillig
University of Texas at Austin
Not scheduled
Talk
Verifying Asynchronous Hyperproperties in Reactive Systems
OOPSLA
Raven Beutner
CISPA Helmholtz Center for Information Security, Germany
Bernd Finkbeiner
CISPA Helmholtz Center for Information Security
Not scheduled
Talk
Efficient Algorithms for the Uniform Tokenization Problem
OOPSLA
Angela W. Li
Rice University
Konstantinos Mamouras
Rice University
Not scheduled
Awards
SIGPLAN Awards
OOPSLA
Alex Potanin
Australian National University
Not scheduled
Awards
SPLASH Awards
OOPSLA
S:
Alex Potanin
Australian National University
S:
Charles Zhang
The Hong Kong University of Science and Technology
Not scheduled
Talk
Peepco: Batch-Based Consistency Optimization
OOPSLA
Ivan Kuraj
Massachusetts Institute of Technology
Jack Feser
Basis
Nadia Polikarpova
University of California at San Diego
Armando Solar-Lezama
Massachusetts Institute of Technology
Not scheduled
Talk
Validating Soundness and Completeness in Pattern-Match Coverage Analyzers
OOPSLA
Cyril Flurin Moser
ETH Zurich
Thodoris Sotiropoulos
ETH Zurich
Chengyu Zhang
ETH Zurich
Zhendong Su
ETH Zurich
Not scheduled
Talk
Multi-Modal Sketch-based Behavior Tree Synthesis
OOPSLA
Wenmeng Zhang
College of Computer Science and Technology, National University of Defense Technology, Changsha, China
Zhenbang Chen
College of Computer, National University of Defense Technology
Weijiang Hong
National University of Defense Technology, Changsha, China
Not scheduled
Awards
OOPSLA Artifact Awards
OOPSLA
Sankha Narayan Guria
University of Kansas
Eric Atkinson
Binghamton University
Not scheduled
Talk
Homomorphism Calculus for User-Defined Aggregations
OOPSLA
Ziteng Wang
University of Texas at Austin
Ruijie Fang
University of Texas at Austin
Linus Zheng
University of Texas at Austin
Dixin Tang
University of Texas Austin
Işıl Dillig
University of Texas at Austin
Pre-print
Not scheduled
Talk
RC Chair Report
OOPSLA
Sukyoung Ryu
KAIST
Shriram Krishnamurthi
Brown University
Not scheduled
Talk
Active Learning for Neurosymbolic Program Synthesis
OOPSLA
Celeste Barnaby
University of Texas at Austin
Jocelyn Qiaochu Chen
New York University, University of Alberta
Ramya Ramalingam
University of Pennsylvania
Osbert Bastani
University of Pennsylvania
Işıl Dillig
University of Texas at Austin
Not scheduled
Talk
General Chair Report
OOPSLA
Charles Zhang
The Hong Kong University of Science and Technology
Not scheduled
Talk
Scalable and Accurate Application-level Crash-Consistency Testing via Representative Testing
OOPSLA
Yile Gu
University of Washington
Ian Neal
University of Michigan and Veridise
Jiexiao Xu
University of Washington
Shaun Christopher Lee
University of Washington
Ayman Said
University of Michigan
Musa Haydar
University of Michigan
Jacob Van Geffen
Veridise Inc.
Rohan Kadekodi
University of Washington
Andrew Quinn
University of California at Santa Cruz
Baris Kasikci
University of Michigan, USA
Accepted Papers
Title
ABC: Towards a Universal Code Styler through Model Merging
OOPSLA
Yitong Chen
Zhiqiang Gao
Chuanqi Shi
Baixuan Li
Miao Gao
Abstract Interpretation of Temporal Safety Effects of Higher Order Programs
OOPSLA
Mihai Nicola
Chaitanya Agarwal
Eric Koskinen
Thomas Wies
Abstraction Refinement-guided Program Synthesis for Robot Learning from Demonstrations
OOPSLA
Guofeng Cui
Yuning Wang
Wensen Mao
Yuanlin Duan
He Zhu
AccelerQ: Accelerating Quantum Eigensolvers With Machine Learning on Quantum Simulators
OOPSLA
Avner Bensoussan
Elena Chachkarova
Karine Even-Mendoza
Sophie Fortz
Connor Lenihan
A complete formal semantics of eBPF instruction set architecture for Solana
OOPSLA
Shenghao Yuan
Zhuoruo Zhang
Jiayi Lu
David Sanan
Rui Chang
Yongwang Zhao
Active Learning for Neurosymbolic Program Synthesis
OOPSLA
Celeste Barnaby
Jocelyn Qiaochu Chen
Ramya Ramalingam
Osbert Bastani
Işıl Dillig
Adaptive Shielding via Parametric Safety Proofs
OOPSLA
Yao Feng
Jun Zhu
André Platzer
Jonathan Laurent
Adequacy for Algebraic Effects Revisited
OOPSLA
Alex Kavvos
A Domain-Specific Probabilistic Programming Language for Reasoning about Reasoning (or: a memo on memo)
OOPSLA
Kartik Chandra
Tony Chen
Joshua B. Tenenbaum
Jonathan Ragan-Kelley
Advancing Performance via a Systematic Application of Research and Industrial Best Practice
OOPSLA
Wenyu Zhao
Stephen M. Blackburn
Kathryn S McKinley
Man Cao
Sara S. Hamouda
A Flow-Sensitive Refinement Type System for Verifying eBPF Programs
OOPSLA
Ameer Hamza
Lucas Zavalia
Arie Gurfinkel
Jorge A. Navas
Grigory Fedyukovich
Agora: Trust Less and Open More in Verification for Confidential Computing
OOPSLA
Hongbo Chen
Quan Zhou
Sen Yang
Dang Sixuan
Xing Han
Danfeng Zhang
Fan Zhang
XiaoFeng Wang
A Hoare Logic For Symmetry Properties
OOPSLA
Vaibhav Mehta
Justin Hsu
A Language for Quantifying Quantum Network Behavior
OOPSLA
Anita Buckley
Pavel Chuprikov
Rodrigo Otoni
Robert Soulé
Robert Rand
Patrick Eugster
A Lightweight Type-and-Effect System for Invalidation Safety: Tracking Permanent and Temporary Invalidation With Constraint-Based Subtype Inference
OOPSLA
Cunyuan Gao
Lionel Parreaux
DOI
A Mechanized Semantics for Dataflow Circuits
OOPSLA
Tony Law
Delphine Demange
Sandrine Blazy
An Empirical Evaluation of Property-Based Testing in Python
OOPSLA
Savitha Ravi
Michael Coblenz
Link to publication
An Empirical Study of Bugs in the rustc Compiler
OOPSLA
Zixi Liu
Yang Feng
Yunbo Ni
Shaohua Li
Xizhe Yin
Qingkai Shi
Baowen Xu
Zhendong Su
API-guided Dataset Synthesis to Finetune Large Code Models
OOPSLA
Li Zongjie
Daoyuan Wu
Shuai Wang
Zhendong Su
ApkDiffer: Accurate and Scalable Cross-Version Diffing Analysis for Android Applications
OOPSLA
Jiarun Dai
Mingyuan Luo
Yuan Zhang
Min Yang
Minghui Yang
A Refinement Methodology for Distributed Programs in Rust
OOPSLA
Aurea Bílá
João Pereira
Peter Müller
DOI
Artemis: Toward Accurate Detection of Server-Side Request Forgeries through LLM-Assisted Inter-Procedural Path-Sensitive Taint Analysis
OOPSLA
Yuchen Ji
Ting Dai
Zhichao Zhou
Yutian Tang
Jingzhu He
A Sound Static Analysis Approach to I/O API Migration
OOPSLA
Shangyu Li
Zhaoyang Zhang
Sizhe Zhong
Diyu Zhou
Jiasi Shen
DOI
Media Attached
File Attached
A Unifying Approach to Product Constructions for Quantitative Temporal Inference
OOPSLA
Kazuki Watanabe
Sebastian Junges
Jurriaan Rot
Ichiro Hasuo
Automated Discovery of Tactic Libraries for Interactive Theorem Proving
OOPSLA
Yutong Xin
Jimmy Xin
Gabriel Poesia
Noah D. Goodman
Jocelyn Qiaochu Chen
Işıl Dillig
Automated Verification of Soundness of DNN Certifiers
OOPSLA
Avaljot Singh
Yasmin Chandini Sarita
Charith Mendis
Gagandeep Singh
Automatically Verifying Replication-aware Linearizability
OOPSLA
Vimala Soundarapandian
Kartik Nagar
Aseem Rastogi
KC Sivaramakrishnan
Link to publication
DOI
Media Attached
Automatic Linear Resource Bound Analysis for Rust via Prophecy Potentials
OOPSLA
Qihao Lian
Di Wang
Pre-print
AutoVerus: Automated Proof Generation for Rust Code
OOPSLA
Chenyuan Yang
Xuheng Li
Md Rakib Hossain Misu
Jianan Yao
Weidong Cui
Yeyun Gong
Chris Hawblitzel
Shuvendu K. Lahiri
Jacob R. Lorch
Shuai Lu
Fan Yang
Ziqiao Zhou
Shan Lu
Bennet: Randomized Specification Testing for Heap-Manipulating Programs
OOPSLA
Zain K Aamer
Benjamin C. Pierce
Binary Cryptographic Function Identification via Similarity Analysis with Path-insensitive Emulation
OOPSLA
Yikun Hu
Yituo He
Wenyu He
Haoran Li
Yubo Zhao
Shuai Wang
Dawu Gu
Bolt-On Strong Consistency: Specification, Implementation, and Verification
OOPSLA
Nicholas V. Lewchenko
Gowtham Kaki
Bor-Yuh Evan Chang
Boosting Program Reduction with the Missing Piece of Syntax-Guided Transformations
OOPSLA
Zhenyang Xu
Yongqiang Tian
Mengxiao Zhang
Chengnian Sun
Borrowing From Session Types
OOPSLA
Hannes Saffrich
Janek Spaderna
Peter Thiemann
Vasco T. Vasconcelos
Bridging the Gap between Real-World and Formal Binary Lifting through Filtered-Simulation
OOPSLA
Jihee Park
Insu Yun
Sukyoung Ryu
Link to publication
DOI
Carapace: Static–Dynamic Information Flow Control in Rust
OOPSLA
Vincent James Beardsley
Chris Xiong
Ada Lamba
Michael D. Bond
Certified Decision Procedures for Width-Independent Bitvector Predicates
OOPSLA
Siddharth Bhat
Leo Stefanesco
Chris Hughes
Tobias Grosser
Characterizing Implementability of Global Protocols with Infinite States and Data
OOPSLA
Elaine Li
Felix Stutz
Thomas Wies
Damien Zufferey
Checking $\delta$-Satisfiability of Reals with Integrals
OOPSLA
Cody Rivera
Bishnu Bhusal
Rohit Chadha
A. Prasad Sistla
Mahesh Viswanathan
Checking Observational Correctness of Database Systems
OOPSLA
Lauren Pick
Amanda Xu
Ankush Desai
Sanjit A. Seshia
Aws Albarghouthi
Choreographic Quick Changes: First-Class Location (Set) Polymorphism
OOPSLA
Ashley Samuelson
Andrew K. Hirsch
Ethan Cecchetti
Code Style Sheets: CSS for Code
OOPSLA
Sam Cohen
Ravi Chugh
Coinductive Proofs of Regular Expression Equivalence in Zero Knowledge
OOPSLA
John C. Kolesar
Shan Ali
Timos Antonopoulos
Ruzica Piskac
Combining Formal and Informal Information in Bayesian Program Analysis via Soft Evidences
OOPSLA
Tianchi Li
Xin Zhang
Compiling Classical Sequent Calculus to Stock Hardware: The Duality of Compilation
OOPSLA
Philipp Schuster
Marius Müller
Klaus Ostermann
Jonathan Immanuel Brachthäuser
Complete the Cycle: Reachability Types with Expressive Cyclic References
OOPSLA
Haotian Deng
Siyuan He
Songlin Jia
Yuyan Bao
Tiark Rompf
Compositional Quantum Control Flow with Efficient Compilation in Qunity
OOPSLA
Mikhail Mints
Finn Voichick
Leonidas Lampropoulos
Robert Rand
Compositional Symbolic Execution for the Next 700 Memory Models
OOPSLA
Andreas Lööw
Seung Hoon Park
Daniele Nantes-Sobrinho
Sacha-Élie Ayoun
Opale Sjöstedt
Philippa Gardner
Link to publication
DOI
Pre-print
Compressed and Parallelized Structured Tensor Algebra
OOPSLA
Mahdi Ghorbani
Emilien Bauer
Tobias Grosser
Amir Shaikhha
Contract System Metatheories à la Carte: A Transition-System View of Contracts
OOPSLA
Shu-Hung You
Christos Dimoulas
Robert Bruce Findler
Convex Hull Approximation for Activation Functions
OOPSLA
Zhongkui Ma
Zihan Wang
Guangdong Bai
Correct Black-Box Monitors for Distributed Deadlock Detection: Formalisation and Implementation
OOPSLA
Radosław Jan Rowicki
Adrian Francalanza
Alceste Scalas
DOI
Pre-print
Correct-By-Construction: Certified Individual Fairness through Neural Network Training
OOPSLA
Ruihan Zhang
Jun Sun
CoSSJIT: Combining Static Analysis and Speculation in JIT Compilers
OOPSLA
Aditya Anand
Vijay Sundaresan
Daryl Maier
Manas Thakur
Cost of Soundness in Mixed-Precision Tuning
OOPSLA
Anastasia Isychev
Debasmita Lohar
Pre-print
Counterexample-Guided Inference of Modular Specifications
OOPSLA
William Hallahan
Ranjit Jhala
Ruzica Piskac
Debugging WebAssembly? Put some Whamm on it!
OOPSLA
Elizabeth Gilbert
Matthew Schneider
Zixi An
Suhas Thalanki
Wavid Bowman
Alexander Bai
Ben L. Titzer
Heather Miller
Link to publication
DOI
Pre-print
Denotational Foundations for Expected Cost Analysis
OOPSLA
Pedro Henrique Azevedo de Amorim
Dependency-Aware Compilation for Surface Code Quantum Architectures
OOPSLA
Abtin Molavi
Amanda Xu
Swamit Tannu
Aws Albarghouthi
DepFuzz: Efficient Smart Contract Fuzzing with Function Dependence Guidance
OOPSLA
Chenyang Ma
Wei Song
Jeff Huang
DOI
DESIL: Detecting Silent Bugs in MLIR Compiler Infrastructure
OOPSLA
Chenyao Suo
Jianrong Wang
Yongjia Wang
Jiajun Jiang
Qingchao Shen
Junjie Chen
Destination calculus: A linear λ-calculus for purely functional memory writes
OOPSLA
Thomas BAGREL
Arnaud Spiwack
Link to publication
DOI
Pre-print
Media Attached
Detecting and explaining (in-)equivalence of context-free grammars
OOPSLA
Marko Schmellenkamp
Thomas Zeume
Sven Argo
Sandra Kiefer
Cedric Siems
Fynn Stebel
Divide and Conquer: A Compositional Approach to Game-Theoretic Security
OOPSLA
Ivana Bocevska
Anja Petković Komel
Laura Kovács
Sophie Rain
Michael Rawson
Divining Profiler Accuracy: An Approach to Approximate Profiler Accuracy Through Machine Code-Level Slowdown
OOPSLA
Humphrey Burchell
Stefan Marr
DOI
Pre-print
Dynamic Wind for Effect Handlers
OOPSLA
David Voigt
Philipp Schuster
Jonathan Immanuel Brachthäuser
Pre-print
Efficient Abstract Interpretation via Selective Widening
OOPSLA
Jiawei Wang
Xiao Cheng
Yulei Sui
Efficient Algorithms for the Uniform Tokenization Problem
OOPSLA
Angela W. Li
Konstantinos Mamouras
Efficient Decrease-And-Conquer Linearizability Monitoring
OOPSLA
Zheng Han Lee
Umang Mathur
Link to publication
DOI
Pre-print
Embedding Quantum Program Verification into Dafny
OOPSLA
Feifei Cheng
Sushen Vangeepuram
Henry Allard
Seyed Mohammad Reza Jafari
Alex Potanin
Liyi Li
Encode the $\forall\exists$ Relational Hoare Logic into Standard Hoare Logic
OOPSLA
Shushu Wu
Xiwei Wu
Qinxiang Cao
Enhancing APR with PRISM: A Semantic-Based Approach to Overfitting Patch Detection
OOPSLA
Dowon Song
Hakjoo Oh
Exploring the Theory and Practice of Concurrency in the Entity-Component-System Pattern
OOPSLA
Patrick Redmond
Jonathan Castello
Jose Calderon
Lindsey Kuper
Pre-print
Extraction and Mutation at a High Level: Template-Based Fuzzing for JavaScript Engines
OOPSLA
Wai Kin Wong
Dongwei Xiao
Cheuk Tung LAI
Yiteng Peng
Daoyuan Wu
Shuai Wang
Fast Client-Driven CFL-Reachability via Regularization-Based Graph Simplification
OOPSLA
Chenghang Shi
Dongjie He
Haofeng Li
Jie Lu
Lian Li
Jingling Xue
Fast Constraint Synthesis for C++ Function Templates
OOPSLA
Shuo Ding
Qirun Zhang
Faster Explicit-Trace Monitoring-Oriented Programming for Runtime Verification of Software Tests
OOPSLA
Kevin Guan
Marcelo d'Amorim
Owolabi Legunsen
Finch: Sparse and Structured Tensor Programming with Control Flow
OOPSLA
Willow Ahrens
Teodoro F. Collin
Radha Patel
Kyle Deeds
Changwan Hong
Saman Amarasinghe
Finding Compiler Bugs through Cross-Language Code Generator and Differential Testing
OOPSLA
Qiong Feng
Xiaotian Ma
Ziyuan Feng
Marat Akhin
Wei Song
Peng Liang
DOI
Flexible and Expressive Typed Path Patterns for GQL
OOPSLA
Wenjia Ye
Matías Toro
Tomás Diaz
Bruno C. d. S. Oliveira
Manuel Rigger
Claudio Gutierrez
Domagoj Vrgoč
Flix: A Design for Language-Integrated Datalog
OOPSLA
Magnus Madsen
Ondřej Lhoták
Float Self-Tagging
OOPSLA
Olivier Melançon
Manuel Serrano
Marc Feeley
Pre-print
FO-Complete Program Verification for Heap Logics
OOPSLA
Adithya Murali
Hrishikesh Balakrishnan
Aaron Councilman
P. Madhusudan
Formalizing Linear Motion G-code for Invariant Checking and Differential Testing of Fabrication Tools
OOPSLA
Yumeng He
Chandrakana Nandi
Sreepathi Pai
Foundations for Deductive Verification of Continuous Probabilistic Programs: From Lebesgue to Riemann and Back
OOPSLA
Kevin Batz
Joost-Pieter Katoen
Francesca Randone
Tobias Winkler
Fray: An Efficient General-Purpose Concurrency Testing Platform for the JVM
OOPSLA
Ao Li
Byeongjee Kang
Vasudev Vikram
Isabella Laybourn
Samvid Dharanikota
Shrey Tiwari
Rohan Padhye
Pre-print
Media Attached
From Linearity to Borrowing
OOPSLA
Andrew Wagner
Olek Gierczak
Brianna Marshall
John Li
Amal Ahmed
DOI
Pre-print
Fuzzing C++ Compilers via Type-Driven Mutation
OOPSLA
Bo Wang
Chong Chen
Ming Deng
Junjie Chen
Xing Zhang
Youfang Lin
Dan Hao
Jun Sun
GALA: A High Performance Graph Neural Network Acceleration LAnguage and Compiler
OOPSLA
Damitha Lenadora
Nikhil Jayakumar
Chamika Sudusinghe
Charith Mendis
Garbage Collection for Rust: The Finalizer Frontier
OOPSLA
Jacob Hughes
Laurence Tratt
DOI
Pre-print
Guarding the Privacy of Label-Only Access to Neural Network Classifiers via Formal Verification
OOPSLA
Anan Kabaha
Dana Drachsler Cohen
Hambazi: Spatial Coordination Synthesis for Augmented Reality
OOPSLA
Yi-Zhen Tsai
Jiasi Chen
Mohsen Lesani
HeapBuffers: Why not just using a binary serialization format for your managed memory?
OOPSLA
Daniele Bonetta
Júnior Löff
Matteo Basso
Walter Binder
Heap-Snapshot Matching and Ordering using CAHPs: A Context-Augmented Heap-Path Representation for Exact and Partial Path Matching using Prefix Trees
OOPSLA
Matteo Basso
Aleksandar Prokopec
Andrea Rosà
Walter Binder
HEMVM: a Heterogeneous Blockchain Framework for Interoperable Virtual Machines
OOPSLA
Vladyslav Nekriach
Sidi Mohamed Beillahi
Chenxing Li
Peilun Li
Ming Wu
Andreas Veneris
Fan Long
HieraSynth: A Parallel Framework for Complete Super-Optimization with Hierarchical Space Decomposition
OOPSLA
Sirui Lu
Rastislav Bodík
Homomorphism Calculus for User-Defined Aggregations
OOPSLA
Ziteng Wang
Ruijie Fang
Linus Zheng
Dixin Tang
Işıl Dillig
Pre-print
HpC: A Calculus for Hybrid and Mobile Systems
OOPSLA
Xiong Xu
Jean-Pierre Talpin
Shuling Wang
Bohua Zhan
Xinxin Liu
Naijun Zhan
HybridPersist: A Compiler Support for User-Friendly and Efficient PM Programming
OOPSLA
Yiyu Zhang
Yongzhi Wang
Yanfeng Gao
Xuandong Li
Zhiqiang Zuo
im2im: Automatically Converting In-Memory Image Representations using A Knowledge Graph Approach
OOPSLA
Fei Chen
Sunita Saha
Manuela Schuler
Philipp Slusallek
Tim Dahmen
IncIDFA: An Efficient and Generic Algorithm for Incremental Iterative Dataflow Analysis
OOPSLA
Aman Nougrahiya
V Krishna Nandivada
Incremental Bidirectional Typing via Order Maintenance
OOPSLA
Thomas J. Porter
Marisa Kirisame
Ivan Wei
Pavel Panchekha
Cyrus Omar
Incremental Certified Programming
OOPSLA
Tomás Diaz
Kenji Maillard
Nicolas Tabareau
Éric Tanter
Inductive Synthesis of Inductive Heap Predicates
OOPSLA
Ziyi Yang
Ilya Sergey
Integrating Resource Analyses via Resource Decomposition
OOPSLA
Long Pham
Yue Niu
Nathan Glover
Feras A. Saad
Jan Hoffmann
Interactive Bit Vector Reasoning using Verified Bitblasting
OOPSLA
Henrik Böving
Siddharth Bhat
Alex Keizer
Luisa Cicolini
Leon Frenot
Abdalrhman Mohamed
Leo Stefanesco
Harun Khan
Josh Clune
Clark Barrett
Tobias Grosser
Interleaving Large Language Models for Compiler Testing
OOPSLA
Yunbo Ni
Shaohua Li
JavART: a Lightweight Rule-Based JIT Compiler Using Translation Rules Extracted from a Learning Approach
OOPSLA
Hanzhang Wang
Wei Peng
Wenwen Wang
Yunping Lu
Pen-Chung Yew
Weihua Zhang
KestRel: Relational Verification Using E-Graphs for Program Alignment
OOPSLA
Robert Dickerson
Prasita Mukherjee
Benjamin Delaware
Language-Parametric Reference Synthesis
OOPSLA
Daniel A. A. Pelsmaeker
Aron Zwaan
Casper Bach
Arjan J. Mooij
Large Language Model powered Symbolic Execution
OOPSLA
Yihe Li
Ruijie Meng
Gregory J. Duck
Laurel: Unblocking Automated Verification with Large Language Models
OOPSLA
Eric Mugnier
Emmanuel Anaya Gonzalez
Nadia Polikarpova
Ranjit Jhala
Zhou Yuanyuan
Liberating Merges via Apartness and Guarded Subtyping
OOPSLA
Han Xu
Xuejing Huang
Bruno C. d. S. Oliveira
Lilo: A Higher-Order, Relational Concurrent Separation Logic for Liveness
OOPSLA
Dongjae Lee
Janggun Lee
Taeyoung Yoon
Minki Cho
Jeehoon Kang
Chung-Kil Hur
LOUD: Synthesizing Strongest and Weakest Specifications
OOPSLA
Kanghee Park
Xuanyu Peng
Loris D'Antoni
Memory-Safety Verification of Open Programs With Angelic Assumptions
OOPSLA
Gourav Takhar
Baldip Bijlani
Prantik Chatterjee
Akash Lal
Subhajit Roy
MetaKernel: Enabling Efficient Encrypted Neural Network Inference Through Unified MVM and Convolution
OOPSLA
Peng Yuan
Yan Liu
Jianxin Lai
Long Li
Tianxiang Sui
Linjie Xiao
Xiaojing Zhang
Qing Zhu
Jingling Xue
Metamorph: Synthesizing Large Objects from Dafny Specifications
OOPSLA
Aleksandr Fedchin
Alexander Bai
Jeffrey S. Foster
Mind the Abstraction Gap: Bringing Equality Saturation to Real-World ML Compilers
OOPSLA
Arya Vohra
Leo Seojun Lee
Jakub Bachurski
Oleksandr Zinenko
Phitchaya Mangpo Phothilimthana
Albert Cohen
William S. Moses
Mini-Batch Robustness Verification of Deep Neural Networks
OOPSLA
Saar Tzour-Shaday
Dana Drachsler Cohen
MIO: Multiverse Debugging in the face of Input/Output
OOPSLA
Tom Lauwaerts
Maarten Steevens
Christophe Scholliers
Link to publication
DOI
Pre-print
Modal Abstractions for Virtualizing Memory Addresses
OOPSLA
Ismail Kuru
Colin Gordon
Modal Effect Types
OOPSLA
Wenhao Tang
Leo White
Stephen Dolan
Daniel Hillerström
Sam Lindley
Anton Lorenzen
Model-guided Fuzzing of Distributed Systems
OOPSLA
Ege Berkay Gulcan
Burcu Kulahcioglu Ozkan
Rupak Majumdar
Srinidhi Nagendra
Modeling Reachability Types with Logical Relations -- Semantic Type Soundness, Termination, Effect Safety, and Equational Theory
OOPSLA
Yuyan Bao
Songlin Jia
Guannan Wei
Oliver Bračevac
Tiark Rompf
Modular Reasoning about Global Variables and Their Initialization
OOPSLA
João Pereira
Isaac van Bakel
Patricia Firlejczyk
Marco Eilers
Peter Müller
MTP: A Meaning-Typed Language Abstraction for AI-Integrated Programming
OOPSLA
Jayanaka Dantanarayana
Yiping Kang
Kugesan Sivasothynathan
Christopher Clarke
Baichuan Li
Savini Kashmira
Krisztian Flautner
Lingjia Tang
Jason Mars
Multi-Language Probabilistic Programming
OOPSLA
Sam Stites
John Li
Steven Holtzen
Multi-Modal Sketch-based Behavior Tree Synthesis
OOPSLA
Wenmeng Zhang
Zhenbang Chen
Weijiang Hong
Non-interference Preserving Optimising Compilation
OOPSLA
Julian Rosemann
Sebastian Hack
Deepak Garg
Link to publication
DOI
Notions of Stack-manipulating Computation and Relative Monads
OOPSLA
Yuchen Jiang
Runze Xue
Max S. New
On Abstraction Refinement for Bayesian Program Analysis
OOPSLA
Yuanfeng Shi
Yifan Zhang
Xin Zhang
On Higher-Order Model Checking of Effectful Answer-Type-Polymorphic Programs
OOPSLA
Taro Sekiyama
Ugo Dal Lago
Hiroshi Unno
On the Impact of Formal Verification on Software Development
OOPSLA
Eric Mugnier
Zhou Yuanyuan
Ranjit Jhala
Michael Coblenz
Opportunistically Parallel Lambda Calculus
OOPSLA
Stephen Mell
Konstantinos Kallas
Steve Zdancewic
Osbert Bastani
Orax: A Feedback-Driven Framework for Efficiently Solving Satisfiability Modulo Theories and Oracles
OOPSLA
Zhineng Zhong
Ziqi Zhang
Hanqin Guan
Ding Li
PAFL: Enhancing Fault Localizers by Leveraging Project-Specific Fault Patterns
OOPSLA
Donguk Kim
Doha Hwang
Minseok Jeon
Hakjoo Oh
Pathological Cases for a Class of Reachability-Based Garbage Collectors
OOPSLA
Matthew Sotoudeh
Link to publication
Peepco: Batch-Based Consistency Optimization
OOPSLA
Ivan Kuraj
Jack Feser
Nadia Polikarpova
Armando Solar-Lezama
Place Capability Graphs: A General-Purpose Model of Rust’s Ownership and Borrowing Guarantees
OOPSLA
Zachary Grannan
Aurea Bílá
Jonáš Fiala
Jasper Geer
Markus de Medeiros
Peter Müller
Alexander J. Summers
Polymorphic Records for Dynamic Languages
OOPSLA
Giuseppe Castagna
Loïc Peyrot
P³: Reasoning about Patches via Product Programs
OOPSLA
Arindam Sharma
Daniel Schemmel
Cristian Cadar
PReMM: LLM-Based Program Repair for Multi-Method Bugs via Divide and Conquer
OOPSLA
Linna Xie
Zhong Li
Yu Pei
Zhongzhen Wen
Kui Liu
Tian Zhang
Xuandong Li
Probabilistic Inference for Datalog with Correlated Inputs
OOPSLA
Jingbo Wang
Shashin Halalingaiah
Weiyi Chen
Chao Wang
Işıl Dillig
Products of Recursive Programs for Hypersafety Verification
OOPSLA
Ruotong Cheng
Azadeh Farzan
Proof Repair across Quotient Type Equivalences
OOPSLA
Cosmo Viola
Max Fan
Talia Lily Ringer
Pyrosome: Verified Compilation for Modular Metatheory
OOPSLA
Dustin Jamner
Gabriel Kammer
Ritam Nag
Adam Chlipala
QbC: Quantum Correctness by Construction
OOPSLA
Anurudh Peduri
Ina Schaefer
Michael Walter
qblaze: An Efficient and Scalable Sparse Quantum Simulator
OOPSLA
Hristo Venev
Thien Udomsrirungruang
Dimitar Dimitrov
Timon Gehr
Martin Vechev
QED in Context: An Observation Study of Proof Assistant Users
OOPSLA
Jessica Shi
Cassia Torczon
Harrison Goldstein
Benjamin C. Pierce
Andrew Head
Qualified Types with Boolean Algebras
OOPSLA
Edward Lee
Jonathan Lindegaard Starup
Ondřej Lhoták
Magnus Madsen
Quantified Underapproximation via Labeled Bunches
OOPSLA
Lang Liu
Farzaneh Derakhshan
Limin Jia
Gabriel A. Moreno
Mark Klein
Quantization with Guaranteed Floating-Point Neural Network Classifications
OOPSLA
Anan Kabaha
Dana Drachsler Cohen
React-tRace: A Semantics for Understanding React Hooks
OOPSLA
Jay Lee
Joongwon Ahn
Kwangkeun Yi
Link to publication
DOI
Reasoning about External Calls
OOPSLA
Julian Mackay
Sophia Drossopoulou
James Noble
Susan Eisenbach
Link to publication
DOI
Pre-print
REPTILE: Performant Tiling of Recurrences
OOPSLA
Muhammad Usman Tariq
Shiv Sundram
Fredrik Kjolstad
RestPi: Path-Sensitive Type Inference for REST APIs
OOPSLA
Mark W. Aldrich
Kyla H. Levin
Michael Coblenz
Jeffrey S. Foster
Revamping Verilog Semantics for Foundational Verification
OOPSLA
Joonwon Choi
Jaewoo Kim
Jeehoon Kang
Revealing Sources of (Memory) Errors via Backward Analysis
OOPSLA
Flavio Ascari
Roberto Bruni
Roberta Gori
Francesco Logozzo
ROSpec: A Domain-Specific Language for ROS-based Robot Software
OOPSLA
Paulo Canelas
Bradley Schmerl
Alcides Fonseca
Christopher Steven Timperley
DOI
Pre-print
Media Attached
SafeRace: Assessing and Addressing WebGPU Memory Safety in the Presence of Data Races
OOPSLA
Reese Levine
Ashley Lee
Neha Abbas
Kyle Little
Tyler Sorensen
SafeTree: Expressive Tree Policies for Microservices
OOPSLA
Karuna Grewal
Brighten Godfrey
Justin Hsu
Scalable Equivalence Checking and Verification of Shallow Quantum Circuits
OOPSLA
Nengkun Yu
Xuan Du Trinh
Thomas Reps
Scaling Instruction-Selection Verification against Authoritative ISA Semantics
OOPSLA
Michael McLoughlin
Ashley Sheng
Chris Fallin
Bryan Parno
Fraser Brown
Alexa VanHattum
DOI
Scaling Optimization Over Uncertainty via Compilation
OOPSLA
Minsung Cho
John Gouwar
Steven Holtzen
Semantics of Sets of Programs
OOPSLA
Jinwoo Kim
Shaan Nagy
Thomas Reps
Loris D'Antoni
Shaking Up Quantum Simulators with Fuzzing and Rigour
OOPSLA
Vasileios Klimis
Karine Even-Mendoza
Avner Bensoussan
Elena Chachkarova
Sophie Fortz
Connor Lenihan
Show Me Why It's Correct: Saving 1/3 of Debugging Time in Program Repair with Interactive Runtime Comparison
OOPSLA
Ruixin Wang
Zhongkai Zhao
Le Fang
Nan Jiang
Yiling Lou
Lin Tan
Tianyi Zhang
Link to publication
DOI
Pre-print
SIGPLAN Awards
OOPSLA
Alex Potanin
Software Model Checking via Summary-Guided Search
OOPSLA
Ruijie Fang
Zachary Kincaid
Thomas Reps
DOI
Pre-print
Sound and Modular Activity Analysis for Automatic Differentiation in MLIR
OOPSLA
Mai Jacob Peng
William S. Moses
Oleksandr Zinenko
Christophe Dubach
Soundness of Predictive Concurrency Analyses
OOPSLA
Shuyang Liu
Doug Lea
Jens Palsberg
Link to publication
SPLAT: A framework for optimised GPU code-generation for SParse reguLar ATtention
OOPSLA
Ahan Gupta
Yueming Yuan
Devansh Jain
Yuhao Ge
David Aponte
Yanqi Zhou
Charith Mendis
Statically Analyzing the Dataflow of R Programs
OOPSLA
Florian Sihler
Matthias Tichy
File Attached
Static Inference of Regular Grammars for Ad Hoc Parsers
OOPSLA
Michael Schröder
Jürgen Cito
DOI
Pre-print
Stencil-Lifting: Hierarchical Recursive Lifting System for Extracting Summary of Stencil Kernel in Legacy Codes
OOPSLA
Mingyi Li
Junmin Xiao
Siyan Chen
Hui Ma
Xi Chen
Peihua Bao
Liang Yuan
Guangming Tan
Structural Abstraction and Refinement for Probabilistic Programs
OOPSLA
Guanyan Li
Juanen Li
Zhilei Han
Peixin Wang
Hongfei Fu
Fei He
Structural Information Flow: A Fresh Look at Types for Non-Interference
OOPSLA
Hemant Gouni
Frank Pfenning
Jonathan Aldrich
Pre-print
Structural temporal logic for mechanized program verification
OOPSLA
Lef Ioannidis
Yannick Zakowski
Steve Zdancewic
Sebastian Angel
Symbolic MRD: Dynamic Memory, Undefined Behaviour, and Extrinsic Choice
OOPSLA
Jay Richards
Daniel Wright
Simon Cooksey
Mark Batty
Synchronized Behavior Checking: A Method for Finding Missed Compiler Optimizations
OOPSLA
Yi Zhang
Yu Wang
Linzhang Wang
Ke Wang
Syntactic Completions with Material Obligations
OOPSLA
David Moon
Andrew Blinn
Thomas J. Porter
Cyrus Omar
DOI
Pre-print
Synthesizing DSLs for Few-Shot Learning
OOPSLA
Paul Krogmeier
P. Madhusudan
Synthesizing Implication Lemmas for Interactive Theorem Proving
OOPSLA
Ana Brendel
Aishwarya Sivaraman
Todd Millstein
Synthesizing Sound and Precise Abstract Transformers for Nonlinear Hyperbolic PDE Solvers
OOPSLA
Jacob Laurel
Ignacio Laguna
Jan Hueckelheim
Tabby: A Synthesis-Aided Compiler for High-Performance Zero-Knowledge Proof Circuits
OOPSLA
Junrui Liu
Jiaxin Song
Yanning Chen
Hanzhi Liu
Hongbo Wen
Luke Pearson
Yanju Chen
Yu Feng
TailTracer: Continuous Tail Tracing for Production Use
OOPSLA
Tianyi Liu
Yi Li
Yiyu Zhang
Zhuangda Wang
Rongxin Wu
Xuandong Li
Zhiqiang Zuo
The Continuous Tensor Abstraction: Where Indices are Real
OOPSLA
Jaeyeon Won
Willow Ahrens
Teodoro F. Collin
Joel S Emer
Saman Amarasinghe
The Power of Regular Constraint Propagation
OOPSLA
Matthew Hague
Artur Jez
Anthony Widjaja Lin
Oliver Markgraf
Philipp Ruemmer
The Simple Essence of Monomorphization
OOPSLA
Matthew Lutze
Philipp Schuster
Jonathan Immanuel Brachthäuser
The Simple Essence of Overloading: Making ad-hoc polymorphism more algebraic with flow-based variational type-checking
OOPSLA
Jiří Beneš
Jonathan Immanuel Brachthäuser
DOI
Pre-print
(TOPLAS) Polynomial Bounds of CFLOBDDs against BDDs
OOPSLA
Xusheng Zhi
Thomas Reps
DOI
(TOPLAS) Type-Safe Compilation of Dynamic Inheritance via Merging
OOPSLA
Yaozhu Sun
Xuejing Huang
Bruno C. d. S. Oliveira
Towards a Theoretically-Backed and Practical Framework for Selective Object-Sensitive Pointer Analysis
OOPSLA
Chaoyue Zhang
Longlong Lu
Yifei Lu
Minxue Pan
Xuandong Li
Towards Verifying Crash Consistency
OOPSLA
Keonho Lee
Conan Truong
Brian Demsky
TraceLinking Implementations with their Verified Designs
OOPSLA
Finn Hackett
Ivan Beschastnikh
Pre-print
Tracing Just-in-time Compilation for Effects and Handlers
OOPSLA
Marcial Gaißert
CF Bolz-Tereick
Jonathan Immanuel Brachthäuser
Pre-print
Translation Validation for LLVM's AArch64 Backend
OOPSLA
Ryan Berger
Mitch Briles
Nader Boushehrinejad Moradi
Nicholas Coughlin
Kait Lam
Nuno P. Lopes
Stefan Mada
Tanmay Tirpankar
John Regehr
Tuning Random Generators: Property-Based Testing as Probabilistic Programming
OOPSLA
Ryan Tjoa
Poorva Garg
Harrison Goldstein
Todd Millstein
Benjamin C. Pierce
Guy Van den Broeck
DOI
Pre-print
Tunneling Through the Hill: Multi-Way Intersection for Version-Space Algebras in Program Synthesis
OOPSLA
Guanlin Chen
Ruyi Ji
Shuhao Zhang
Yingfei Xiong
DOI
Two Approaches to Fast Bytecode Frontend for Static Analysis
OOPSLA
Chenxi Li
Haoran Lin
Tian Tan
Yue Li
Type-Outference with Label-Listeners: Foundations for Decidable Type-Consistency for Nominal Object-Oriented Generics
OOPSLA
Ross Tate
DOI
Pre-print
Type-Preserving Flat Closure Optimization
OOPSLA
Adam T. Geller
Sean Bocirnea
Chester Gould
Paulette Koronkevich
William J. Bowman
DOI
Understanding and Improving Flaky Test Classification
OOPSLA
Shanto Rahman
Saikat Dutta
August Shi
Universal Scalability in Declarative Program Analysis (with Choice-Based Combination Pruning)
OOPSLA
Anastasios Antoniadis
Ilias Tsatiris
Neville Grech
Yannis Smaragdakis
Link to publication
DOI
Unveiling Heisenbugs with Diversified Execution
OOPSLA
Arjun Ramesh
Tianshu Huang
Jaspreet Riar
Ben L. Titzer
Anthony Rowe
UTFix: Change Aware Unit Test Repairing using LLM
OOPSLA
Shanto Rahman
Sachit Kuhar
Berk Cirisci
Pranav Garg
Shiqi Wang
Xiaofei Ma
Anoop Deoras
Baishakhi Ray
Validating SMT Rewriters via Rewrite Space Exploration Supported by Generative Equality Saturation
OOPSLA
Maolin Sun
Yibiao Yang
Jiangchang Wu
Yuming Zhou
Verification of Bit-Flip Attacks against Quantized Neural Networks
OOPSLA
Yedi Zhang
Lei Huang
Pengfei Gao
Fu Song
Jun Sun
Jin Song Dong
We’ve Got You Covered: Type-Guided Repair of Incomplete Input Generators
OOPSLA
Patrick LaFontaine
Zhe Zhou
Ashish Mishra
Suresh Jagannathan
Benjamin Delaware
What's in the Box: Ergonomic and Expressive Capture Tracking over Generic Data Structures
OOPSLA
Yichen Xu
Oliver Bračevac
Nguyen Pham
Martin Odersky
Pre-print
Work Packets: A New Abstraction for GC Software Engineering, Optimization, and Innovation
OOPSLA
Wenyu Zhao
Stephen M. Blackburn
Kathryn S McKinley
Zero-Overhead Lexical Effect Handlers
OOPSLA
Cong Ma
Zhaoyi Ge
Jonghyun Jung
Yizhou Zhang
Call for Papers
Introduction
What’s New
Contact
Review Process
Reserve Reviewer Policy
Submissions
Template
Page Limit
Anonymity
Novelty
Data-Availability Statement
Procedure
Publication
ACM Policies
FAQ
All Dates
Introduction
The OOPSLA issue of the Proceedings of the ACM on Programming Languages (PACMPL) welcomes papers focusing on all practical and theoretical investigations of programming systems, languages, and environments. Papers may target any stage of software development, including requirements, modeling, prototyping, design, implementation, generation, analysis, verification, testing, evaluation, maintenance, and reuse of software systems. Contributions may include the development of new tools, techniques, principles, and evaluations.
OOPSLA 2025 will have two rounds of reviewing, with the Round 1 submission deadline
October 15, 2024
and Round 2 submission deadline
March 25, 2025
(AoE). All deadlines are firm. New papers may be submitted to either round. Papers accepted in either round will be published in the 2025 volume of PACMPL(OOPSLA) and invited to present at the SPLASH conference in 2025.
What’s New
There are two new things in this year’s Call that you should be sure to pay attention to:
Reserve Reviewer Policy
Data-Availability Statement
Contact
You can reach the two RC Chairs (Shriram and Sukyoung) by email. Since it has been picked up by spammers, the previously-published collective email address
has been taken down
. Please email the chairs directly through their public email addresses instead.
In your email, please mention the number of the paper you are writing about (if you have one). That makes it easier to track the context (and avoids ambiguity).
Review Process
PACMPL(OOPSLA) has two rounds of reviewing. Each paper will typically receive three or more reviews. You will get an opportunity to respond to these reviews before decisions are finalized.
At the end of each round, each paper will receive one of the five following decisions:
Accept
: Your paper will appear in the upcoming volume of PACMPL(OOPSLA).
Reject
: Your paper will not appear in the upcoming volume of PACMPL(OOPSLA). In addition, a resubmission in less than a year from the original submission is not guaranteed a review. A paper is considered a resubmission if, in the judgment of the Chairs, it is substantially similar to the original submission.
Conditional Accept
: While the Review Committee likes the work, it would like to see some specific changes made. You will receive a list of specific required revisions.
Minor Revision
: While the Review Committee likes the direction of the work, it has several concerns that it would like to see revised. These concerns go beyond what can be enumerated in a list. Thus, you may receive some specific required revisions, but can also expect to receive broader comments.
Major Revision
: While the Review Committee thinks the direction of the work has promise, it has significant concerns that it would like to see revised. You may receive some specific required revisions, but will also receive broader comments that may take significantly longer to execute.
If you receive one of the latter three decisions, please note:
Unlike in some previous years, there is no restriction on when you can submit your revision. The decision does not imply a duration.
If you choose to submit a revised paper, you must also submit both (a) a clear explanation of how your revision addresses these comments, and (b) unless impossible, a diff of the PDFs. Independent of the decision, you can submit at the next deadline (either the opening deadline of the next round or the revision deadline of the current round). To the extent possible, your submission will be reviewed by the same reviewers.
Unless you explicitly withdraw your paper, it is considered
under review
. Therefore, it would violate policy to submit it elsewhere. If you choose to withdraw the paper (e.g., to submit elsewhere), the next time you submit it, it will be treated as a fresh paper: you may get entirely different reviewers, previous reviews and comments will not be available, etc.
Until your paper is accepted or rejected, you should maintain the anonymity of your submission. If you believe you need to violate it to respond to the reviews, please first discuss this with the Chairs.
If the Artifact Evaluation submission deadline occurs before the decision date, Conditionally Accepted papers will be invited to submit artifacts. However, acceptance of artifacts has no impact on the acceptance of the revised papers.
Only
Accepted and Conditionally Accepted papers can submit artifacts for evaluation. The reason for this is that often, Minor and Major revisions end up affecting the artifacts, sometimes substantially. It is not reasonable to ask the AEC to review the artifacts twice; nor does it make sense to review artifacts that are likely to change. For this reason, artifact evaluation will only happen once the paper reaches (near-)final form. Thus, for instance, a paper accepted after revisions in R1 can submit to the AEC for R2, and get its badges then.
Reserve Reviewer Policy
To prepare for the possibility of a higher volume of submissions, we are implementing a new review policy: for each paper, at least one senior author must — unless exempt under the criteria below — register as a reserve reviewer. They must list their information on the submission form, and they must register themselves on
TPMS
Instructions
: Log into TPMS with the same email address as for your HotCRP account. The system will ask you to upload (or provide URLs for) 5-10 of your previous papers, to base your matching on. Uploading papers/URLs is pretty straightforward; here’s also a
step-by-step video
. You get to choose which papers you want to upload; these determine what papers you are most likely to be asked to review. So please go for both depth and breadth. In particular, please provide papers on topics for which you are a relatively rare expert.
The goal of this policy is to uphold the high standard of reviews within the SIGPLAN community. To achieve this, we must ensure manageable review loads, prevent burnout, and encourage reviewers to stay engaged for future rounds. High-quality reviews are one of the community’s greatest assets, playing a crucial role in elevating the quality of research for everyone.
Our hope is that these reserve reviewers won’t be needed at all! They will only be called upon as ad hoc reviewers if our projections fall significantly short. Even in that case, their review load will be far lighter than that of RC members, and we will do our best to assign papers that closely match expertise (hence the need for TPMS registration).
We define “senior” authors as those who completed their PhD five or more years ago. A paper is exempt from the reserve reviewer policy if:
The paper has no senior authors.
At least one senior author is already in the RC for this conference.
Every
senior author of the paper satisfies one or more of these criteria:
is new to SIGPLAN (has never published in it before);
is chairing a SIGPLAN conference with 150 or more submissions last year, this year, or next year;
has some other exceptional circumstance that didn’t prevent writing the paper but prevents doing any reviewing. This must be cleared at least three days before submission with the RC Chairs.
It is okay for one person to serve as the reserve reviewer for more than one paper. Please enter their information for each such paper (preferably identically).
Submissions
Template
SPLASH’s PACMPL templates and instructions are on the
SIGPLAN author information
page. Please use
\documentclass[acmsmall,screen,review]{acmart}
at the top of your paper.
Page Limit
Initial submissions must be
at most 23 pages
using the template. This page limit does not include required statements, references, or supplementary material (such as appendices). However, papers must be self-contained; reviewers are under no obligation to read the supplementary material.
Revisions can correspondingly go up to a maximum of
25 pages
. This includes papers given a minor or major revision in 2024, as well as the final, camera-ready papers. For fairness, there will not be an option to purchase additional pages. For the final paper, we ask you to stick as closely as possible to the final version accepted by reviewers, and only add material that reviewers requested or that you promised.
Anonymity
PACMPL uses double-blind reviewing. Authors’ identities are only revealed if a paper is accepted. Your papers must
omit author names and institutions,
use the third person when referencing your work,
anonymize supplementary material.
Nothing should be done in the name of anonymity that weakens the submission. When in doubt, contact the Review Committee Chairs.
Novelty
Papers must describe unpublished work that is not currently submitted for publication elsewhere as described by
SIGPLAN’s Re-Publication Policy
. Submitters should also be aware of ACM’s Policy and Procedures on Plagiarism. Submissions are expected to comply with the ACM Policies for Authorship.
Data-Availability Statement
To help readers understand the state of the intended artifact, we ask you to add a section just before references titled
Data-Availability Statement
in the initial submission. This will not count towards the page limit, but please limit it to at most a few paragraphs (usually one paragraph suffices).
In it, indicate whether an artifact exists, its nature and limitations, and whether it will be submitted for Artifact Evaluation. This section should ideally also include links to preliminary versions of (anonymized) artifacts, datasets, and so on that reviewers may find useful (but are not obliged to follow). The statement is not meant to be a detailed description of how to
use
the artifact; that should accompany the artifact itself.
It is understood that some papers have no artifacts but, given the broad range of what constitutes an artifact, it would be helpful to readers to explain why the paper has none.
Accepted papers that fail to provide an artifact after promising one will be asked to explain why they did not do so.
Artifact Evaluation submission will closely follow paper notification, so make sure you check the Artifact Call as soon as you submit your paper.
Procedure
Please submit using
HotCRP
Publication
PACMPL is a Gold Open Access journal. All papers will be freely available to the public. Authors can voluntarily cover the article processing charge (USD 400), but payment is not required.
The official publication date is the date the journal is made available in the ACM Digital Library. The journal issue and associated papers accepted in Round 1 (OOPSLA1) will be published no earlier than April 1, 2025, while those accepted in Round 2 (OOPSLA2) will be published no earlier than October 1, 2025. The official publication date affects the deadline for any patent filings related to published work.
ACM Policies
By submitting your article to an ACM Publication, you are acknowledging that you and your co-authors are subject to all
ACM Publications Policies
, including ACM’s new
Publications Policy on Research Involving Human Participants and Subjects
. Alleged violations of this policy or any ACM Publications Policy will be investigated by ACM and may result in a full retraction of your paper, in addition to other potential penalties, as per ACM Publications Policy.
Please ensure that you and your co-authors
obtain an ORCID iD
, so you can complete the publishing process for your accepted paper. ACM has been involved in ORCID from the start and has made a
commitment to collecting ORCID iDs from all of our published authors
. ORCID iDs help improve author discoverability, ensuring proper attribution and contributing to ongoing community efforts around name normalization; your ORCID iD will help in these efforts.
The ACM Publications Board has recently updated the ACM Authorship Policy in several ways:
Addressing the use of generative AI systems in the publications process
Clarifying criteria for authorship and the responsibilities of authors
Defining prohibited behaviour, such as gift, ghost, or purchased authorship
Providing a linked FAQ explaining the rationale for the policy and providing additional details
You can find the
updated policy here
FAQ
What are reviewers looking for?
We consider the following criteria when evaluating papers:
Novelty
: The paper presents new ideas and results and places them appropriately within the context established by previous research.
Importance
: The paper contributes to the advancement of knowledge in the field. We welcome papers that diverge from the dominant trajectory of the field.
Evidence
: The paper presents sufficient evidence supporting its claims, such as proofs, implemented systems, experimental results, statistical analyses, user studies, case studies, and anecdotes.
Clarity
: The paper presents its contributions, methodology, and results clearly.
How are papers from previous years handled?
We follow the same timeline as the other papers with the following two differences: (1) we try to assign the same reviewers you had in the previous year’s OOPSLA; (2) we strongly discourage reviewers from giving another “major revision” decision.
Are artifacts required?
No! It is understood that some papers have no artifacts. However, if the nature of the paper’s content and claims suggest there ought to be an artifact, authors must explain why they will not be providing one. The absence of such an explanation can be cause for rejection.
Can a paper be accepted if the artifact is rejected?
Yes. Sometimes artifacts are rejected for reasons having nothing to do with the research results (e.g., packaging issues).
What exactly do I have to do to anonymize my paper?
Use common sense. Your job is not to make your identity completely undiscoverable (e.g., if a reviewer does a Web search for the text of your paper) but simply to make it possible for reviewers to evaluate your submission without knowing who you are. This includes omitting your names from your title page, and referring to your own work in the third person. For example, if your name is Smith and you have worked on amphibious type systems, instead of saying “We extend our earlier work on statically typed toads [Smith 2004]”, you might say “We extend Smith’s [2004] work on statically typed toads.” Also, be sure not to include any acknowledgements that would give away your identity. It is best to suppress acknowledgments entirely until camera-ready.
Should I change the name of my system?
No. However, if it is not a new system and is likely to be known to others, you should refer to it as if it were created by a third party, rather than as your own creation.
My submission is based on code available in a public repository. How do I deal with this?
Cite the code in your paper, but replace the URL with text like “link removed for double-blind review”. If you believe reviewer access to your code would help during author response, contact the Review Committee Chairs.
I am submitting an extension of my workshop paper. Should I anonymize reference to that work?
Yes, you should treat it like any other anonymization. But you should also change the title of the paper to break a direct link between the two.
Am I allowed to post my paper on my web page or arXiv, send it to colleagues, give a talk about it, mention it on social media, …?
We want to help you navigate the tension between the normal communication of scientific results and actions that essentially force potential reviewers to learn the identity of authors. Roughly speaking, you may discuss work under submission, but you should not broadly advertise your work through media that are likely to reach your reviewers. We acknowledge there are grey areas and trade-offs. When in doubt about any of these guidelines, please first check in with the Review Committee Chairs: better safe than sorry. (If the Chairs give you permission, they can then also address any subsequent complaints about those actions from reviewers.)
Things you
may
do:
Put your submission on your home page, arXiv, or other pre-publication sites.
Discuss your work with anyone not on the review committees or reviewers with whom you already have a conflict.
Present your work at professional meetings, job interviews, etc.
Submit work previously discussed at an informal workshop, previously posted on a pre-publication site, previously submitted to a conference not using double-blind reviewing, etc.
Things you
should
not
do
Contact members of the review committee about your work, or deliberately present your work where you expect them to be.
Publicize your work on social media in an identifiable way with broad settings. For example, a post with a broad privacy setting (public or all friends) saying, “Whew, OOPSLA paper in, time to sleep” is okay, but one describing the work or giving its title is not appropriate. Alternatively, a post with paper details to a group including only the colleagues at your institution is fine.
Reviewers will not be asked to recuse themselves from reviewing your paper unless they feel you have gone out of your way to advertise your authorship information to them.
All Dates
To reduce clutter in the calendar, we present only the immediately necessary dates. For reference, and for the historical record, all the important dates are listed below:
R1
R2
Submission
Tue 15 October
2024
Tue 25 March
2025
Author Response
Tue 3 Dec - Fri 6 Dec
Mon 26 May - Thu 29 May
Author Notification
Wed 18 Dec
Wed 18 June
Revision submission
Tue 4 February
2025
Tue 29 July
Author Notification
Tue 18 Feb
Tue 12 August
Camera Ready
Fri 28 Feb
Fri 22 August
Important Dates
AoE (UTC-12h)
Fri 22 Aug 2025
Camera Ready R2
Tue 12 Aug 2025
Author Notification of Revisions R2
Tue 29 Jul 2025
Submission of Revisions R2
Wed 18 Jun 2025
Author Notification R2
Mon 26 - Thu 29 May 2025
Author Response R2
Tue 25 Mar 2025
Submission R2
OOPSLA Review Committee
Shriram Krishnamurthi
Co-chair
Brown University
United States
Sukyoung Ryu
Co-chair
KAIST
South Korea
Işıl Dillig
Associate Chair
University of Texas at Austin
United States
Sebastian Erdweg
Associate Chair
KIT
Germany
Matthias Hauswirth
Associate Chair
USI Lugano
Switzerland
Zhenjiang Hu
Associate Chair
Peking University
China
Limin Jia
Associate Chair
Carnegie Mellon University
Alexandra Silva
Associate Chair
Cornell University
United States
KC Sivaramakrishnan
Associate Chair
IIT Madras and Tarides
India
Tobias Wrigstad
Associate Chair
Uppsala University
Sweden
Coşku Acay
Committee Member
Observe, Inc.
United States
Eddie Aftandilian
Committee Member
GitHub Next
United States
Alejandro Aguirre
Committee Member
Aarhus University
Denmark
Dalal Alrajeh
Committee Member
Imperial College London
United Kingdom
Dan Barowy
Committee Member
Williams College
United States
Guillaume Baudart
Committee Member
Inria
France
Rohan Bavishi
Committee Member
Amazon
United States
Julia Belyakova
Committee Member
Purdue University
United States
Dorra
Ben Khalifa
Committee Member
ENAC - University of Toulouse
France
Jasmin Blanchette
Committee Member
Ludwig-Maximilians-Universität München
Germany
Joanna
C. S. Santos
Committee Member
University of Notre Dame
United States
Sooyoung Cha
Committee Member
Sungkyunkwan University
Sen Chen
Committee Member
Nankai University
China
Yanju Chen
Committee Member
University of California, San Diego
United States
Alvin Cheung
Committee Member
University of California at Berkeley
United States
Michele Chiari
Committee Member
TU Wien
Austria
Benjamin Chung
Committee Member
JuliaHub
Tiago Cogumbreiro
Committee Member
University of Massachusetts Boston
United States
Loris D'Antoni
Committee Member
University of California at San Diego
United States
Francesco Dagnino
Committee Member
Maryam Mehri
Dehnavi
Committee Member
University of Toronto
Canada
Christos Dimoulas
Committee Member
Northwestern University
United States
Xiaoning Du
Committee Member
Monash University
Australia
Richard A.
Eisenberg
Committee Member
Jane Street
United States
Constantin Enea
Committee Member
LIX, CNRS, Ecole Polytechnique
Karine Even-Mendoza
Committee Member
King’s College London
United Kingdom
Pietro Ferrara
Committee Member
Ca’ Foscari University of Venice
Italy
Emily First
Committee Member
University of California, San Diego
United States
Nate Foster
Committee Member
Cornell University; Jane Street
United States
Michael Franz
Committee Member
University of California, Irvine
United States
Daniel Frumin
Committee Member
University of Groningen
Netherlands
Ronald Garcia
Committee Member
University of British Columbia
Canada
François Gauthier
Committee Member
Oracle Labs
Australia
Michael Greenberg
Committee Member
Stevens Institute of Technology
United States
Ben Greenman
Committee Member
University of Utah
United States
Ben Hardekopf
Committee Member
University of California at Santa Barbara
United States
Pinjia He
Committee Member
Chinese University of Hong Kong, Shenzhen
China
Martin Hirzel
Committee Member
IBM Research
United States
Jingmei Hu
Committee Member
Amazon
Shoaib Kamil
Committee Member
Adobe Research
Eunsuk Kang
Committee Member
Carnegie Mellon University
United States
Alex Kavvos
Committee Member
University of Bristol
United Kingdom
Hanjun Kim
Committee Member
Yonsei University
Eric Koskinen
Committee Member
Stevens Institute of Technology
United States
Nikita Koval
Committee Member
JetBrains
Netherlands
Krishna Nandivada
Committee Member
IIT Madras
Lindsey Kuper
Committee Member
University of California, Santa Cruz
United States
Christian Kästner
Committee Member
Carnegie Mellon University
Juneyoung Lee
Committee Member
AWS
Woosuk Lee
Committee Member
Hanyang University
South Korea
Caroline Lemieux
Committee Member
University of British Columbia
Canada
Ning Luo
Committee Member
UIUC
United States
Aravind Machiry
Committee Member
Purdue University
United States
Magnus Madsen
Committee Member
Aarhus University
Denmark
Michaël Marcozzi
Committee Member
Université Paris-Saclay, CEA, List
France
Stefan Marr
Committee Member
Johannes Kepler University Linz
Austria
Chris Martens
Committee Member
Northeastern University
United States
Ruben Martins
Committee Member
Carnegie Mellon University
United States
Kristóf Marussy
Committee Member
Budapest University of Technology and Economics
Hungary
Hidehiko Masuhara
Committee Member
Institute of Science Tokyo
Japan
Umang Mathur
Committee Member
National University of Singapore
Singapore
Angelica Moreira
Committee Member
Microsoft Research
Canada
Charlie Murphy
Committee Member
Amazon Web Services, USA
United States
Kartik Nagar
Committee Member
IIT Madras
India
Tomoki Nakamaru
Committee Member
The University of Tokyo
Japan
Hoan Nguyen
Committee Member
Amazon Web Services
James Noble
Committee Member
Independent. Wellington, NZ
New Zealand
Hakjoo Oh
Committee Member
Korea University
South Korea
Oded Padon
Committee Member
Weizmann Institute of Science
Israel
Pavel Parizek
Committee Member
Charles University
Jihyeok Park
Committee Member
Korea University
South Korea
Lionel Parreaux
Committee Member
HKUST (The Hong Kong University of Science and Technology)
Hong Kong SAR China
Daniel Perelman
Committee Member
Microsoft
United States
David Pichardie
Committee Member
Meta
France
Clément Pit-Claudel
Committee Member
EPFL
Switzerland
Azalea Raad
Committee Member
Imperial College London
United Kingdom
Arjun Radhakrishna
Committee Member
Microsoft
United States
Marianna Rapoport
Committee Member
Amazon Web Services
Canada
Baber Rehman
Committee Member
University of Hong Kong
Hong Kong SAR China
Manuel Rigger
Committee Member
National University of Singapore
Singapore
Manuel Serrano
Committee Member
Inria; Université Côte d’Azur
France
Jiasi Shen
Committee Member
The Hong Kong University of Science and Technology
Gagandeep Singh
Committee Member
University of Illinois at Urbana-Champaign; VMware Research
United States
Tyler Sorensen
Committee Member
Microsoft Research and University of California at Santa Cruz
United States
Caleb Stanford
Committee Member
University of California, Davis
United States
Jonathan Sterling
Committee Member
University of Cambridge
United Kingdom
Quentin Stiévenart
Committee Member
Université du Québec à Montréal
Canada
Felix Stutz
Committee Member
University of Luxembourg, Luxembourg
Vaishnavi Sundararajan
Committee Member
IIT Delhi
India
Milijana Surbatovich
Committee Member
University of Maryland
Gang (Gary)
Tan
Committee Member
Pennsylvania State University
United States
Tachio Terauchi
Committee Member
Waseda University
Japan
Bernardo Toninho
Committee Member
NOVA-LINCS; Nova University of Lisbon
Portugal
Yakir Vizel
Committee Member
Technion—Israel Institute of Technology
Israel
Wenxi Wang
Committee Member
University of Virgina
United States
Xinyu Wang
Committee Member
University of Michigan
United States
Conrad Watt
Committee Member
Nanyang Technological University
Singapore
Guannan Wei
Committee Member
Tufts University
United States
John Wickerson
Committee Member
Imperial College London
United Kingdom
Christian Wimmer
Committee Member
Amazon Web Services
United States
Peisen Yao
Committee Member
Zhejiang University
China
Nobuko Yoshida
Committee Member
University of Oxford
United Kingdom
Yannick Zakowski
Committee Member
Inria
France
Jialu Zhang
Committee Member
University of Waterloo
Canada
Xiangyu Zhang
Committee Member
Purdue University
United States
External Review / Artifact Evaluation Committee
No members yet
Fri 24 Apr 12:04