Orchid East - SPLASH 2025

VenueMarina Bay Sands Convention Centre

Room nameOrchid East

Floor4

Room number4202-4203

Capacity180

Room Information

Venue floor plan

app-screen

Program

This program is tentative and subject to change.

Time Zone

The program is currently displayed in (GMT+08:00) Perth.

Use conference time zone: (GMT+08:00) PerthSelect 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

Mon 13 Oct
Displayed time zone: Perth change

10:50 - 12:05	Opening and KeynoteSAS at Orchid East

10:50 10m Day opening		Opening SAS
11:05 60m Keynote		On a simple problem due to Yves Bertot SAS Olivier Danvy Yale-NUS College and School of Computing, Singapore

13:40 - 15:20	VerificationSAS at Orchid East

13:40 60m Keynote		Multi-Modal Verification of Distributed Systems in Lean SAS Ilya Sergey National University of Singapore
14:40 20m Talk		Verifying Neural Networks with PyRAT SAS Tristan Le Gall CEA LIST, Augustin Lemesle CEA, LIST, France, Julien Lehmann CEA, LIST, France, Zakaria Chihani CEA, LIST, France
15:00 20m Talk		Enhancing Neural Network Robustness via Synthesis of Repair Programs SAS Tom Yuviler Technion, Dana Drachsler Cohen Technion

16:00 - 17:40	Abstraction and ProofsSAS at Orchid East Chair(s): Xavier Rival Inria; ENS; CNRS; PSL University

16:00 20m Talk		Relating Distances and Abstractions: An Abstract Interpretation Perspective SAS Marco Campion INRIA & ENS Paris \| Université PSL, Isabella Mastroeni University of Verona, Caterina Urban Inria & ENS \| PSL
16:20 20m Talk		Precise Abstract Interpretation of Probabilistic Programs with Interval Data Uncertainty SAS Zixin Huang University of Illinois at Urbana-Champaign, USA, Jacob Laurel Georgia Institute of Technology, Saikat Dutta University of Illinois at Urbana-Champaign, Sasa Misailovic University of Illinois at Urbana-Champaign
16:40 20m Talk		Specifying and Verifying Future Conditions SAS Yahui Song Standard Chartered Bank, Darius Foo National University of Singapore, Wei-Ngan Chin National University of Singapore
17:00 20m Talk		Contextual Equality Saturation SAS Alexandre Drewery INRIA, Thomas P. Jensen INRIA Rennes, David Pichardie Meta
17:20 20m Talk		Abstracting Concolic Execution for Soft Contract Verification SAS Bram Vandenbogaerde , Quentin Stiévenart Université du Québec à Montréal, Coen De Roover Vrije Universiteit Brussel

Tue 14 Oct
Displayed time zone: Perth change

10:50 - 12:05	CompilerSAS at Orchid East

10:50 55m Keynote		From Within: Compiler Testing and Validation via Compilers SAS Qirun Zhang Georgia Institute of Technology
11:45 20m Talk		Ductape: Optimizing Dynamically Typed Programs using Ahead-of-Time Compilation and Data-Flow Analysis SAS Adi Harif , Shachar Itzhaky Technion

13:40 - 15:20	Abstract InterpretationSAS at Orchid East

13:40 60m Keynote		Towards static analyses and abstract domains for hyperproperties SAS Xavier Rival Inria; ENS; CNRS; PSL University
14:40 20m Talk		Comparing the Precision of Abstract Operators in the eBPF Verifier using Differential Synthesis SAS Matan Shachnai , Harishankar Vishwanathan , Srinivas Narayana Rutgers University, Santosh Nagarakatte Rutgers University
15:00 20m Talk		A Programming Language for Feasible Solutions SAS Weijun Chen Shanghai Jiao Tong University, China, Yuxi Fu Shanghai Jiao Tong University, China, Huan Long Shanghai Jiao Tong University

16:00 - 17:40	Testing and Constraint SolvingSAS at Orchid East

16:00 20m Talk		Bounded-Exhaustive Subspace Diversification for SMT Solver Testing SAS Junda Zheng , Peisen Yao Zhejiang University
16:20 20m Talk		Monarch: A Modular Framework for Abstract Definitional Interpreters in Haskell SAS Bram Vandenbogaerde , Sarah Verbelen Vrije Universiteit Brussel, Belgium, Noah Van Es Sofware Languages Lab, Vrije Universiteit Brussel, Coen De Roover Vrije Universiteit Brussel
16:40 20m Talk		Delta Store Semantics: Abstract Garbage Collection for Abstract Definitional Interpreters SAS Noah Van Es Sofware Languages Lab, Vrije Universiteit Brussel, Bram Vandenbogaerde , Coen De Roover Vrije Universiteit Brussel
17:00 20m Talk		Automated Catamorphism Synthesis for Solving Constrained Horn Clauses over Algebraic Data Types SAS Hiroyuki Katsura , Naoki Kobayashi University of Tokyo, Ken Sakayori University of Tokyo, Ryosuke Sato Tokyo University of Agriculture and Technology
17:20 20m Talk		Formal Analysis of Networked PLC Controllers Interacting with Physical Environments SAS Jaeseo Lee POSTECH, Kyungmin Bae POSTECH

