San Gabriel - UNSOUND 2024

VenueHilton Pasadena

Room nameSan Gabriel

Room InformationNo extra information available

Program

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

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 programSpecify 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 AnalysisSAS 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 partitioningSAS 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 networksSAS 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 networksSAS 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 responsibilitySAS 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 analysisSAS 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 analysisSAS 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 MeetingSAS 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 AnalysisSAS 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 flawsSAS 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 analysisSAS 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	SemanticsSPLASH OOPSLA 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 SPLASH OOPSLA 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 SPLASH OOPSLA 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 SPLASH OOPSLA 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 SPLASH OOPSLA 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 SPLASH OOPSLA 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 1SPLASH OOPSLA at San Gabriel Chair(s): Benjamin Delaware Purdue University

13:40 20m Talk		Realistic Realizability: Specifying ABIs You Can Count On SPLASH OOPSLA 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 SPLASH OOPSLA 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 SPLASH OOPSLA 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 SPLASH OOPSLA 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 SPLASH OOPSLA 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 2SPLASH OOPSLA 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 SPLASH OOPSLA 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 SPLASH OOPSLA 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 SPLASH OOPSLA 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 SPLASH OOPSLA 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 SPLASH OOPSLA 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 1SPLASH OOPSLA at San Gabriel Chair(s): Emery D. Berger University of Massachusetts Amherst

10:40 20m Talk		Compilation of Shape Operators on Sparse Arrays SPLASH OOPSLA 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 SPLASH OOPSLA 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 SPLASH OOPSLA Shiv Sundram Stanford University, Muhammad Usman Tariq Stanford University, Fredrik Kjolstad Stanford University DOI
11:40 20m Talk		Fully Verified Instruction Scheduling SPLASH OOPSLA 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) SPLASH OOPSLA Aman Nougrahiya IIT Madras, V Krishna Nandivada IIT Madras Link to publication

13:40 - 15:20	Compilers and Optimisation 2SPLASH OOPSLA at San Gabriel Chair(s): Manu Sridharan University of California at Riverside

13:40 20m Talk		Hydra: Generalizing Peephole Optimizations with Program Synthesis SPLASH OOPSLA Manasij Mukherjee NVIDIA, John Regehr University of Utah DOI Pre-print
14:00 20m Talk		Minotaur: A SIMD-Oriented Synthesizing SuperoptimizerOOPSLA 2024 Distinguished Paper Award SPLASH OOPSLA 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 SPLASH OOPSLA 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 SPLASH OOPSLA 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 SPLASH OOPSLA 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 1SPLASH OOPSLA at San Gabriel Chair(s): Di Wang Peking University

16:00 20m Talk		A modal type-theory of expected cost in higher-order probabilistic programsRemote SPLASH OOPSLA 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 SPLASH OOPSLA 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 SPLASH OOPSLA 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 SPLASH OOPSLA 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 SPLASH OOPSLA 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 1SPLASH OOPSLA 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 SPLASH OOPSLA 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 SPLASH OOPSLA 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 SPLASH OOPSLA 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 SPLASH OOPSLA 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 2SPLASH OOPSLA 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 SPLASH OOPSLA 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 SPLASH OOPSLA 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 SPLASH OOPSLA 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 SPLASH OOPSLA Chengyu Zhang ETH Zurich, Zhendong Su ETH Zurich DOI
15:10 20m Talk		Validating SMT Solvers for Correctness and Performance via Grammar-based Enumeration SPLASH OOPSLA Dominik Winterer ETH Zurich, Zhendong Su ETH Zurich DOI

