San Gabriel - VMIL 2024

VenueHilton Pasadena

Room nameSan Gabriel

Room InformationNo extra information available

Program

This program is tentative and subject to change.

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	Memory AnalysisSAS at San Gabriel

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

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

14:00 - 15:30	Machine learning and Neural networksSAS at San Gabriel

14:00 60m Tutorial		Abstract Interpretation-Based Certification of Hyperproperties for High-Stakes Machine Learning Software SAS Caterina Urban Inria & École Normale Supérieure \| Université PSL
15:00 30m Full-paper		Robustness Verification of Multi-Label Neural Network Classifiers SAS Julian Mour , Dana Drachsler Cohen Technion

16:00 - 17:30	Machine Learning and Neural networksSAS at San Gabriel

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
16:30 30m Short-paper		ConstraintFlow: A DSL for Specification and Verification of Neural Network Analyses (NEAT paper) SAS Avaljot Singh , Yasmin Sarita Cornell University, Charith Mendis University of Illinois at Urbana-Champaign, Gagandeep Singh University of Illinois at Urbana-Champaign; VMware Research

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

09:00 - 10:30	Quantitative analysisSAS at San Gabriel

09:00 60m Keynote		Measuring data lineage SAS Francesco Logozzo Facebook
10: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 \| Université PSL

11:00 - 12:30	Verification cost and quantum analysisSAS at San Gabriel

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
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
12:00 30m Full-paper		Static Analysis of Quantum Programs SAS Nicola Assolini Università degli Studi di Verona, Alessandra Di Pierro University of Verona, Italy, Isabella Mastroeni University of Verona, Italy

14:00 - 15:30	Authorisation and responsibilitySAS at San Gabriel

14:00 60m Tutorial		A New Language for Expressive, Fast, Safe, and Analyzable Authorization SAS Emina Torlak Amazon Web Services, USA
15:00 30m Full-paper		On the Role of Cognizance in Responsibility SAS Laura Canaia , Mila Dalla Preda University of Verona

16:00 - 17:30	SAS24 Business MeetingSAS at San Gabriel

16:00 60m Meeting		Business Meeting SAS

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

09:00 - 10:30	Automatising Program AnalysisSAS at San Gabriel

09:00 60m Keynote		TBA 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

11:00 - 12:30	System level analysisSAS at San Gabriel

11:00 30m Full-paper		Lift-offline: Instruction Lifter Generators SAS Nicholas Coughlin Defence Science and Technology Group, Australia, Alistair Michael , Kait Lam
11:30 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
12: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

14:00 - 15:30	System level analysisSAS at San Gabriel

14:00 30m Full-paper		GoGuard: Efficient Static Blocking Bug Detection for Go SAS Bozhen Liu Texas A&M University, USA, Dhruti Joshi
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

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

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
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
14:20 20m Talk		Quantitative Weakest Hyper Pre: Unifying Correctness and Incorrectness Hyperproperties via Predicate Transformers SPLASH OOPSLA Linpeng Zhang University College London, Noam Zilberstein Cornell University, Benjamin Lucien Kaminski Saarland University; University College London, Alexandra Silva Cornell University
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
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

16:00 - 17:40	Formal Methods 2SPLASH OOPSLA at San Gabriel

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
16:20 20m Talk		Imperative Compositional Programming SPLASH OOPSLA Wenjia Ye University of Hong Kong, Yaozhu Sun University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong
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 Pre-print
17:00 20m Talk		Message-Observing Sessions SPLASH OOPSLA Ryan Kavanagh Université du Québec à Montréal (UQAM), Brigitte Pientka McGill University
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

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

10:40 - 12:20	Compilers and Optimisation 1SPLASH OOPSLA at San Gabriel

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

13:40 20m Talk		Hydra: Generalizing Peephole Optimizations with Program Synthesis SPLASH OOPSLA Manasij Mukherjee University of Utah, John Regehr University of Utah Pre-print
14:00 20m Talk		Minotaur: A SIMD-Oriented Synthesizing Superoptimizer SPLASH OOPSLA Zhengyang Liu University of Utah, Stefan Mada University of Utah, John Regehr University of Utah
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
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 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

16:00 - 17:40	Probabilistic Programming and Analysis 1SPLASH OOPSLA at San Gabriel

16:00 20m Talk		A modal type-theory of expected cost in higher-order probabilistic programs SPLASH OOPSLA Vineet Rajani University of Kent, Gilles Barthe MPI-SP; IMDEA Software Institute, Deepak Garg MPI-SWS
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
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
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é
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

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
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
11:40 20m Talk		Extending the C/C++ Memory Model with Inline Assembly SPLASH OOPSLA Paulo Emílio de Vilhena Imperial College London, Ori Lahav Tel Aviv University, Viktor Vafeiadis MPI-SWS, Azalea Raad Imperial College London
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

13:50 - 15:30	Program Synthesis and Verification 2SPLASH OOPSLA at San Gabriel

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
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
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
14:50 20m Talk		SMT2Test: From SMT Formulas to Effective Test Cases SPLASH OOPSLA Chengyu Zhang ETH Zurich, Zhendong Su ETH Zurich
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

16:00 - 17:40	Memory Management and Analysis 2SPLASH OOPSLA at San Gabriel

16:00 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
16:20 20m Talk		Mix Testing: Specifying and Testing ABI Compatibility of C/C++ Atomics Implementations SPLASH OOPSLA Luke Geeson University College London, James Brotherston , Wilco Dijkstra Arm Ltd, Alastair F. Donaldson Imperial College London, Lee Smith Arm, Tyler Sorensen University of California at Santa Cruz, John Wickerson Imperial College London
16:40 20m Talk		PROMPT: A Fast and Extensible Memory Profiling Framework SPLASH OOPSLA Ziyang Xu Princeton University, 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
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
17:20 20m Talk		StarMalloc: Verifying a Modern, Hardened Memory Allocator SPLASH OOPSLA Antonin Reitz Inria, Aymeric Fromherz Inria, Jonathan Protzenko Microsoft Azure Research

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 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 Quantitative analysis																								SAS Verification cost and quantum analysis																																				SAS Authorisation and responsibility																								SAS 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 System level analysis																																				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 Measuring data lineage 09:00 - 10:00												SAS Quantitative Static Timing Analysis 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 Static Analysis of Quantum Programs 12:00 - 12:30																								SAS A New Language for Expressive, Fast, Safe, and Analyzable Authorization 14:00 - 15:00												SAS On the Role of Cognizance in Responsibility 15:00 - 15:30												SAS 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 TBA 09:00 - 10:00												SAS Synthesizing Abstract Transformers for Reduced-Product Domains 10:00 - 10:30												SAS Lift-offline: Instruction Lifter Generators 11:00 - 11:30						SAS Fixing Latent Unsound Abstract Operators in the eBPF Verifier of the Li ... 11:30 - 12:00						SAS Verifying components of Arm® Confidential Computing Architecture with E ... 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 Quantitative Weakest Hyper Pre: Unifying Correctness and Incorrectness ... 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 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 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 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 Extending the C/C++ Memory Model with Inline Assembly 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 Mark--Scavenge: Waiting for Trash to Take Itself Out 16:00 - 16:20				SPLASH OOPSLA Mix Testing: Specifying and Testing ABI Compatibility of C/C++ Atomics ... 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

This program is tentative and subject to change.

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