Wed 15 Oct
Displayed time zone: Perth change

10:50 - 12:05	KeynoteLMPL at Orchid East

10:50 75m Keynote		AI Safety through Programming? LMPL Jun Sun Singapore Management University

13:40 - 15:20	LLMs for Program Analysis and Verification ILMPL at Orchid East

13:40 15m Talk		Function Renaming in Reverse Engineering of Embedded Device Firmware with ChatGPT LMPL Puzhuo Liu Ant Group & Tsinghua University, Peng Di Ant Group & UNSW Sydney, Yu Jiang Tsinghua University
13:55 15m Talk		Enhancing Semantic Understanding in Pointer Analysis Using Large Language Models LMPL Baijun Cheng Peking University, Kailong Wang Huazhong University of Science and Technology, Ling Shi Nanyang Technological University, Haoyu Wang Huazhong University of Science and Technology, Yao Guo Peking University, Ding Li Peking University, Xiangqun Chen Peking University
14:10 15m Talk		Improving SAST Detection Capability with LLMs and Enhanced DFA LMPL Yuan Luo Tencent Security Yunding Lab, Zhaojun Chen Tencent Security Yunding Lab, Yuxin Dong Peking University, Haiquan Zhang Tencent Security Yunding Lab, Yi Sun Tencent Security Yunding Lab, Fei Xie Tencent Security Yunding Lab, Zhiqiang Dong Tencent Security Yunding Lab
14:25 15m Talk		ClearAgent: Agentic Binary Analysis for Effective Vulnerability Detection LMPL Xiang Chen The Hong Kong University of Science and Technology, Anshunkang Zhou The Hong Kong University of Science and Technology, Chengfeng Ye The Hong Kong University of Science and Technology, Charles Zhang The Hong Kong University of Science and Technology
14:40 15m Talk		CG-Bench: Can Language Models Assist Call Graph Construction in the Real World? LMPL Ting Yuan , Wenrui Zhang Huawei Technologies Co., Ltd, Dong Chen Huawei, Jie Wang Huawei Technologies Co., Ltd Pre-print
14:55 20m Talk		Beyond Static Pattern Matching? Rethinking Automatic Cryptographic API Misuse Detection in the Era of LLMs LMPL Yifan Xia

16:00 - 17:40	LLMs for Program Analysis and Verification IILMPL at Orchid East

16:00 15m Talk		Hallucination-Resilient LLM-Driven Sound and Tunable Static Analysis LMPL Guannan Wei Tufts University, Zhuo Zhang Columbia University, Caterina Urban Inria & ENS \| PSL
16:15 20m Talk		Toward Repository-Level Program Verification with Large Language Models LMPL Si Cheng Zhong University of Toronto, Xujie Si University of Toronto DOI
16:35 15m Talk		Preguss: It Analyzes, It Specifies, It Verifies LMPL Zhongyi Wang Zhejiang University, China, Tengjie Lin Zhejiang University, Mingshuai Chen Zhejiang University, Mingqi Yang Zhejiang University, Haokun Li Peking University, Xiao Yi The Chinese University of Hong Kong, Shengchao Qin Xidian University, Jianwei Yin Zhejiang University
16:50 20m Talk		A Case Study on the Effectiveness of LLMs in Verification with Proof Assistants LMPL Barış Bayazıt University of Toronto, Yao Li Portland State University, Xujie Si University of Toronto Pre-print
17:10 20m Talk		Understanding Formal Reasoning Failures in LLMs as Abstract Interpreters LMPL Jacqueline Mitchell University of Southern California, Brian Hyeongseok Kim University of Southern California, Chenyu Zhou University of Southern California, Chao Wang University of Southern California

Thu 16 Oct
Displayed time zone: Perth change

10:30 - 12:15	RuntimeOOPSLA at Orchid East

10:30 15m Talk		Unveiling Heisenbugs with Diversified Execution OOPSLA Arjun Ramesh Carnegie Mellon University, Tianshu Huang Carnegie Mellon University, Jaspreet Riar Carnegie Mellon University, Ben L. Titzer Carnegie Mellon University, Anthony Rowe Carnegie Mellon University
10:45 15m Talk		TailTracer: Continuous Tail Tracing for Production Use OOPSLA Tianyi Liu Nanjing University, Yi Li Nanyang Technological University, Yiyu Zhang Nanjing University, Zhuangda Wang Xiamen University, Rongxin Wu Xiamen University, Xuandong Li Nanjing University, Zhiqiang Zuo Nanjing University
11:00 15m Talk		Heap-Snapshot Matching and Ordering using CAHPs: A Context-Augmented Heap-Path Representation for Exact and Partial Path Matching using Prefix Trees OOPSLA Matteo Basso Università della Svizzera italiana (USI), Aleksandar Prokopec Oracle Labs, Andrea Rosà USI Lugano, Walter Binder USI Lugano
11:15 15m Talk		Float Self-Tagging OOPSLA Olivier Melançon Université de Montréal, Manuel Serrano Inria; Université Côte d’Azur, Marc Feeley Université de Montréal Pre-print
11:30 15m Talk		HEMVM: a Heterogeneous Blockchain Framework for Interoperable Virtual Machines OOPSLA Vladyslav Nekriach University Of Toronto, Sidi Mohamed Beillahi University of Toronto, Chenxing Li Shanghai Tree-Graph Blockchain Research Institute, Peilun Li Shanghai Tree-Graph Blockchain Research Institute, Ming Wu Shanghai Tree-Graph Blockchain Research Institute, Andreas Veneris University of Toronto, Fan Long University of Toronto
11:45 15m Talk		Advancing Performance via a Systematic Application of Research and Industrial Best Practice OOPSLA Wenyu Zhao Australian National University, Stephen M. Blackburn Google; Australian National University, Kathryn S McKinley Google, Man Cao Google, Sara S. Hamouda Canva

