UNSOUND 2024
Sun 20 - Fri 25 October 2024 Pasadena, California, United States
co-located with SPLASH 2024
SPLASH 2024 (series) / UNSOUND 2024 (series) / Hilton Pasadena /

Room information: IBR West

VenueHilton Pasadena
Room nameIBR West
Room InformationNo extra information available
Program

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

Wed 23 Oct

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

10:40 - 12:20
Ownership, Security, and PrivacySPLASH OOPSLA at IBR West
Chair(s): Tobias Wrigstad Uppsala University
10:40
20m
Talk
Law and Order for Typestate with Borrowing
SPLASH OOPSLA
Hannes Saffrich University of Freiburg, Yuki Nishida Tohoku University, Peter Thiemann University of Freiburg, Germany
DOI
11:00
20m
Talk
Taypsi: Static Enforcement of Privacy Policies for Policy-Agnostic Oblivious Computation
SPLASH OOPSLA
Qianchuan Ye University at Buffalo, SUNY, Benjamin Delaware Purdue University
DOI
11:20
20m
Talk
Gradient: Gradual Compartmentalization via Object Capabilities Tracked in Types
SPLASH OOPSLA
Aleksander Boruch-Gruszecki Charles University, Adrien Ghosn Microsoft Research, Mathias Payer EPFL, Clément Pit-Claudel EPFL
DOI
11:40
20m
Talk
Automatically Reducing Privilege for Access Control Policies
SPLASH OOPSLA
Loris D'Antoni University of Wisconsin-Madison, Shuo Ding Georgia Institute of Technology, Amit Goel AWS, Mathangi Ramesh Amazon Web Services, Neha Rungta Amazon Web Services, Chungha Sung Amazon Web Services, USA
DOI
12:00
20m
Talk
Functional Ownership through Fractional Uniqueness
SPLASH OOPSLA
Danielle Marshall University of Glasgow; University of Kent, Dominic Orchard University of Kent; University of Cambridge
DOI
13:40 - 15:20
Performance Analysis and Optimisation 1SPLASH OOPSLA at IBR West
Chair(s): Manu Sridharan University of California at Riverside
13:40
20m
Talk
Accurate Data Race Prediction in the Linux Kernel through Sparse Fourier Learning
SPLASH OOPSLA
Gabriel Ryan Columbia University, Burcu Cetin Columbia University, Christian Yongwhan Lim Columbia University, Suman Jana Columbia University
DOI
14:00
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
DOI Media Attached
14:20
20m
Talk
Practical Verification Of Smart Contracts Using Memory Splitting
SPLASH OOPSLA
Shelly Grossman Tel Aviv University, Alexander Bakst Certora, Sameer Arora Certora Inc., John Toman Certora, inc., Chandrakana Nandi Certora, Mooly Sagiv Tel Aviv University
DOI
14:40
20m
Talk
Fast and Optimal Extraction for Sparse Equality GraphsOOPSLA 2024 Distinguished Paper Award
SPLASH OOPSLA
Amir Kafshdar Goharshady Hong Kong University of Science and Technology, Chun Kit Lam Hong Kong University of Science and Technology, Lionel Parreaux HKUST (The Hong Kong University of Science and Technology)
DOI
15:00
20m
Talk
HybridSA: GPU Acceleration of Multi-Pattern Regex Matching using Bit Parallelism
SPLASH OOPSLA
Alexis Le Glaunec Rice University, Lingkun Kong Rice University, Konstantinos Mamouras Rice University
DOI
16:00 - 17:40
Performance Analysis and Optimisation 2SPLASH OOPSLA at IBR West
Chair(s): Matthew Flatt University of Utah
16:00
20m
Talk
Jmvx: Fast Multi-threaded Multi-Version eXecution and Record-Replay for Managed Languages
SPLASH OOPSLA
David Schwartz University of Illinois at Chicago, Ankith Kowshik University of Illinois Chicago, Luís Pina University of Illinois at Chicago
DOI
16:20
20m
Talk
libLISA: Instruction Discovery and Analysis on x86-64
SPLASH OOPSLA
Jos Craaijo Open Universiteit, Freek Verbeek Open Universiteit & Virginia Tech, Binoy Ravindran Virginia Tech
DOI
16: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
DOI
17:00
20m
Talk
TorchQL: A Programming Framework for Integrity Constraints in Machine Learning
SPLASH OOPSLA
Aaditya Naik University of Pennsylvania, Adam Stein University of Pennsylvania, Yinjun Wu University of Pennsylvania, Mayur Naik University of Pennsylvania, Eric Wong
DOI
17:20
20m
Talk
Verification of Neural Networks' Global RobustnessRemote
SPLASH OOPSLA
Anan Kabaha Technion, Israel Institute of Technology, Dana Drachsler Cohen Technion
DOI