16:00 - 17:40	Memory Management and Analysis 2SPLASH OOPSLA 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 SPLASH OOPSLA 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 SPLASH OOPSLA 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 SPLASH OOPSLA 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 SPLASH OOPSLA 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 SPLASH OOPSLA 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									SPLASH OOPSLA Semantics																																				SPLASH OOPSLA Formal Methods 1																												SPLASH OOPSLA 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									SPLASH OOPSLA Compilers and Optimisation 1																																				SPLASH OOPSLA Compilers and Optimisation 2																												SPLASH OOPSLA 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	SPLASH OOPSLA Memory Management and Analysis 1																																		SPLASH OOPSLA Program Synthesis and Verification 2																										SPLASH OOPSLA 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 OOPSLAOOPSLA 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 OOPSLARemote 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

Room information: San Gabriel

Program Display Configuration

Sun 20 OctDisplayed time zone: Pacific Time (US & Canada) change

Mon 21 OctDisplayed time zone: Pacific Time (US & Canada) change

Tue 22 OctDisplayed time zone: Pacific Time (US & Canada) change

Wed 23 OctDisplayed time zone: Pacific Time (US & Canada) change

Thu 24 OctDisplayed time zone: Pacific Time (US & Canada) change

Fri 25 OctDisplayed time zone: Pacific Time (US & Canada) change

Sun 20 OctDisplayed time zone: Pacific Time (US & Canada) change

SAS

SAS

SAS

SAS

Mon 21 OctDisplayed time zone: Pacific Time (US & Canada) change

SAS

SAS

SAS

SAS

Tue 22 OctDisplayed time zone: Pacific Time (US & Canada) change

SAS

SAS

SAS

SAS

Wed 23 OctDisplayed time zone: Pacific Time (US & Canada) change

SPLASH OOPSLA

SPLASH OOPSLA

SPLASH OOPSLA

Thu 24 OctDisplayed time zone: Pacific Time (US & Canada) change

SPLASH OOPSLA

SPLASH OOPSLA

SPLASH OOPSLA

Fri 25 OctDisplayed time zone: Pacific Time (US & Canada) change

SPLASH OOPSLA

SPLASH OOPSLA

SPLASH OOPSLA

Sun 20 OctDisplayed time zone: Pacific Time (US & Canada) change

Mon 21 OctDisplayed time zone: Pacific Time (US & Canada) change

Tue 22 OctDisplayed time zone: Pacific Time (US & Canada) change

Wed 23 OctDisplayed time zone: Pacific Time (US & Canada) change

Thu 24 OctDisplayed time zone: Pacific Time (US & Canada) change

Fri 25 OctDisplayed time zone: Pacific Time (US & Canada) change

Sun 20 Oct
Displayed time zone: Pacific Time (US & Canada) change

Mon 21 Oct
Displayed time zone: Pacific Time (US & Canada) change

Tue 22 Oct
Displayed time zone: Pacific Time (US & Canada) change

Wed 23 Oct
Displayed time zone: Pacific Time (US & Canada) change

Thu 24 Oct
Displayed time zone: Pacific Time (US & Canada) change

Fri 25 Oct
Displayed time zone: Pacific Time (US & Canada) change

Sun 20 Oct
Displayed time zone: Pacific Time (US & Canada) change

Mon 21 Oct
Displayed time zone: Pacific Time (US & Canada) change

Tue 22 Oct
Displayed time zone: Pacific Time (US & Canada) change

Wed 23 Oct
Displayed time zone: Pacific Time (US & Canada) change

Thu 24 Oct
Displayed time zone: Pacific Time (US & Canada) change

Fri 25 Oct
Displayed time zone: Pacific Time (US & Canada) change

Sun 20 Oct
Displayed time zone: Pacific Time (US & Canada) change

Mon 21 Oct
Displayed time zone: Pacific Time (US & Canada) change

Tue 22 Oct
Displayed time zone: Pacific Time (US & Canada) change

Wed 23 Oct
Displayed time zone: Pacific Time (US & Canada) change

Thu 24 Oct
Displayed time zone: Pacific Time (US & Canada) change

Fri 25 Oct
Displayed time zone: Pacific Time (US & Canada) change