13:45 - 15:30	Compilation 1OOPSLA at Orchid East

13:45 15m Talk		Bridging the Gap between Real-World and Formal Binary Lifting through Filtered-Simulation OOPSLA Jihee Park KAIST, Insu Yun KAIST, Sukyoung Ryu KAIST
14:00 15m Talk		Compiling Classical Sequent Calculus to Stock Hardware: The Duality of Compilation OOPSLA Philipp Schuster University of Tübingen, Marius Müller University of Tübingen, Klaus Ostermann University of Tübingen, Jonathan Immanuel Brachthäuser University of Tübingen
14:15 15m Talk		HybridPersist: A Compiler Support for User-Friendly and Efficient PM Programming OOPSLA Yiyu Zhang Nanjing University, Yongzhi Wang Xidian University, Yanfeng Gao Nanjing University, Xuandong Li Nanjing University, Zhiqiang Zuo Nanjing University
14:30 15m Talk		JavART: a Lightweight Rule-Based JIT Compiler Using Translation Rules Extracted from a Learning Approach OOPSLA Hanzhang Wang Fudan University, China, Wei Peng Fudan University, Wenwen Wang University of Georgia, Yunping Lu Fudan University, Pen-Chung Yew University of Minnesota at Twin Cities, Weihua Zhang Fudan University
14:45 15m Talk		Mind the Abstraction Gap: Bringing Equality Saturation to Real-World ML Compilers OOPSLA Arya Vohra University of Chicago, Leo Seojun Lee University of Oxford, Jakub Bachurski University of Cambridge, Oleksandr Zinenko Brium, Phitchaya Mangpo Phothilimthana OpenAI, Albert Cohen Google DeepMind, William S. Moses University of Illinois Urbana-Champaign
15:00 15m Talk		Scaling Optimization Over Uncertainty via Compilation OOPSLA Minsung Cho , John Gouwar Northeastern University, Steven Holtzen Northeastern University
15:15 15m Talk		Tracing Just-in-time Compilation for Effects and Handlers OOPSLA Marcial Gaißert University of Tübingen, CF Bolz-Tereick Heinrich-Heine-Universität Düsseldorf, Jonathan Immanuel Brachthäuser University of Tübingen Pre-print

16:00 - 17:30	Compilation 2OOPSLA at Orchid East

16:00 15m Talk		An Empirical Study of Bugs in the rustc Compiler OOPSLA Zixi Liu Nanjing University, Yang Feng Nanjing University, Yunbo Ni The Chinese University of Hong Kong, Shaohua Li The Chinese University of Hong Kong, Xizhe Yin Nanjing University, Qingkai Shi Nanjing University, Baowen Xu Nanjing University, Zhendong Su ETH Zurich
16:15 15m Talk		DESIL: Detecting Silent Bugs in MLIR Compiler Infrastructure OOPSLA Chenyao Suo Tianjin University, Jianrong Wang Tianjin University, Yongjia Wang College of Intelligence and Computing, Tianjin University, Jiajun Jiang Tianjin University, Qingchao Shen Tianjin University, Junjie Chen Tianjin University
16:30 15m Talk		GALA: A High Performance Graph Neural Network Acceleration LAnguage and Compiler OOPSLA Damitha Lenadora University of Illinois at Urbana-Champaign, Nikhil Jayakumar University of Texas at Austin, Chamika Sudusinghe University of Illinois at Urbana-Champaign, Charith Mendis University of Illinois at Urbana-Champaign
16:45 15m Talk		Non-interference Preserving Optimising Compilation OOPSLA Julian Rosemann Saarland University, Saarland Informatics Campus, Sebastian Hack Saarland University, Saarland Informatics Campus, Deepak Garg MPI-SWS
17:00 15m Talk		Synchronized Behavior Checking: A Method for Finding Missed Compiler Optimizations OOPSLA Yi Zhang Nanjing University, Yu Wang Nanjing University, Linzhang Wang Nanjing University, Ke Wang Peking University
17:15 15m Talk		Tabby: A Synthesis-Aided Compiler for High-Performance Zero-Knowledge Proof Circuits OOPSLA Junrui Liu University of California, Santa Barbara, Jiaxin Song University of Illinois at Urbana-Champaign, Yanning Chen University of Toronto, Hanzhi Liu University of California, Santa Barbara & Riema Labs, Hongbo Wen University of California, Santa Barbara & Riema Labs, Luke Pearson Polychain Capital, Yanju Chen University of California, San Diego, Yu Feng University of California at Santa Barbara