Thu 24 Oct

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

10:40 - 12:20
DatalogSPLASH OOPSLA at IBR West
Chair(s): John Regehr University of Utah
10:40
20m
Talk
A Typed Multi-Level Datalog IR and its Compiler Framework
SPLASH OOPSLA
David Klopp JGU Mainz, Sebastian Erdweg JGU Mainz, André Pacak JGU Mainz
DOI
11:00
20m
Talk
Finding Cross-rule Optimization Bugs in Datalog Engines
SPLASH OOPSLA
Chi Zhang Nanjing University, Linzhang Wang Nanjing University, Manuel Rigger National University of Singapore
DOI
11:20
20m
Talk
Making Formulog Fast: An Argument for Unconventional Datalog EvaluationOOPSLA 2024 Distinguished Artifact Award
SPLASH OOPSLA
Aaron Bembenek University of Melbourne, Michael Greenberg Stevens Institute of Technology, Stephen Chong Harvard University
DOI Pre-print
11:40
20m
Talk
Object-Oriented Fixpoint Programming with Datalog
SPLASH OOPSLA
David Klopp JGU Mainz, Sebastian Erdweg JGU Mainz, André Pacak JGU Mainz
DOI
12:00
20m
Talk
Scaling Abstraction Refinement for Program Analyses in Datalog Using Graph Neural Networks
SPLASH OOPSLA
Zhenyu Yan Peking University, Xin Zhang Peking University, Peng Di Ant Group
DOI
13:40 - 15:20
Program Synthesis and Verification 1SPLASH OOPSLA at IBR West
Chair(s): Benjamin Delaware Purdue University
13:40
20m
Talk
Control-Flow Deobfuscation using Trace-Informed Compositional Program Synthesis
SPLASH OOPSLA
Benjamin Mariano University of Texas at Austin, Ziteng Wang University of Texas at Austin, Shankara Pailoor University of Texas at Austin, Christian Collberg University of Arizona, Işıl Dillig University of Texas at Austin
DOI
14:00
20m
Talk
Finding ∀∃ Hyperbugs Using Symbolic Execution
SPLASH OOPSLA
Arthur Correnson CISPA Helmholtz Center for Information Security, Tobias Nießen TU Wien, Bernd Finkbeiner CISPA Helmholtz Center for Information Security, Georg Weissenbacher TU Wien
DOI
14:20
20m
Talk
Mechanizing the CMP Abstraction for Parameterized Verification
SPLASH OOPSLA
Yongjian Li Key Laboratory of System Software (Chinese Academy of Sciences) and State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, China, Bohua Zhan Institute of Software, Chinese Academy of Sciences, Jun Pang University of Luxembourg
DOI
14:40
20m
Talk
Model Checking Distributed Protocols in Must
SPLASH OOPSLA
Constantin Enea LIX, CNRS, Ecole Polytechnique, Dimitra Giannakopoulou Amazon Web Services, Michalis Kokologiannakis ETH Zurich, Rupak Majumdar MPI-SWS
DOI
15:00
20m
Talk
Monotone Procedure Summarization via Vector Addition Systems and Inductive Potentials
SPLASH OOPSLA
Nikhil Pimpalkhare Princeton University, Zachary Kincaid Princeton University
DOI
16:00 - 17:40
Types and Gradual Typing 1SPLASH OOPSLA at IBR West
Chair(s): Fabian Muehlboeck Australian National University
16:00
20m
Talk
Intensional Functions
SPLASH OOPSLA
Zachary Palmer Swarthmore College, Nathaniel Wesley Filardo Microsoft, Ke Wu Johns Hopkins University
DOI
16:20
20m
Talk
Qualifying System F-sub
SPLASH OOPSLA
Edward Lee University of Waterloo, Yaoyu Zhao University of Waterloo, Ondřej Lhoták University of Waterloo, James You University of Waterloo, Kavin Satheeskumar University of Waterloo, Jonathan Immanuel Brachthäuser University of Tübingen
DOI
16:40
20m
Talk
Refinement Type Refutations
SPLASH OOPSLA
Robin Webbers Vrije Universiteit Amsterdam, Klaus von Gleissenthall Vrije Universiteit Amsterdam, Ranjit Jhala UCSD
DOI
17:00
20m
Talk
Type Inference Logics
SPLASH OOPSLA
Denis Carnier KU Leuven, François Pottier Inria, Steven Keuchel Vrije Universiteit Brussel
DOI
17:20
20m
Talk
Polymorphic Reachability Types: Tracking Freshness, Aliasing, and Separation in Higher-Order Generic Programs (SIGPLAN)
SPLASH OOPSLA
Guannan Wei Inria/ENS; Tufts University, Oliver Bračevac EPFL, LAMP, Songlin Jia Purdue University, USA, Yuyan Bao Augusta University, Tiark Rompf Purdue University
Link to publication

