SPLASH 2024
Sun 20 - Fri 25 October 2024
Pasadena, California, United States
Toggle navigation
Attending
Venue: Hilton Pasadena
Students
Registration
Visa Support Letters
Sponsoring
Code of conduct
Instructions for Presenters
Chair's Welcome
How to SPLASH (Quick Attendee Guide)
Mt. Baldy Bicycle Trip
Attractions Around Pasadena
Live Stream
Program
SPLASH Program
Your Program
Sun 20 Oct
Mon 21 Oct
Tue 22 Oct
Wed 23 Oct
Thu 24 Oct
Fri 25 Oct
Tracks
SPLASH 2024
DEI Activities
Doctoral Symposium
Keynotes
OOPSLA 2024
OOPSLA Artifacts
Onward! Essays
Onward! Papers
PLMW
Posters
REBASE
SPLASH-E
Student Research Competition
Volunteers
Workshops
Co-hosted Conferences
GPCE
SLE
Workshops
HATRA
IWACO
JENSFEST
LIVE
NSAD
PAINT
ProLaLa
UNSOUND
VIVEKFEST
VMIL
VMIL
- A tour of CPython's runtime
Co-hosted Symposia
SAS
SAS
SAS
Artifacts
Organization
SPLASH 2024 Committees
Organizing Committee
Steering Committee
Track Committees
Doctoral Symposium
OOPSLA 2024
OOPSLA Artifacts
Onward! Essays
Program Committee
Onward! Steering Committee
Onward! Papers
Program Committee
Steering Committee
PLMW
Organizing Committee
Speakers & Panelists
Mentors
Posters
REBASE
SPLASH-E
Program Commitee
Steering Committee
Student Research Competition
Organizers
Reviewers
Volunteers
Workshops
Contributors
People Index
Co-hosted Conferences
GPCE
Organizing Committee
Program Committee
Steering Committee
SLE
Organizing Committee
Program Committee
Artifact Evaluation Committee
Steering Committee
Workshops
HATRA
Organizing Committee
Program Committee
IWACO
Organizing Committee
Program Committee
JENSFEST
Organizing Committee
Program Committee
LIVE
Organizing Committee
Program Committee
NSAD
Organizing Committee
Program Committee
PAINT
Organizing Committee
Program Committee
ProLaLa
Organizing Committee
Program Committee
UNSOUND
Organizing Committee
VIVEKFEST
Organizing Committee
Program Committee
VMIL
Organizing Committee
Program Committee
Co-hosted Symposia
SAS
SAS 2024
Organizing Committee
SAS 2024
Program Committee
SAS Artifacts
Search
Series
Series
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
Sign in
Sign up
SPLASH 2024
(
series
) /
Hilton Pasadena
/
Room information: San Gabriel
Venue
Hilton Pasadena
Room name
San Gabriel
Room Information
No extra information available
Program
Detailed Table
Session Timeline
Detailed Timeline
Program Display Configuration
Time Zone
The program is currently displayed in
(GMT-07:00) Pacific Time (US & Canada)
.
Use conference time zone: (GMT-07:00) Pacific Time (US & Canada)
Select other time zone
(GMT-12:00) AoE (Anywhere On Earth)
(GMT-11:00) Midway Island, Samoa
(GMT-09:00) Hawaii-Aleutian
(GMT-10:00) Hawaii
(GMT-09:30) Marquesas Islands
(GMT-09:00) Gambier Islands
(GMT-08:00) Alaska
(GMT-07:00) Tijuana, Baja California
(GMT-08:00) Pitcairn Islands
(GMT-07:00) Pacific Time (US & Canada)
(GMT-06:00) Mountain Time (US & Canada)
(GMT-06:00) Chihuahua, La Paz, Mazatlan
(GMT-07:00) Arizona
(GMT-06:00) Saskatchewan, Central America
(GMT-05:00) Guadalajara, Mexico City, Monterrey
(GMT-05:00) Easter Island
(GMT-05:00) Central Time (US & Canada)
(GMT-04:00) Eastern Time (US & Canada)
(GMT-04:00) Cuba
(GMT-05:00) Bogota, Lima, Quito, Rio Branco
(GMT-04:00) Caracas
(GMT-03:00) Santiago
(GMT-04:00) La Paz
(GMT-03:00) Faukland Islands
(GMT-04:00) Manaus, Amazonas, Brazil
(GMT-03:00) Atlantic Time (Goose Bay)
(GMT-03:00) Atlantic Time (Canada)
(GMT-02:30) Newfoundland
(GMT-03:00) UTC-3
(GMT-03:00) Montevideo
(GMT-02:00) Miquelon, St. Pierre
(GMT-02:00) Greenland
(GMT-03:00) Buenos Aires
(GMT-03:00) Brasilia, Distrito Federal, Brazil
(GMT-02:00) Mid-Atlantic
(GMT-01:00) Cape Verde Is.
(GMT) Azores
(UTC) Coordinated Universal Time
(GMT+01:00) Belfast
(GMT+01:00) Dublin
(GMT+01:00) Lisbon
(GMT+01:00) London
(GMT) Monrovia, Reykjavik
(GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
(GMT+02:00) Belgrade, Bratislava, Budapest, Ljubljana, Prague
(GMT+02:00) Brussels, Copenhagen, Madrid, Paris
(GMT+01:00) West Central Africa
(GMT+02:00) Windhoek
(GMT+03:00) Athens
(GMT+03:00) Beirut
(GMT+02:00) Cairo
(GMT+03:00) Gaza
(GMT+02:00) Harare, Pretoria
(GMT+03:00) Jerusalem
(GMT+03:00) Minsk
(GMT+03:00) Syria
(GMT+03:00) Moscow, St. Petersburg, Volgograd
(GMT+03:00) Nairobi
(GMT+03:30) Tehran
(GMT+04:00) Abu Dhabi, Muscat
(GMT+04:00) Yerevan
(GMT+04:30) Kabul
(GMT+05:00) Ekaterinburg
(GMT+05:00) Tashkent
(GMT+05:30) Chennai, Kolkata, Mumbai, New Delhi
(GMT+05:45) Kathmandu
(GMT+06:00) Astana, Dhaka
(GMT+07:00) Novosibirsk
(GMT+06:30) Yangon (Rangoon)
(GMT+07:00) Bangkok, Hanoi, Jakarta
(GMT+07:00) Krasnoyarsk
(GMT+08:00) Beijing, Chongqing, Hong Kong, Urumqi
(GMT+08:00) Irkutsk, Ulaan Bataar
(GMT+08:00) Perth
(GMT+08:45) Eucla
(GMT+09:00) Osaka, Sapporo, Tokyo
(GMT+09:00) Seoul
(GMT+09:00) Yakutsk
(GMT+10:30) Adelaide
(GMT+09:30) Darwin
(GMT+10:00) Brisbane
(GMT+11:00) Hobart
(GMT+10:00) Vladivostok
(GMT+11:00) Lord Howe Island
(GMT+11:00) Solomon Is., New Caledonia
(GMT+11:00) Magadan
(GMT+12:00) Norfolk Island
(GMT+12:00) Anadyr, Kamchatka
(GMT+13:00) Auckland, Wellington
(GMT+12:00) Fiji, Kamchatka, Marshall Is.
(GMT+13:45) Chatham Islands
(GMT+13:00) Nuku'alofa
(GMT+14:00) Kiritimati
The GMT offsets shown reflect the offsets
at the moment of the conference
.
Time Band
By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.
Display full program
Specify a time band
-
Save
×
You're viewing the program in a time zone which is different from your device's time zone
change time zone
Sun 20 Oct
Displayed time zone:
Pacific Time (US & Canada)
change
09:00 - 10:30
Modularity and Memory Analysis
SAS
at
San Gabriel
Chair(s):
Roberto Giacobazzi
University of Arizona
09:00
60m
Keynote
Static Analysis Sparsity and Modularity
SAS
Kwangkeun Yi
Seoul National University
10:00
30m
Under-approximating Memory Abstractions
SAS
Marco Milanese
Sorbonne University
,
Antoine Miné
Sorbonne Université
Pre-print
11:00 - 12:30
Types, Control-flow and trace partitioning
SAS
at
San Gabriel
Chair(s):
Michele Pasqua
University of Verona
11:00
30m
Full-paper
BinSub: The Simple Essence of Polymorphic Type Inference for Machine Code
SAS
Ian Smith
Trail of Bits
Pre-print
11:30
30m
Full-paper
Full Control-Flow Sensitivity for Definitional Interpreters
SAS
Kimball Germane
Brigham Young University
Pre-print
12:00
30m
Full-paper
Trace Partitioning as an Optimization Problem
SAS
Charles Babu M
CEA-List
,
Matthieu Lemerre
Université Paris-Saclay - CEA LIST
,
Sébastien Bardin
CEA LIST, University Paris-Saclay
,
Jean-Yves Marion
LORIA
Pre-print
14:00 - 15:30
Machine learning and Neural networks
SAS
at
San Gabriel
Chair(s):
Marco Campion
INRIA & École Normale Supérieure | Université PSL
14:00
60m
Tutorial
Abstract Interpretation-Based Certification of Hyperproperties for High-Stakes Machine Learning Software
SAS
Caterina Urban
Inria - École Normale Supérieure
15:00
30m
Full-paper
Robustness Verification of Multi-Label Neural Network Classifiers
SAS
Julian Mour
,
Dana Drachsler Cohen
Technion
Pre-print
16:00 - 17:30
Machine Learning and Neural networks
SAS
at
San Gabriel
Chair(s):
Marco Campion
INRIA & École Normale Supérieure | Université PSL
16:00
30m
Full-paper
Abstract Interpretation of ReLU Neural Networks with Optimizable Polynomial Relaxations
SAS
Philipp Kern
Karlsruhe Institute of Technology (KIT)
,
Carsten Sinz
Karlsruhe Institute of Technology
Pre-print
16:30
30m
Short-paper
ConstraintFlow: A DSL for Specification and Verification of Neural Network Analyses (NEAT paper)
SAS
Avaljot Singh
UIUC
,
Yasmin Sarita
Cornell University
,
Charith Mendis
University of Illinois at Urbana-Champaign
,
Gagandeep Singh
University of Illinois at Urbana-Champaign; VMware Research
Pre-print
Mon 21 Oct
Displayed time zone:
Pacific Time (US & Canada)
change
09:00 - 10:30
Authorisation and responsibility
SAS
at
San Gabriel
Chair(s):
Patrick Cousot
09:00
60m
Tutorial
A New Language for Expressive, Fast, Safe, and Analyzable Authorization
SAS
Emina Torlak
Amazon Web Services, USA
10:00
30m
Full-paper
On the Role of Cognizance in Responsibility
SAS
Laura Canaia
,
Mila Dalla Preda
University of Verona
Pre-print
11:00 - 12:30
Verification cost and quantitative analysis
SAS
at
San Gabriel
Chair(s):
Sébastien Bardin
CEA LIST, University Paris-Saclay
11:00
30m
Full-paper
Verification of programs with ADTs using Shallow Horn Clauses
SAS
Théo Losekoot
,
Thomas Genet
IRISA, Univ Rennes
,
Thomas P. Jensen
INRIA Rennes
Pre-print
11:30
30m
Full-paper
An Order Theory Framework of Recurrence Equations for Static Cost Analysis – Dynamic Inference of Non-Linear Inequality Invariants
SAS
Louis Rustenholz
Universidad Politécnica de Madrid (UPM) and IMDEA Software Institute
,
Pedro López-García
IMDEA Software Institute
,
José Morales
IMDEA Software Institute
,
Manuel Hermenegildo
Technical University of Madrid (UPM) and IMDEA Software Institute
Link to publication
Pre-print
File Attached
12:00
30m
Full-paper
Quantitative Static Timing Analysis
SAS
Denis Mazzucato
INRIA & École Normale Supérieure
,
Marco Campion
INRIA & École Normale Supérieure | Université PSL
,
Caterina Urban
Inria - École Normale Supérieure
Pre-print
14:00 - 15:30
Quantum and system level analysis
SAS
at
San Gabriel
Chair(s):
Qirun Zhang
Georgia Institute of Technology
14:00
30m
Short-paper
Fixing Latent Unsound Abstract Operators in the eBPF Verifier of the Linux Kernel (NEAT paper)
SAS
Matan Shachnai
,
Harishankar Vishwanathan
,
Srinivas Narayana
Rutgers University
,
Santosh Nagarakatte
Rutgers University
Pre-print
14:30
30m
Full-paper
Static Analysis of Quantum Programs
SAS
Nicola Assolini
University of Verona
,
Alessandra Di Pierro
University of Verona
,
Isabella Mastroeni
University of Verona
Pre-print
15:00
30m
Short-paper
Verifying components of Arm® Confidential Computing Architecture with ESBMC (NEAT paper)
SAS
Tong Wu
,
Shale Xiong
ARM
,
Edoardo Manino
,
Gareth Stockwell
ARM
,
Lucas C. Cordeiro
University of Manchester, UK and Federal University of Amazonas, Brazil
Pre-print
16:00 - 17:30
Radhia Cousot Award and SAS24 Business Meeting
SAS
at
San Gabriel
Chair(s):
Marco Campion
INRIA & École Normale Supérieure | Université PSL
,
Roberto Giacobazzi
University of Arizona
,
Alessandra Gorla
IMDEA Software Institute
16:00
60m
Meeting
Radhia Cousot Award and Business Meeting
SAS
Tue 22 Oct
Displayed time zone:
Pacific Time (US & Canada)
change
09:00 - 10:30
Automatising Program Analysis
SAS
at
San Gabriel
Chair(s):
Manuel Hermenegildo
Technical University of Madrid (UPM) and IMDEA Software Institute
09:00
60m
Keynote
What's Still Missing in Static Analysis? A Decade-Long Journey.
SAS
Mayur Naik
University of Pennsylvania
10:00
30m
Full-paper
Synthesizing Abstract Transformers for Reduced-Product Domains
SAS
Pankaj Kumar Kalita
IIT Kanpur
,
Thomas Reps
University of Wisconsin-Madison
,
Subhajit Roy
IIT Kanpur
Pre-print
11:00 - 12:30
Tracing bugs and flaws
SAS
at
San Gabriel
Chair(s):
Aditya V. Thakur
University of California at Davis
11:00
60m
Keynote
Measuring data lineage: when program analysis meets data science
SAS
Francesco Logozzo
Meta
12:00
30m
Full-paper
Lift-offline: Instruction Lifter Generators
SAS
Nicholas Coughlin
Defence Science and Technology Group, Australia
,
Alistair Michael
,
Kait Lam
Pre-print
14:00 - 15:30
System level analysis
SAS
at
San Gabriel
Chair(s):
Roberto Giacobazzi
University of Arizona
14:00
30m
Full-paper
GoGuard: Efficient Static Blocking Bug Detection for Go
SAS
Dhruti Joshi
,
Bozhen Liu
Texas A&M University - Corpus Christi
Pre-print
14:30
30m
Short-paper
Should We Balance? Towards Formal Verification of the Linux Kernel Scheduler (NEAT paper)
SAS
Julia Lawall
Inria
,
Keisuke Nishimura
,
Jean-Pierre Lozi
Pre-print
File Attached
Wed 23 Oct
Displayed time zone:
Pacific Time (US & Canada)
change
10:40 - 12:20
Semantics
OOPSLA 2024
at
San Gabriel
Chair(s):
Ilya Sergey
National University of Singapore
10:40
20m
Talk
A Pure Demand Operational Semantics with Applications to Program Analysis
OOPSLA 2024
Scott F. Smith
The Johns Hopkins University
,
Robert Zhang
The University of Texas at Austin, The Johns Hopkins University
Link to publication
DOI
Pre-print
11:00
20m
Talk
Automating Pruning in Top-Down Enumeration for Program Synthesis Problems with Monotonic Semantics
OOPSLA 2024
Keith J.C. Johnson
University of Wisconsin–Madison
,
Rahul Krishnan
University of Wisconsin-Madison
,
Thomas Reps
University of Wisconsin-Madison
,
Loris D'Antoni
University of Wisconsin-Madison
DOI
Pre-print
11:20
20m
Talk
HOL4P4: mechanized small-step semantics for P4
OOPSLA 2024
Anoud Alshnakat
KTH Royal Institute of Technology
,
Didrik Lundberg
KTH Royal Institute of Technology and Saab AB
,
Roberto Guanciale
KTH Royal Institute of Technology
,
Mads Dam
KTH
DOI
11:40
20m
Talk
Semantics Lifting for Syntactic Sugar
OOPSLA 2024
Zhichao Guan
Peking University
,
Yiyuan Cao
Peking University
,
Tailai Yu
Tsinghua University
,
Ziheng Wang
,
Di Wang
Peking University
,
Zhenjiang Hu
Peking University
DOI
12:00
20m
Talk
Synthesizing Formal Semantics from Executable Interpreters
OOPSLA 2024
Jiangyi Liu
University of Wisconsin - Madison
,
Charlie Murphy
University of Wisconsin–Madison
,
Anvay Grover
University of Wisconsin-Madison
,
Keith J.C. Johnson
University of Wisconsin–Madison
,
Thomas Reps
University of Wisconsin-Madison
,
Loris D'Antoni
University of Wisconsin-Madison
DOI
Pre-print
13:40 - 15:20
Formal Methods 1
OOPSLA 2024
at
San Gabriel
Chair(s):
Benjamin Delaware
Purdue University
13:40
20m
Talk
Realistic Realizability: Specifying ABIs You Can Count On
OOPSLA 2024
Andrew Wagner
Northeastern University
,
Zachary Eisbach
Northeastern University
,
Amal Ahmed
Northeastern University, USA
DOI
14:00
20m
Talk
AUTOMAP: Inferring Rank-Polymorphic Function Applications with Integer Linear Programming
OOPSLA 2024
Robert Schenck
DIKU, University of Copenhagen
,
Nikolaj Hey Hinnerskov
DIKU, University of Copenhagen
,
Troels Henriksen
University of Copenhagen
,
Magnus Madsen
Aarhus University
,
Martin Elsman
University of Copenhagen
DOI
14:20
20m
Talk
Outcome Separation Logic: Local Reasoning for Correctness and Incorrectness with Computational Effects
OOPSLA 2024
Noam Zilberstein
Cornell University
,
Angelina Saliling
Cornell University
,
Alexandra Silva
Cornell University
DOI
14:40
20m
Talk
VarLifter: Recovering Variables and Types from Bytecode of Solidity Smart Contracts
OOPSLA 2024
Yichuan Li
Nanjing University of Science and Technology
,
Wei Song
Nanjing University of Science and Technology
,
Jeff Huang
Texas A&M University
DOI
15:00
20m
Talk
Weighted Context-Free-Language Ordered Binary Decision Diagrams
OOPSLA 2024
Meghana Aparna Sistla
The University of Texas at Austin
,
Swarat Chaudhuri
University of Texas at Austin
,
Thomas Reps
University of Wisconsin-Madison
DOI
16:00 - 17:40
Formal Methods 2
OOPSLA 2024
at
San Gabriel
Chair(s):
Bor-Yuh Evan Chang
University of Colorado Boulder & Amazon
16:00
20m
Talk
A Constraint Solving Approach to Parikh Images of Regular Languages
OOPSLA 2024
Amanda Stjerna
Uppsala university
,
Philipp Rümmer
University of Regensburg and Uppsala University
DOI
16:20
20m
Talk
Imperative Compositional Programming: Type Sound Distributive Intersection Subtyping with References via Bidirectional Typing
OOPSLA 2024
Wenjia Ye
National University of Singapore
,
Yaozhu Sun
University of Hong Kong
,
Bruno C. d. S. Oliveira
University of Hong Kong
DOI
16:40
20m
Talk
Inductive diagrams for causal reasoning
OOPSLA 2024
Jonathan Castello
University of California, Santa Cruz
,
Patrick Redmond
University of California at Santa Cruz
,
Lindsey Kuper
University of California, Santa Cruz
DOI
Pre-print
17:00
20m
Talk
Message-Observing Sessions
OOPSLA 2024
Ryan Kavanagh
Université du Québec à Montréal (UQAM)
,
Brigitte Pientka
McGill University
DOI
17:20
20m
Talk
Plume: Efficient and Complete Black-box Checking of Weak Isolation Levels
OOPSLA 2024
Si Liu
ETH Zurich
,
Long Gu
State Key Laboratory for Novel Software Technology, Nanjing University
,
Hengfeng Wei
State Key Laboratory for Novel Software Technology, Nanjing University
,
David Basin
ETH Zurich
DOI
Thu 24 Oct
Displayed time zone:
Pacific Time (US & Canada)
change
10:40 - 12:20
Compilers and Optimisation 1
OOPSLA 2024
at
San Gabriel
Chair(s):
Emery D. Berger
University of Massachusetts Amherst
10:40
20m
Talk
Compilation of Shape Operators on Sparse Arrays
OOPSLA 2024
Alexander J Root
Stanford University
,
Bobby Yan
Stanford University
,
Peiming Liu
Google Inc
,
Christophe Gyurgyik
Stanford University
,
Aart Bik
Google, Inc.
,
Fredrik Kjolstad
Stanford University
DOI
Pre-print
11:00
20m
Talk
Compiler Support for Sparse Tensor Convolutions
OOPSLA 2024
Peiming Liu
Google Inc
,
Alexander J Root
Stanford University
,
Anlun Xu
Google
,
Yinying Li
Google
,
Fredrik Kjolstad
Stanford University
,
Aart Bik
Google, Inc.
DOI
11:20
20m
Talk
Compiling Recurrences over Dense and Sparse Arrays
OOPSLA 2024
Shiv Sundram
Stanford University
,
Muhammad Usman Tariq
Stanford University
,
Fredrik Kjolstad
Stanford University
DOI
11:40
20m
Talk
Fully Verified Instruction Scheduling
OOPSLA 2024
Ziteng Yang
Georgia Institute of Technology
,
Jun Shirako
Georgia Institute of Technology
,
Vivek Sarkar
Georgia Institute of Technology
DOI
Pre-print
12:00
20m
Talk
Homeostasis: Design and Implementation of a Self-Stabilizing Compiler (TOPLAS)
OOPSLA 2024
Aman Nougrahiya
IIT Madras
,
V Krishna Nandivada
IIT Madras
Link to publication
13:40 - 15:20
Compilers and Optimisation 2
OOPSLA 2024
at
San Gabriel
Chair(s):
Manu Sridharan
University of California at Riverside
13:40
20m
Talk
Hydra: Generalizing Peephole Optimizations with Program Synthesis
OOPSLA 2024
Manasij Mukherjee
NVIDIA
,
John Regehr
University of Utah
DOI
Pre-print
14:00
20m
Talk
Minotaur: A SIMD-Oriented Synthesizing Superoptimizer
OOPSLA 2024 Distinguished Paper Award
OOPSLA 2024
Zhengyang Liu
University of Utah
,
Stefan Mada
University of Utah
,
John Regehr
University of Utah
DOI
14:20
20m
Talk
PolyJuice: Detecting Mis-Compilation Bugs in Tensor Compilers with Equality Saturation Based Rewriting
OOPSLA 2024
Chijin Zhou
Tsinghua University
,
Bingzhou Qian
National University of Defense Technology
,
Gwihwan Go
Tsinghua University
,
Quan Zhang
Tsinghua University
,
Shanshan Li
National University of Defense Technology
,
Yu Jiang
Tsinghua University
DOI
14:40
20m
Talk
SparseAuto: An Auto-Scheduler for Sparse Tensor Computations Using Recursive Loop Nest Restructuring
OOPSLA 2024
Adhitha Dias
Purdue University, USA
,
Logan Anderson
Purdue University
,
Kirshanthan Sundararajah
Virginia Tech
,
Artem Pelenitsyn
Purdue University
,
Milind Kulkarni
Purdue University
DOI
Pre-print
15:00
20m
Talk
Understanding and Finding Java Decompiler Bugs
OOPSLA 2024
Yifei Lu
Nanjing University
,
Weidong Hou
Nanjing University
,
Minxue Pan
Nanjing University
,
Xuandong Li
Nanjing University
,
Zhendong Su
ETH Zurich
DOI
16:00 - 17:40
Probabilistic Programming and Analysis 1
OOPSLA 2024
at
San Gabriel
Chair(s):
Di Wang
Peking University
16:00
20m
Talk
A modal type-theory of expected cost in higher-order probabilistic programs
Remote
OOPSLA 2024
Vineet Rajani
University of Kent
,
Gilles Barthe
MPI-SP; IMDEA Software Institute
,
Deepak Garg
MPI-SWS
DOI
16:20
20m
Talk
Distributions for Compositionally Differentiating Parametric Discontinuities
OOPSLA 2024
Jesse Michel
Massachusetts Institute of Technology
,
Kevin Mu
University of Washington
,
Xuanda Yang
University of California San Diego
,
Sai Praveen Bangaru
MIT
,
Elias Rojas Collins
MIT
,
Gilbert Bernstein
University of Washington, Seattle
,
Jonathan Ragan-Kelley
Massachusetts Institute of Technology
,
Michael Carbin
Massachusetts Institute of Technology
,
Tzu-Mao Li
Massachusetts Institute of Technology; University of California at San Diego
DOI
16:40
20m
Talk
Exact Bayesian Inference for Loopy Probabilistic Programs Using Generating Functions
OOPSLA 2024
Lutz Klinkenberg
RWTH Aachen University
,
Christian Blumenthal
RWTH Aachen University
,
Mingshuai Chen
Zhejiang University
,
Darion Haase
RWTH Aachen University
,
Joost-Pieter Katoen
RWTH Aachen University
DOI
17:00
20m
Talk
Hopping Proofs of Expectation-Based Properties: Applications to Skiplists and Security Proofs
OOPSLA 2024
Martin Avanzini
Inria
,
Gilles Barthe
MPI-SP; IMDEA Software Institute
,
Benjamin Gregoire
INRIA
,
Georg Moser
University of Innsbruck
,
Gabriele Vanoni
IRIF, Université Paris Cité
DOI
17:20
20m
Talk
Learning Abstraction Selection for Bayesian Program Analysis
OOPSLA 2024
Yifan Zhang
Peking University
,
Yuanfeng Shi
Peking University
,
Xin Zhang
Peking University
DOI
Pre-print
Fri 25 Oct
Displayed time zone:
Pacific Time (US & Canada)
change
11:00 - 12:20
Memory Management and Analysis 1
OOPSLA 2024
at
San Gabriel
Chair(s):
Amal Ahmed
Northeastern University, USA
11:00
20m
Talk
A Dependent Nominal Physical Type System for Static Analysis of Memory in Low Level Code
OOPSLA 2024
Julien Simonnet
CEA LIST
,
Matthieu Lemerre
Université Paris-Saclay - CEA LIST
,
Mihaela Sighireanu
University Paris-Saclay, ENS Paris-Saclay, CNRS, LMF
DOI
11:20
20m
Talk
Modeling Dynamic (De)Allocations of Local Memory for Translation Validation
OOPSLA 2024
Abhishek Rose
IIT Delhi
,
Sorav Bansal
IIT Delhi and CompilerAI Labs
DOI
11:40
20m
Talk
Mark--Scavenge: Waiting for Trash to Take Itself Out
OOPSLA 2024
Jonas Norlinder
Uppsala University
,
Erik Österlund
Oracle
,
David Black-Schaffer
Uppsala University
,
Tobias Wrigstad
Uppsala University
DOI
12:00
20m
Talk
Iris-MSWasm: elucidating and mechanising the security invariants of Memory-Safe WebAssembly
OOPSLA 2024
Maxime Legoupil
Aarhus University
,
June Rousseau
Aarhus University
,
Aina Linn Georges
Max Planck Institute for Software Systems (MPI-SWS)
,
Jean Pichon-Pharabod
Aarhus University
,
Lars Birkedal
Aarhus University
DOI
13:50 - 15:30
Program Synthesis and Verification 2
OOPSLA 2024
at
San Gabriel
Chair(s):
Tony Hosking
Australian National University
13:50
20m
Talk
Automating Unrealizability Logic: Hoare-style Proof Synthesis for Infinite Sets of Programs
OOPSLA 2024
Shaan Nagy
University of Wisconsin-Madison
,
Jinwoo Kim
Seoul National University
,
Thomas Reps
University of Wisconsin-Madison
,
Loris D'Antoni
University of Wisconsin-Madison
DOI
14:10
20m
Talk
Compositionality and Observational Refinement for Linearizability with Crashes
OOPSLA 2024
Arthur Oliveira Vale
Yale University
,
Zhongye Wang
Shanghai Jiao Tong University
,
Yixuan Chen
Yale University
,
Peixin You
Yale University
,
Zhong Shao
Yale University
DOI
14:30
20m
Talk
Hypra: A Deductive Program Verifier for Hyper Hoare Logic
OOPSLA 2024
Thibault Dardinier
ETH Zurich
,
Anqi Li
ETH Zurich
,
Peter Müller
ETH Zurich
DOI
14:50
20m
Talk
SMT2Test: From SMT Formulas to Effective Test Cases
OOPSLA 2024
Chengyu Zhang
ETH Zurich
,
Zhendong Su
ETH Zurich
DOI
15:10
20m
Talk
Validating SMT Solvers for Correctness and Performance via Grammar-based Enumeration
OOPSLA 2024
Dominik Winterer
ETH Zurich
,
Zhendong Su
ETH Zurich
DOI
16:00 - 17:40
Memory Management and Analysis 2
OOPSLA 2024
at
San Gabriel
Chair(s):
Michael D. Bond
Ohio State University
16:00
20m
Talk
Making Sense of Multi-Threaded Application Performance at Scale with NonSequitur
OOPSLA 2024
Augustine Wong
University of British Columbia
,
Paul Bucci
University of British Columbia
,
Ivan Beschastnikh
University of British Columbia
,
Alexandra (Sasha) Fedorova
University of British Columbia
DOI
Media Attached
16:20
20m
Talk
A Runtime System for Interruptible Query Processing -- When Incremental Computing Meets Fine-Grained Parallelism
OOPSLA 2024
Jeffrey Eymer
SUNY Binghamton
,
Philip Dexter
SUNY Binghamton
,
Joseph Raskind
SUNY Binghamton
,
Yu David Liu
SUNY Binghamton
DOI
16:40
20m
Talk
PROMPT: A Fast and Extensible Memory Profiling Framework
OOPSLA 2024
Ziyang Xu
Princeton / AWS
,
Yebin Chon
Princeton University
,
Yian Su
Northwestern University
,
Zujun Tan
Princeton University, USA
,
Sotiris Apostolakis
Google
,
Simone Campanoni
Northwestern University
,
David I. August
Princeton University
DOI
17:00
20m
Talk
Semantics of Remote Direct Memory Access: Operational and Declarative Models of RDMA on TSO Architectures
OOPSLA 2024
Guillaume Ambal
,
Brijesh Dongol
University of Surrey
,
Haggai Eran
NVIDIA
,
Vasileios Klimis
Queen Mary University of London
,
Ori Lahav
Tel Aviv University
,
Azalea Raad
Imperial College London
DOI
17:20
20m
Talk
StarMalloc: Verifying a Modern, Hardened Memory Allocator
OOPSLA 2024
Antonin Reitz
Inria
,
Aymeric Fromherz
Inria
,
Jonathan Protzenko
Microsoft Azure Research
DOI
Sun 20 Oct
Displayed time zone:
Pacific Time (US & Canada)
change
Room
9:00
30
10:00
30
11:00
30
12:00
30
13:00
30
14:00
30
15:00
30
16:00
30
17:00
30
San Gabriel
SAS
Modularity and Memory Analysis
SAS
Types, Control-flow and trace partitioning
SAS
Machine learning and Neural networks
SAS
Machine Learning and Neural networks
Mon 21 Oct
Displayed time zone:
Pacific Time (US & Canada)
change
Room
9:00
30
10:00
30
11:00
30
12:00
30
13:00
30
14:00
30
15:00
30
16:00
30
17:00
30
San Gabriel
SAS
Authorisation and responsibility
SAS
Verification cost and quantitative analysis
SAS
Quantum and system level analysis
SAS
Radhia Cousot Award and SAS24 Business Meeting
Tue 22 Oct
Displayed time zone:
Pacific Time (US & Canada)
change
Room
9:00
30
10:00
30
11:00
30
12:00
30
13:00
30
14:00
30
15:00
30
16:00
30
17:00
30
San Gabriel
SAS
Automatising Program Analysis
SAS
Tracing bugs and flaws
SAS
System level analysis
SAS
Wed 23 Oct
Displayed time zone:
Pacific Time (US & Canada)
change
Room
10:00
30
11:00
30
12:00
30
13:00
30
14:00
30
15:00
30
16:00
30
17:00
30
San Gabriel
OOPSLA 2024
Semantics
OOPSLA 2024
Formal Methods 1
OOPSLA 2024
Formal Methods 2
Thu 24 Oct
Displayed time zone:
Pacific Time (US & Canada)
change
Room
10:00
30
11:00
30
12:00
30
13:00
30
14:00
30
15:00
30
16:00
30
17:00
30
San Gabriel
OOPSLA 2024
Compilers and Optimisation 1
OOPSLA 2024
Compilers and Optimisation 2
OOPSLA 2024
Probabilistic Programming and Analysis 1
Fri 25 Oct
Displayed time zone:
Pacific Time (US & Canada)
change
Room
11:00
30
12:00
30
13:00
30
14:00
30
15:00
30
16:00
30
17:00
30
San Gabriel
OOPSLA 2024
Memory Management and Analysis 1
OOPSLA 2024
Program Synthesis and Verification 2
OOPSLA 2024
Memory Management and Analysis 2
Sun 20 Oct
Displayed time zone:
Pacific Time (US & Canada)
change
Room
9:00
15
30
45
10:00
15
30
45
11:00
15
30
45
12:00
15
30
45
13:00
15
30
45
14:00
15
30
45
15:00
15
30
45
16:00
15
30
45
San Gabriel
SAS
Static Analysis Sparsity and Modularity
09:00 - 10:00
SAS
Under-approximating Memory Abstractions
10:00 - 10:30
SAS
BinSub: The Simple Essence of Polymorphic Type Inference for Machine Code
11:00 - 11:30
SAS
Full Control-Flow Sensitivity for Definitional Interpreters
11:30 - 12:00
SAS
Trace Partitioning as an Optimization Problem
12:00 - 12:30
SAS
Abstract Interpretation-Based Certification of Hyperproperties for High ...
14:00 - 15:00
SAS
Robustness Verification of Multi-Label Neural Network Classifiers
15:00 - 15:30
SAS
Abstract Interpretation of ReLU Neural Networks with Optimizable Polyno ...
16:00 - 16:30
SAS
ConstraintFlow: A DSL for Specification and Verification of Neural Netw ...
16:30 - 17:00
Mon 21 Oct
Displayed time zone:
Pacific Time (US & Canada)
change
Room
9:00
15
30
45
10:00
15
30
45
11:00
15
30
45
12:00
15
30
45
13:00
15
30
45
14:00
15
30
45
15:00
15
30
45
16:00
15
30
45
San Gabriel
SAS
A New Language for Expressive, Fast, Safe, and Analyzable Authorization
09:00 - 10:00
SAS
On the Role of Cognizance in Responsibility
10:00 - 10:30
SAS
Verification of programs with ADTs using Shallow Horn Clauses
11:00 - 11:30
SAS
An Order Theory Framework of Recurrence Equations for Static Cost Analy ...
11:30 - 12:00
SAS
Quantitative Static Timing Analysis
12:00 - 12:30
SAS
Fixing Latent Unsound Abstract Operators in the eBPF Verifier of the Li ...
14:00 - 14:30
SAS
Static Analysis of Quantum Programs
14:30 - 15:00
SAS
Verifying components of Arm® Confidential Computing Architecture with E ...
15:00 - 15:30
SAS
Radhia Cousot Award and Business Meeting
16:00 - 17:00
Tue 22 Oct
Displayed time zone:
Pacific Time (US & Canada)
change
Room
9:00
15
30
45
10:00
15
30
45
11:00
15
30
45
12:00
15
30
45
13:00
15
30
45
14:00
15
30
45
San Gabriel
SAS
What's Still Missing in Static Analysis? A Decade-Long Journey.
09:00 - 10:00
SAS
Synthesizing Abstract Transformers for Reduced-Product Domains
10:00 - 10:30
SAS
Measuring data lineage: when program analysis meets data science
11:00 - 12:00
SAS
Lift-offline: Instruction Lifter Generators
12:00 - 12:30
SAS
GoGuard: Efficient Static Blocking Bug Detection for Go
14:00 - 14:30
SAS
Should We Balance? Towards Formal Verification of the Linux Kernel Sche ...
14:30 - 15:00
Wed 23 Oct
Displayed time zone:
Pacific Time (US & Canada)
change
Room
10:00
15
30
45
11:00
15
30
45
12:00
15
30
45
13:00
15
30
45
14:00
15
30
45
15:00
15
30
45
16:00
15
30
45
17:00
15
30
45
San Gabriel
SPLASH OOPSLA
A Pure Demand Operational Semantics with Applications to Program Analysis
10:40 - 11:00
SPLASH OOPSLA
Automating Pruning in Top-Down Enumeration for Program Synthesis Proble ...
11:00 - 11:20
SPLASH OOPSLA
HOL4P4: mechanized small-step semantics for P4
11:20 - 11:40
SPLASH OOPSLA
Semantics Lifting for Syntactic Sugar
11:40 - 12:00
SPLASH OOPSLA
Synthesizing Formal Semantics from Executable Interpreters
12:00 - 12:20
SPLASH OOPSLA
Realistic Realizability: Specifying ABIs You Can Count On
13:40 - 14:00
SPLASH OOPSLA
AUTOMAP: Inferring Rank-Polymorphic Function Applications with Integer ...
14:00 - 14:20
SPLASH OOPSLA
Outcome Separation Logic: Local Reasoning for Correctness and Incorrect ...
14:20 - 14:40
SPLASH OOPSLA
VarLifter: Recovering Variables and Types from Bytecode of Solidity Sma ...
14:40 - 15:00
SPLASH OOPSLA
Weighted Context-Free-Language Ordered Binary Decision Diagrams
15:00 - 15:20
SPLASH OOPSLA
A Constraint Solving Approach to Parikh Images of Regular Languages
16:00 - 16:20
SPLASH OOPSLA
Imperative Compositional Programming: Type Sound Distributive Intersect ...
16:20 - 16:40
SPLASH OOPSLA
Inductive diagrams for causal reasoning
16:40 - 17:00
SPLASH OOPSLA
Message-Observing Sessions
17:00 - 17:20
SPLASH OOPSLA
Plume: Efficient and Complete Black-box Checking of Weak Isolation Levels
17:20 - 17:40
Thu 24 Oct
Displayed time zone:
Pacific Time (US & Canada)
change
Room
10:00
15
30
45
11:00
15
30
45
12:00
15
30
45
13:00
15
30
45
14:00
15
30
45
15:00
15
30
45
16:00
15
30
45
17:00
15
30
45
San Gabriel
SPLASH OOPSLA
Compilation of Shape Operators on Sparse Arrays
10:40 - 11:00
SPLASH OOPSLA
Compiler Support for Sparse Tensor Convolutions
11:00 - 11:20
SPLASH OOPSLA
Compiling Recurrences over Dense and Sparse Arrays
11:20 - 11:40
SPLASH OOPSLA
Fully Verified Instruction Scheduling
11:40 - 12:00
SPLASH OOPSLA
Homeostasis: Design and Implementation of a Self-Stabilizing Compiler ( ...
12:00 - 12:20
SPLASH OOPSLA
Hydra: Generalizing Peephole Optimizations with Program Synthesis
13:40 - 14:00
SPLASH OOPSLA
OOPSLA 2024 Distinguished Paper Award
Minotaur: A SIMD-Oriented Synthesizing Superoptimizer
14:00 - 14:20
SPLASH OOPSLA
PolyJuice: Detecting Mis-Compilation Bugs in Tensor Compilers with Equa ...
14:20 - 14:40
SPLASH OOPSLA
SparseAuto: An Auto-Scheduler for Sparse Tensor Computations Using Recu ...
14:40 - 15:00
SPLASH OOPSLA
Understanding and Finding Java Decompiler Bugs
15:00 - 15:20
SPLASH OOPSLA
Remote
A modal type-theory of expected cost in higher-order probabilistic programs
16:00 - 16:20
SPLASH OOPSLA
Distributions for Compositionally Differentiating Parametric Discontinu ...
16:20 - 16:40
SPLASH OOPSLA
Exact Bayesian Inference for Loopy Probabilistic Programs Using Generat ...
16:40 - 17:00
SPLASH OOPSLA
Hopping Proofs of Expectation-Based Properties: Applications to Skiplis ...
17:00 - 17:20
SPLASH OOPSLA
Learning Abstraction Selection for Bayesian Program Analysis
17:20 - 17:40
Fri 25 Oct
Displayed time zone:
Pacific Time (US & Canada)
change
Room
11:00
15
30
45
12:00
15
30
45
13:00
15
30
45
14:00
15
30
45
15:00
15
30
45
16:00
15
30
45
17:00
15
30
45
San Gabriel
SPLASH OOPSLA
A Dependent Nominal Physical Type System for Static Analysis of Memory ...
11:00 - 11:20
SPLASH OOPSLA
Modeling Dynamic (De)Allocations of Local Memory for Translation Validation
11:20 - 11:40
SPLASH OOPSLA
Mark--Scavenge: Waiting for Trash to Take Itself Out
11:40 - 12:00
SPLASH OOPSLA
Iris-MSWasm: elucidating and mechanising the security invariants of Mem ...
12:00 - 12:20
SPLASH OOPSLA
Automating Unrealizability Logic: Hoare-style Proof Synthesis for Infin ...
13:50 - 14:10
SPLASH OOPSLA
Compositionality and Observational Refinement for Linearizability with ...
14:10 - 14:30
SPLASH OOPSLA
Hypra: A Deductive Program Verifier for Hyper Hoare Logic
14:30 - 14:50
SPLASH OOPSLA
SMT2Test: From SMT Formulas to Effective Test Cases
14:50 - 15:10
SPLASH OOPSLA
Validating SMT Solvers for Correctness and Performance via Grammar-base ...
15:10 - 15:30
SPLASH OOPSLA
Making Sense of Multi-Threaded Application Performance at Scale with No ...
16:00 - 16:20
SPLASH OOPSLA
A Runtime System for Interruptible Query Processing -- When Incremental ...
16:20 - 16:40
SPLASH OOPSLA
PROMPT: A Fast and Extensible Memory Profiling Framework
16:40 - 17:00
SPLASH OOPSLA
Semantics of Remote Direct Memory Access: Operational and Declarative M ...
17:00 - 17:20
SPLASH OOPSLA
StarMalloc: Verifying a Modern, Hardened Memory Allocator
17:20 - 17:40
x
Thu 21 Nov 10:03