Fri 17 Oct
Displayed time zone: Perth change

10:30 - 12:15	Analysis 1OOPSLA at Orchid East

10:30 15m Talk		Artemis: Toward Accurate Detection of Server-Side Request Forgeries through LLM-Assisted Inter-Procedural Path-Sensitive Taint Analysis OOPSLA Yuchen Ji ShanghaiTech University, Ting Dai IBM Research, Zhichao Zhou School of Information Science and Technology, ShanghaiTech University, Yutian Tang University of Glasgow, United Kingdom, Jingzhu He ShanghaiTech University
10:45 15m Talk		A Sound Static Analysis Approach to I/O API Migration OOPSLA Shangyu Li The Hong Kong University of Science and Technology, Zhaoyang Zhang The Hong Kong University of Science and Technology, Sizhe Zhong The Hong Kong University of Science and Technology, Diyu Zhou Peking University, Jiasi Shen The Hong Kong University of Science and Technology
11:00 15m Talk		Automatic Linear Resource Bound Analysis for Rust via Prophecy Potentials OOPSLA Qihao Lian Peking University, Di Wang Peking University Pre-print
11:15 15m Talk		Denotational Foundations for Expected Cost Analysis OOPSLA Pedro Henrique Azevedo de Amorim Cornell University
11:30 15m Talk		IncIDFA: An Efficient and Generic Algorithm for Incremental Iterative Dataflow Analysis OOPSLA Aman Nougrahiya IIT Madras, V Krishna Nandivada IIT Madras
11:45 15m Talk		Revealing Sources of (Memory) Errors via Backward Analysis OOPSLA Flavio Ascari University of Pisa, Roberto Bruni University of Pisa, Roberta Gori Diaprtimento di Informatica, Universita' di Pisa, Italy, Francesco Logozzo Meta
12:00 15m Talk		Two Approaches to Fast Bytecode Frontend for Static Analysis OOPSLA Chenxi Li Nanjing University, China, Haoran Lin Nanjing University, China, Tian Tan Nanjing University, Yue Li Nanjing University

13:45 - 15:30	Analysis 2OOPSLA at Orchid East

13:45 15m Talk		ApkDiffer: Accurate and Scalable Cross-Version Diffing Analysis for Android Applications OOPSLA Jiarun Dai Fudan University, Mingyuan Luo Fudan University, Yuan Zhang Fudan University, Min Yang Fudan University, Minghui Yang OPPO
14:00 15m Talk		Combining Formal and Informal Information in Bayesian Program Analysis via Soft Evidences OOPSLA Tianchi Li Peking University, China, Xin Zhang Peking University
14:15 15m Talk		CoSSJIT: Combining Static Analysis and Speculation in JIT Compilers OOPSLA Aditya Anand Indian Institute of Technology Bombay, Vijay Sundaresan IBM Canada, Daryl Maier IBM Canada, Manas Thakur IIT Bombay
14:30 15m Talk		On Abstraction Refinement for Bayesian Program Analysis OOPSLA Yuanfeng Shi Peking University, Yifan Zhang Peking University, Xin Zhang Peking University
14:45 15m Talk		Sound and Modular Activity Analysis for Automatic Differentiation in MLIR OOPSLA Mai Jacob Peng McGill University, William S. Moses University of Illinois Urbana-Champaign, Oleksandr Zinenko Brium, Christophe Dubach McGill University
15:00 15m Talk		Towards a Theoretically-Backed and Practical Framework for Selective Object-Sensitive Pointer Analysis OOPSLA Chaoyue Zhang Nanjing University, Longlong Lu State Key Laboratory for Novel Software Technology, Nanjing University, China, Yifei Lu State Key Laboratory for Novel Software Technology, Nanjing University, China, Minxue Pan Nanjing University, Xuandong Li Nanjing University
15:15 15m Talk		Universal Scalability in Declarative Program Analysis (with Choice-Based Combination Pruning) OOPSLA Anastasios Antoniadis University of Athens, Greece, Ilias Tsatiris Dedaub, Neville Grech Dedaub Limited, Yannis Smaragdakis University of Athens

16:00 - 17:30	Verification 1OOPSLA at Orchid East

16:00 15m Talk		A Flow-Sensitive Refinement Type System for Verifying eBPF Programs OOPSLA Ameer Hamza Florida State University, Lucas Zavalia Florida State University Tallahassee, Arie Gurfinkel University of Waterloo, Jorge A. Navas Certora, Grigory Fedyukovich Florida State University
16:15 15m Talk		Automatically Verifying Replication-aware Linearizability OOPSLA Vimala Soundarapandian IIT Madras, Kartik Nagar IIT Madras, Aseem Rastogi Microsoft Research, KC Sivaramakrishnan IIT Madras and Tarides
16:30 15m Talk		On the Impact of Formal Verification on Software Development OOPSLA Eric Mugnier University of California San Diego, Zhou Yuanyuan UCSD, Ranjit Jhala University of California at San Diego, Michael Coblenz University of California, San Diego
16:45 15m Talk		Towards Verifying Crash Consistency OOPSLA Keonho Lee University of California, Irvine, Conan Truong University of California, Irvine, Brian Demsky University of California at Irvine
17:00 15m Talk		TraceLinking Implementations with their Verified Designs OOPSLA Finn Hackett University of British Columbia, Ivan Beschastnikh The University of British Columbia Pre-print
17:15 15m Talk		Pyrosome: Verified Compilation for Modular Metatheory OOPSLA Dustin Jamner MIT CSAIL, Gabriel Kammer MIT, Ritam Nag MIT, Adam Chlipala MIT CSAIL