Fri 25 Oct

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

11:00 - 12:20
Static Analysis and Program Verification 4SPLASH OOPSLA at IBR West
Chair(s): Anders Møller Aarhus University
11:00
20m
Talk
A Learning-Based Approach to Static Program Slicing
SPLASH OOPSLA
Aashish Yadavally University of Texas at Dallas, Yi Li University of Texas at Dallas, Shaohua Wang Central University of Finance and Economics, Tien N. Nguyen University of Texas at Dallas
DOI Pre-print
11:20
20m
Talk
Boosting the Performance of Alias-Aware IFDS Analysis with CFL-based Environment Transformers
SPLASH OOPSLA
Haofeng Li Institute of Computing Technology at Chinese Academy of Sciences, Chenghang Shi SKLP, Institute of Computing Technology, CAS, Jie Lu SKLP, Institute of Computing Technology, CAS, Lian Li Institute of Computing Technology at Chinese Academy of Sciences; University of Chinese Academy of Sciences, Jingling Xue UNSW Sydney
DOI
11:40
20m
Talk
The ART of Sharing Points-to Analysis: Reusing Points-to Analysis Results Safely and Efficiently
SPLASH OOPSLA
Shashin Halalingaiah UT Austin, IIT Madras, Vijay Sundaresan IBM Canada, Daryl Maier IBM Canada, V Krishna Nandivada IIT Madras
DOI
12:00
20m
Talk
UniSparse: An Intermediate Language for General Sparse Format Customization
SPLASH OOPSLA
Jie Liu Cornell University, Zhongyuan Zhao Qualcomm, Zijian Ding UCLA, Benjamin Brock Parallel Computing Lab (PCL), Intel, Hongbo Rong Intel Labs, Zhiru Zhang Cornell University, USA
DOI
13:50 - 15:30
Novel Programming Concepts and ParadigmsSPLASH OOPSLA at IBR West
Chair(s): Tobias Wrigstad Uppsala University
13:50
20m
Talk
A Case for First-Class Environments
SPLASH OOPSLA
Jinhao Tan University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong
DOI
14:10
20m
Talk
Deriving Dependently-Typed OOP from First PrinciplesOOPSLA 2024 Distinguished Artifact Award
SPLASH OOPSLA
David Binder University of Tübingen, Ingo Skupin University of Tübingen, Tim Süberkrüb Aleph Alpha, Klaus Ostermann University of Tübingen
DOI
14:30
20m
Talk
Multiverse Notebook: Shifting Data Scientists to Time Travelers
SPLASH OOPSLA
Shigeyuki Sato The University of Electro-Communications, Tomoki Nakamaru The University of Tokyo
DOI
14:50
20m
Talk
The Ultimate Conditional SyntaxOOPSLA 2024 Distinguished Paper Award
SPLASH OOPSLA
Luyu Cheng Hong Kong University of Science and Technology, Lionel Parreaux HKUST (The Hong Kong University of Science and Technology)
DOI
15:10
20m
Talk
Unifying Static and Dynamic Intermediate Languages for Accelerator Generators
SPLASH OOPSLA
Caleb Kim Massachusetts Institute of Technology (MIT), Pai Li Cornell University, USA, Anshuman Mohan Cornell University, Andrew Butt Cornell University, Adrian Sampson Cornell University, Rachit Nigam Massachusetts Institute of Technology
DOI
16:00 - 17:40
Education and Language UsabilitySPLASH OOPSLA at IBR West
Chair(s): Arjun Guha Northeastern University; Roblox
16:00
20m
Talk
Forge: A Tool and Language for Teaching Formal Methods
SPLASH OOPSLA
Tim Nelson Brown University, Ben Greenman University of Utah, Siddhartha Prasad Brown University, Tristan Dyer Brown University, Ethan Bove Brown University, Qianfan Chen Brown University, Charlie Cutting Brown University, Thomas Del Vecchio Brown University, Sidney LeVine Brown University, Julianne Rudner Brown University, Benjamin Ryjikov Brown University, Alexander Varga Brown University, Andrew Wagner Northeastern University, Luke West Brown University, Shriram Krishnamurthi Brown University
DOI
16:20
20m
Talk
HiPy: Extracting High-Level Semantics From Python Code For Data Processing
SPLASH OOPSLA
Michael Jungmair Technical University of Munich, Alexis Engelke TU Munich, Jana Giceva Technical University of Munich
DOI
16:40
20m
Talk
Identifying and Correcting Programming Language Behavior MisconceptionsOOPSLA 2024 Distinguished Paper Award
SPLASH OOPSLA
Kuang-Chen Lu Brown University, USA, Shriram Krishnamurthi Brown University
DOI
17:00
20m
Talk
PyDex: Repairing Bugs in Introductory Python Assignments using LLMs
SPLASH OOPSLA
Jialu Zhang University of Waterloo, José Pablo Cambronero Google, USA, Sumit Gulwani Microsoft, Vu Le Microsoft, Ruzica Piskac Yale University, Gustavo Soares Microsoft, Gust Verbruggen Microsoft
DOI
17:20
20m
Talk
Profiling Programming Language LearningOOPSLA 2024 Distinguished Paper Award
SPLASH OOPSLA
Will Crichton Brown University, Shriram Krishnamurthi Brown University
DOI Pre-print