Sat 18 Oct
Displayed time zone: Perth change

10:30 - 12:15	Type 2OOPSLA at Orchid East

10:30 15m Talk		Borrowing From Session Types OOPSLA Hannes Saffrich University of Freiburg, Janek Spaderna University of Freiburg, Germany, Peter Thiemann University of Freiburg, Germany, Vasco T. Vasconcelos LASIGE, University of Lisbon
10:45 15m Talk		Modal Effect Types OOPSLA Wenhao Tang The University of Edinburgh, Leo White Jane Street, Stephen Dolan Jane Street, Daniel Hillerström Category Labs and The University of Edinburgh, Sam Lindley The University of Edinburgh, Anton Lorenzen University of Edinburgh
11:00 15m Talk		On Higher-Order Model Checking of Effectful Answer-Type-Polymorphic Programs OOPSLA Taro Sekiyama National Institute of Informatics, Ugo Dal Lago University of Bologna & INRIA Sophia Antipolis, Hiroshi Unno Tohoku University
11:15 15m Talk		Proof Repair across Quotient Type Equivalences OOPSLA Cosmo Viola University of Illinois Urbana-Champaign, Max Fan Cornell University, Talia Lily Ringer University of Illinois Urbana-Champaign
11:30 15m Talk		Structural Information Flow: A Fresh Look at Types for Non-Interference OOPSLA Hemant Gouni Carnegie Mellon University, Frank Pfenning Carnegie Mellon University, USA, Jonathan Aldrich Carnegie Mellon University Pre-print
11:45 15m Talk		The Simple Essence of Overloading: Making ad-hoc polymorphism more algebraic with flow-based variational type-checking OOPSLA Jiří Beneš University of Tübingen, Jonathan Immanuel Brachthäuser University of Tübingen Pre-print
12:00 15m Talk		We’ve Got You Covered: Type-Guided Repair of Incomplete Input Generators OOPSLA Patrick LaFontaine Purdue University, Zhe Zhou Purdue University, Ashish Mishra IIT Hyderabad, Suresh Jagannathan Purdue University, Benjamin Delaware Purdue University

13:45 - 15:30	MemoryOOPSLA at Orchid East

13:45 15m Talk		Compositional Symbolic Execution for the Next 700 Memory Models OOPSLA Andreas Lööw Imperial College London, Seung Hoon Park Imperial College London, Daniele Nantes-Sobrinho Imperial College London, Sacha-Élie Ayoun Imperial College London, Opale Sjöstedt Imperial College London, Philippa Gardner Imperial College London Pre-print
14:00 15m Talk		Destination calculus: A linear λ-calculus for purely functional memory writes OOPSLA Thomas BAGREL Tweag, LORIA/INRIA, Arnaud Spiwack Tweag
14:15 15m Talk		Divining Profiler Accuracy: An Approach to Approximate Profiler Accuracy Through Machine Code-Level Slowdown OOPSLA Humphrey Burchell University of Kent, Stefan Marr University of Kent
14:30 15m Talk		HeapBuffers: Why not just using a binary serialization format for your managed memory? OOPSLA Daniele Bonetta VU Amsterdam, Júnior Löff Università della Svizzera italiana, Matteo Basso Università della Svizzera italiana (USI), Walter Binder USI Lugano
14:45 15m Talk		im2im: Automatically Converting In-Memory Image Representations using A Knowledge Graph Approach OOPSLA Fei Chen , Sunita Saha German Research Center for Artificial Intelligence (DFKI), Saarbrücken, Germany, Manuela Schuler German Research Center for Artificial Intelligence (DFKI), Saarbrücken, Germany; Saarland University, Saarbrücken, Germany, Philipp Slusallek DFKI, Germany, Tim Dahmen Aalen University, Aalen, Germany; German Research Center for Artificial Intelligence (DFKI), Saarbrücken, Germany
15:00 15m Talk		SafeRace: Assessing and Addressing WebGPU Memory Safety in the Presence of Data Races OOPSLA Reese Levine , Ashley Lee University of California, Santa Cruz, Neha Abbas University of California, Santa Cruz, Kyle Little University of Utah, Tyler Sorensen Microsoft Research and University of California at Santa Cruz
15:15 15m Talk		Symbolic MRD: Dynamic Memory, Undefined Behaviour, and Extrinsic Choice OOPSLA Jay Richards University of Kent, Daniel Wright University of Surrey, Simon Cooksey , Mark Batty University of Kent

16:00 - 17:30	AbstractionOOPSLA at Orchid East

16:00 15m Talk		Abstract Interpretation of Temporal Safety Effects of Higher Order Programs OOPSLA Mihai Nicola Stevens Institute of Technology, Chaitanya Agarwal New York University, Eric Koskinen Stevens Institute of Technology, Thomas Wies New York University
16:15 15m Talk		A Hoare Logic For Symmetry Properties OOPSLA Vaibhav Mehta Cornell University, Justin Hsu Cornell University
16:30 15m Talk		Efficient Abstract Interpretation via Selective Widening OOPSLA Jiawei Wang UNSW, Xiao Cheng Macquarie University, Yulei Sui University of New South Wales
16:45 15m Talk		Encode the $\forall\exists$ Relational Hoare Logic into Standard Hoare Logic OOPSLA Shushu Wu Shanghai Jiao Tong University, Xiwei Wu Shanghai Jiao Tong University, Qinxiang Cao Shanghai Jiao Tong University
17:00 15m Talk		Structural Abstraction and Refinement for Probabilistic Programs OOPSLA Guanyan Li University of Oxford, Juanen Li Beijing Normal University, Zhilei Han Tsinghua University, Peixin Wang East China Normal University, Hongfei Fu Shanghai Jiao Tong University, Fei He Tsinghua University
17:15 15m Talk		Work Packets: A New Abstraction for GC Software Engineering, Optimization, and Innovation OOPSLA Wenyu Zhao Australian National University, Stephen M. Blackburn Google; Australian National University, Kathryn S McKinley Google

Mon 13 Oct
Displayed time zone: Perth 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
Orchid East											SAS Opening and Keynote																																		SAS Verification																												SAS Abstraction and Proofs

Tue 14 Oct
Displayed time zone: Perth 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
Orchid East											SAS Compiler																																		SAS Abstract Interpretation																												SAS Testing and Constraint Solving

Wed 15 Oct
Displayed time zone: Perth 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
Orchid East											LMPL Keynote																																		LMPL LLMs for Program Analysis and Verification I																												LMPL LLMs for Program Analysis and Verification II

Thu 16 Oct
Displayed time zone: Perth 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
Orchid East							OOPSLA Runtime																																							OOPSLA Compilation 1																											OOPSLA Compilation 2

Fri 17 Oct
Displayed time zone: Perth 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
Orchid East							OOPSLA Analysis 1																																							OOPSLA Analysis 2																											OOPSLA Verification 1

Sat 18 Oct
Displayed time zone: Perth 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
Orchid East							OOPSLA Type 2																																							OOPSLA Memory																											OOPSLA Abstraction

Mon 13 Oct
Displayed time zone: Perth 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
Orchid East											SAS Opening 10:50 - 11:00			SAS On a simple problem due to Yves Bertot 11:05 - 12:05																															SAS Multi-Modal Verification of Distributed Systems in Lean 13:40 - 14:40												SAS Verifying Neural Networks with PyRAT 14:40 - 15:00				SAS Enhancing Neural Network Robustness via Synthesis of Repair Programs 15:00 - 15:20												SAS Relating Distances and Abstractions: An Abstract Interpretation Perspective 16:00 - 16:20				SAS Precise Abstract Interpretation of Probabilistic Programs with Interval ... 16:20 - 16:40				SAS Specifying and Verifying Future Conditions 16:40 - 17:00				SAS Contextual Equality Saturation 17:00 - 17:20				SAS Abstracting Concolic Execution for Soft Contract Verification 17:20 - 17:40

Tue 14 Oct
Displayed time zone: Perth 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
Orchid East											SAS From Within: Compiler Testing and Validation via Compilers 10:50 - 11:45											SAS Ductape: Optimizing Dynamically Typed Programs using Ahead-of-Time Comp ... 11:45 - 12:05																							SAS Towards static analyses and abstract domains for hyperproperties 13:40 - 14:40												SAS Comparing the Precision of Abstract Operators in the eBPF Verifier usin ... 14:40 - 15:00				SAS A Programming Language for Feasible Solutions 15:00 - 15:20												SAS Bounded-Exhaustive Subspace Diversification for SMT Solver Testing 16:00 - 16:20				SAS Monarch: A Modular Framework for Abstract Definitional Interpreters in ... 16:20 - 16:40				SAS Delta Store Semantics: Abstract Garbage Collection for Abstract Definit ... 16:40 - 17:00				SAS Automated Catamorphism Synthesis for Solving Constrained Horn Clauses o ... 17:00 - 17:20				SAS Formal Analysis of Networked PLC Controllers Interacting with Physical ... 17:20 - 17:40

Wed 15 Oct
Displayed time zone: Perth 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
Orchid East											LMPL AI Safety through Programming? 10:50 - 12:05																																		LMPL Function Renaming in Reverse Engineering of Embedded Device Firmware wi ... 13:40 - 13:55			LMPL Enhancing Semantic Understanding in Pointer Analysis Using Large Langua ... 13:55 - 14:10			LMPL Improving SAST Detection Capability with LLMs and Enhanced DFA 14:10 - 14:25			LMPL ClearAgent: Agentic Binary Analysis for Effective Vulnerability Detection 14:25 - 14:40			LMPL CG-Bench: Can Language Models Assist Call Graph Construction in the Rea ... 14:40 - 14:55			LMPL Beyond Static Pattern Matching? Rethinking Automatic Cryptographic API ... 14:55 - 15:15													LMPL Hallucination-Resilient LLM-Driven Sound and Tunable Static Analysis 16:00 - 16:15			LMPL Toward Repository-Level Program Verification with Large Language Models 16:15 - 16:35				LMPL Preguss: It Analyzes, It Specifies, It Verifies 16:35 - 16:50			LMPL A Case Study on the Effectiveness of LLMs in Verification with Proof As ... 16:50 - 17:10				LMPL Understanding Formal Reasoning Failures in LLMs as Abstract Interpreters 17:10 - 17:30