Wed 23 Oct

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

Room10:003011:003012:003013:003014:003015:003016:003017:0030
IBR West

SPLASH OOPSLA

Ownership, Security, and Privacy

SPLASH OOPSLA

Performance Analysis and Optimisation 1

SPLASH OOPSLA

Performance Analysis and Optimisation 2

Thu 24 Oct

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

Room10:003011:003012:003013:003014:003015:003016:003017:0030
IBR West

SPLASH OOPSLA

Datalog

SPLASH OOPSLA

Program Synthesis and Verification 1

SPLASH OOPSLA

Types and Gradual Typing 1

Fri 25 Oct

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

Room11:003012:003013:003014:003015:003016:003017:0030
IBR West

SPLASH OOPSLA

Static Analysis and Program Verification 4

SPLASH OOPSLA

Novel Programming Concepts and Paradigms

SPLASH OOPSLA

Education and Language Usability

Wed 23 Oct

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

Room10:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:00153045
IBR West
SPLASH OOPSLA
Law and Order for Typestate with Borrowing
10:40 - 11:00
SPLASH OOPSLA
Taypsi: Static Enforcement of Privacy Policies for Policy-Agnostic Obli ...
11:00 - 11:20
SPLASH OOPSLA
Gradient: Gradual Compartmentalization via Object Capabilities Tracked ...
11:20 - 11:40
SPLASH OOPSLA
Automatically Reducing Privilege for Access Control Policies
11:40 - 12:00
SPLASH OOPSLA
Functional Ownership through Fractional Uniqueness
12:00 - 12:20
SPLASH OOPSLA
Accurate Data Race Prediction in the Linux Kernel through Sparse Fourie ...
13:40 - 14:00
SPLASH OOPSLA
Mix Testing: Specifying and Testing ABI Compatibility of C/C++ Atomics ...
14:00 - 14:20
SPLASH OOPSLA
Practical Verification Of Smart Contracts Using Memory Splitting
14:20 - 14:40
SPLASH OOPSLAOOPSLA 2024 Distinguished Paper Award
Fast and Optimal Extraction for Sparse Equality Graphs
14:40 - 15:00
SPLASH OOPSLA
HybridSA: GPU Acceleration of Multi-Pattern Regex Matching using Bit Pa ...
15:00 - 15:20
SPLASH OOPSLA
Jmvx: Fast Multi-threaded Multi-Version eXecution and Record-Replay for ...
16:00 - 16:20
SPLASH OOPSLA
libLISA: Instruction Discovery and Analysis on x86-64
16:20 - 16:40
SPLASH OOPSLA
Extending the C/C++ Memory Model with Inline Assembly
16:40 - 17:00
SPLASH OOPSLA
TorchQL: A Programming Framework for Integrity Constraints in Machine L ...
17:00 - 17:20
SPLASH OOPSLARemote
Verification of Neural Networks' Global Robustness
17:20 - 17:40