Thu 16 Oct
Displayed time zone: Perth 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
Orchid East							SPLASH OOPSLA Unveiling Heisenbugs with Diversified Execution 10:30 - 10:45			SPLASH OOPSLA TailTracer: Continuous Tail Tracing for Production Use 10:45 - 11:00			SPLASH OOPSLA Heap-Snapshot Matching and Ordering using CAHPs: A Context-Augmented He ... 11:00 - 11:15			SPLASH OOPSLA Float Self-Tagging 11:15 - 11:30			SPLASH OOPSLA HEMVM: a Heterogeneous Blockchain Framework for Interoperable Virtual M ... 11:30 - 11:45			SPLASH OOPSLA Advancing Performance via a Systematic Application of Research and Indu ... 11:45 - 12:00																								SPLASH OOPSLA Bridging the Gap between Real-World and Formal Binary Lifting through F ... 13:45 - 14:00			SPLASH OOPSLA Compiling Classical Sequent Calculus to Stock Hardware: The Duality of ... 14:00 - 14:15			SPLASH OOPSLA HybridPersist: A Compiler Support for User-Friendly and Efficient PM Pr ... 14:15 - 14:30			SPLASH OOPSLA JavART: a Lightweight Rule-Based JIT Compiler Using Translation Rules E ... 14:30 - 14:45			SPLASH OOPSLA Mind the Abstraction Gap: Bringing Equality Saturation to Real-World ML ... 14:45 - 15:00			SPLASH OOPSLA Scaling Optimization Over Uncertainty via Compilation 15:00 - 15:15			SPLASH OOPSLA Tracing Just-in-time Compilation for Effects and Handlers 15:15 - 15:30									SPLASH OOPSLA An Empirical Study of Bugs in the rustc Compiler 16:00 - 16:15			SPLASH OOPSLA DESIL: Detecting Silent Bugs in MLIR Compiler Infrastructure 16:15 - 16:30			SPLASH OOPSLA GALA: A High Performance Graph Neural Network Acceleration LAnguage and ... 16:30 - 16:45			SPLASH OOPSLA Non-interference Preserving Optimising Compilation 16:45 - 17:00			SPLASH OOPSLA Synchronized Behavior Checking: A Method for Finding Missed Compiler Op ... 17:00 - 17:15			SPLASH OOPSLA Tabby: A Synthesis-Aided Compiler for High-Performance Zero-Knowledge P ... 17:15 - 17:30