Thu 24 Oct

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

Room10:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:00153045
IBR West
SPLASH OOPSLA
A Typed Multi-Level Datalog IR and its Compiler Framework
10:40 - 11:00
SPLASH OOPSLA
Finding Cross-rule Optimization Bugs in Datalog Engines
11:00 - 11:20
SPLASH OOPSLAOOPSLA 2024 Distinguished Artifact Award
Making Formulog Fast: An Argument for Unconventional Datalog Evaluation
11:20 - 11:40
SPLASH OOPSLA
Object-Oriented Fixpoint Programming with Datalog
11:40 - 12:00
SPLASH OOPSLA
Scaling Abstraction Refinement for Program Analyses in Datalog Using Gr ...
12:00 - 12:20
SPLASH OOPSLA
Control-Flow Deobfuscation using Trace-Informed Compositional Program S ...
13:40 - 14:00
SPLASH OOPSLA
Finding ∀∃ Hyperbugs Using Symbolic Execution
14:00 - 14:20
SPLASH OOPSLA
Mechanizing the CMP Abstraction for Parameterized Verification
14:20 - 14:40
SPLASH OOPSLA
Model Checking Distributed Protocols in Must
14:40 - 15:00
SPLASH OOPSLA
Monotone Procedure Summarization via Vector Addition Systems and Induct ...
15:00 - 15:20
SPLASH OOPSLA
Intensional Functions
16:00 - 16:20
SPLASH OOPSLA
Qualifying System F-sub
16:20 - 16:40
SPLASH OOPSLA
Refinement Type Refutations
16:40 - 17:00
SPLASH OOPSLA
Type Inference Logics
17:00 - 17:20
SPLASH OOPSLA
Polymorphic Reachability Types: Tracking Freshness, Aliasing, and Separ ...
17:20 - 17:40

Fri 25 Oct

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

Room11:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:00153045
IBR West
SPLASH OOPSLA
A Learning-Based Approach to Static Program Slicing
11:00 - 11:20
SPLASH OOPSLA
Boosting the Performance of Alias-Aware IFDS Analysis with CFL-based En ...
11:20 - 11:40
SPLASH OOPSLA
The ART of Sharing Points-to Analysis: Reusing Points-to Analysis Resul ...
11:40 - 12:00
SPLASH OOPSLA
UniSparse: An Intermediate Language for General Sparse Format Customization
12:00 - 12:20
SPLASH OOPSLA
A Case for First-Class Environments
13:50 - 14:10
SPLASH OOPSLAOOPSLA 2024 Distinguished Artifact Award
Deriving Dependently-Typed OOP from First Principles
14:10 - 14:30
SPLASH OOPSLA
Multiverse Notebook: Shifting Data Scientists to Time Travelers
14:30 - 14:50
SPLASH OOPSLAOOPSLA 2024 Distinguished Paper Award
The Ultimate Conditional Syntax
14:50 - 15:10
SPLASH OOPSLA
Unifying Static and Dynamic Intermediate Languages for Accelerator Gene ...
15:10 - 15:30
SPLASH OOPSLA
Forge: A Tool and Language for Teaching Formal Methods
16:00 - 16:20
SPLASH OOPSLA
HiPy: Extracting High-Level Semantics From Python Code For Data Processing
16:20 - 16:40
SPLASH OOPSLAOOPSLA 2024 Distinguished Paper Award
Identifying and Correcting Programming Language Behavior Misconceptions
16:40 - 17:00
SPLASH OOPSLA
PyDex: Repairing Bugs in Introductory Python Assignments using LLMs
17:00 - 17:20
SPLASH OOPSLAOOPSLA 2024 Distinguished Paper Award
Profiling Programming Language Learning
17:20 - 17:40