Fri 17 Oct
Displayed time zone: Perth 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
Orchid East							SPLASH OOPSLA Artemis: Toward Accurate Detection of Server-Side Request Forgeries thr ... 10:30 - 10:45			SPLASH OOPSLA A Sound Static Analysis Approach to I/O API Migration 10:45 - 11:00			SPLASH OOPSLA Automatic Linear Resource Bound Analysis for Rust via Prophecy Potentials 11:00 - 11:15			SPLASH OOPSLA Denotational Foundations for Expected Cost Analysis 11:15 - 11:30			SPLASH OOPSLA IncIDFA: An Efficient and Generic Algorithm for Incremental Iterative D ... 11:30 - 11:45			SPLASH OOPSLA Revealing Sources of (Memory) Errors via Backward Analysis 11:45 - 12:00			SPLASH OOPSLA Two Approaches to Fast Bytecode Frontend for Static Analysis 12:00 - 12:15																					SPLASH OOPSLA ApkDiffer: Accurate and Scalable Cross-Version Diffing Analysis for And ... 13:45 - 14:00			SPLASH OOPSLA Combining Formal and Informal Information in Bayesian Program Analysis ... 14:00 - 14:15			SPLASH OOPSLA CoSSJIT: Combining Static Analysis and Speculation in JIT Compilers 14:15 - 14:30			SPLASH OOPSLA On Abstraction Refinement for Bayesian Program Analysis 14:30 - 14:45			SPLASH OOPSLA Sound and Modular Activity Analysis for Automatic Differentiation in MLIR 14:45 - 15:00			SPLASH OOPSLA Towards a Theoretically-Backed and Practical Framework for Selective Ob ... 15:00 - 15:15			SPLASH OOPSLA Universal Scalability in Declarative Program Analysis (with Choice-Base ... 15:15 - 15:30									SPLASH OOPSLA A Flow-Sensitive Refinement Type System for Verifying eBPF Programs 16:00 - 16:15			SPLASH OOPSLA Automatically Verifying Replication-aware Linearizability 16:15 - 16:30			SPLASH OOPSLA On the Impact of Formal Verification on Software Development 16:30 - 16:45			SPLASH OOPSLA Towards Verifying Crash Consistency 16:45 - 17:00			SPLASH OOPSLA TraceLinking Implementations with their Verified Designs 17:00 - 17:15			SPLASH OOPSLA Pyrosome: Verified Compilation for Modular Metatheory 17:15 - 17:30

Sat 18 Oct
Displayed time zone: Perth 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
Orchid East							SPLASH OOPSLA Borrowing From Session Types 10:30 - 10:45			SPLASH OOPSLA Modal Effect Types 10:45 - 11:00			SPLASH OOPSLA On Higher-Order Model Checking of Effectful Answer-Type-Polymorphic Pro ... 11:00 - 11:15			SPLASH OOPSLA Proof Repair across Quotient Type Equivalences 11:15 - 11:30			SPLASH OOPSLA Structural Information Flow: A Fresh Look at Types for Non-Interference 11:30 - 11:45			SPLASH OOPSLA The Simple Essence of Overloading: Making ad-hoc polymorphism more alge ... 11:45 - 12:00			SPLASH OOPSLA We’ve Got You Covered: Type-Guided Repair of Incomplete Input Generators 12:00 - 12:15																					SPLASH OOPSLA Compositional Symbolic Execution for the Next 700 Memory Models 13:45 - 14:00			SPLASH OOPSLA Destination calculus: A linear λ-calculus for purely functional memory ... 14:00 - 14:15			SPLASH OOPSLA Divining Profiler Accuracy: An Approach to Approximate Profiler Accurac ... 14:15 - 14:30			SPLASH OOPSLA HeapBuffers: Why not just using a binary serialization format for your ... 14:30 - 14:45			SPLASH OOPSLA im2im: Automatically Converting In-Memory Image Representations using A ... 14:45 - 15:00			SPLASH OOPSLA SafeRace: Assessing and Addressing WebGPU Memory Safety in the Presence ... 15:00 - 15:15			SPLASH OOPSLA Symbolic MRD: Dynamic Memory, Undefined Behaviour, and Extrinsic Choice 15:15 - 15:30									SPLASH OOPSLA Abstract Interpretation of Temporal Safety Effects of Higher Order Programs 16:00 - 16:15			SPLASH OOPSLA A Hoare Logic For Symmetry Properties 16:15 - 16:30			SPLASH OOPSLA Efficient Abstract Interpretation via Selective Widening 16:30 - 16:45			SPLASH OOPSLA Encode the $\forall\exists$ Relational Hoare Logic into Standard Hoare ... 16:45 - 17:00			SPLASH OOPSLA Structural Abstraction and Refinement for Probabilistic Programs 17:00 - 17:15			SPLASH OOPSLA Work Packets: A New Abstraction for GC Software Engineering, Optimizati ... 17:15 - 17:30

Room information: Orchid East

This program is tentative and subject to change.

Program Display Configuration

Mon 13 OctDisplayed time zone: Perth change

Tue 14 OctDisplayed time zone: Perth change

Wed 15 OctDisplayed time zone: Perth change

Thu 16 OctDisplayed time zone: Perth change

Fri 17 OctDisplayed time zone: Perth change

Sat 18 OctDisplayed time zone: Perth change

Mon 13 OctDisplayed time zone: Perth change

SAS

SAS

SAS

Tue 14 OctDisplayed time zone: Perth change

SAS

SAS

SAS

Wed 15 OctDisplayed time zone: Perth change

LMPL

LMPL

LMPL

Thu 16 OctDisplayed time zone: Perth change

OOPSLA

OOPSLA

OOPSLA

Fri 17 OctDisplayed time zone: Perth change

OOPSLA

OOPSLA

OOPSLA

Sat 18 OctDisplayed time zone: Perth change

OOPSLA

OOPSLA

OOPSLA

Mon 13 OctDisplayed time zone: Perth change

Tue 14 OctDisplayed time zone: Perth change

Wed 15 OctDisplayed time zone: Perth change

Thu 16 OctDisplayed time zone: Perth change

Fri 17 OctDisplayed time zone: Perth change

Sat 18 OctDisplayed time zone: Perth change

Mon 13 Oct
Displayed time zone: Perth change

Tue 14 Oct
Displayed time zone: Perth change

Wed 15 Oct
Displayed time zone: Perth change

Thu 16 Oct
Displayed time zone: Perth change

Fri 17 Oct
Displayed time zone: Perth change

Sat 18 Oct
Displayed time zone: Perth change

Mon 13 Oct
Displayed time zone: Perth change

Tue 14 Oct
Displayed time zone: Perth change

Wed 15 Oct
Displayed time zone: Perth change

Thu 16 Oct
Displayed time zone: Perth change

Fri 17 Oct
Displayed time zone: Perth change

Sat 18 Oct
Displayed time zone: Perth change

Mon 13 Oct
Displayed time zone: Perth change

Tue 14 Oct
Displayed time zone: Perth change

Wed 15 Oct
Displayed time zone: Perth change

Thu 16 Oct
Displayed time zone: Perth change

Fri 17 Oct
Displayed time zone: Perth change

Sat 18 Oct
Displayed time zone: Perth change