SPLASH 2025 will feature keynote talks by Julia Lawall, Frank Piessens, and Zhendong Su.
Accepted Papers
| Title | |
|---|---|
| Automating maintenance of the Linux kernel: a perspective over 20 years SPLASH Keynotes K: Julia Lawall | |
| Software Stacks for Confidential Computing Hardware SPLASH Keynotes | |
| The Quest Toward that Perfect Compiler SPLASH Keynotes K: Zhendong Su |
Dates
Tracks
Plenary
This program is tentative and subject to change.
Thu 16 OctDisplayed time zone: Perth change
Thu 16 Oct
Displayed time zone: Perth change
09:00 - 10:00 | |||
09:00 60mKeynote | Automating maintenance of the Linux kernel: a perspective over 20 years SPLASH Keynotes | ||
10:00 - 10:30 | |||
10:00 30mCoffee break | Break ICFP/SPLASH Catering | ||
10:30 - 12:15 | |||
10:30 15mTalk | 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 15mTalk | 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 15mTalk | 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 15mTalk | 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 15mTalk | 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 15mTalk | 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 | ||
10:30 - 12:15 | |||
10:30 15mTalk | ABC: Towards a Universal Code Styler through Model Merging OOPSLA Yitong Chen School of Computer Science and Engineering, College of Software Engineering, School of Artificial Intelligence, Southeast University, Zhiqiang Gao School of Computer Science and Engineering, College of Software Engineering, School of Artifical Intelligence, Southeast University, Chuanqi Shi School of Computer Science and Engineering, College of Software Engineering, School of Artifical Intelligence, Southeast University, Baixuan Li School of Computer Science and Engineering, College of Software Engineering, School of Artifical Intelligence, Southeast University, Miao Gao School of Computer Science and Engineering, College of Software Engineering, School of Artifical Intelligence, Southeast University | ||
10:45 15mTalk | Binary Cryptographic Function Identification via Similarity Analysis with Path-insensitive Emulation OOPSLA | ||
11:00 15mTalk | Boosting Program Reduction with the Missing Piece of Syntax-Guided Transformations OOPSLA Zhenyang Xu University of Waterloo, Yongqiang Tian Monash University, Mengxiao Zhang , Chengnian Sun University of Waterloo | ||
11:15 15mTalk | Code Style Sheets: CSS for Code OOPSLA | ||
11:30 15mTalk | Enhancing APR with PRISM: A Semantic-Based Approach to Overfitting Patch Detection OOPSLA | ||
11:45 15mTalk | PAFL: Enhancing Fault Localizers by Leveraging Project-Specific Fault Patterns OOPSLA | ||
12:00 15mTalk | Stencil-Lifting: Hierarchical Recursive Lifting System for Extracting Summary of Stencil Kernel in Legacy Codes OOPSLA Mingyi Li , Junmin Xiao , Siyan Chen Institute of Computing Technology, Chinese Academy of Sciences, Hui Ma Institute of Computing Technology, Chinese Academy of Sciences, Xi Chen Institute of Computing Technology, Chinese Academy of Sciences, Peihua Bao University of Chinese Academy of Sciences, Liang Yuan Chinese Academy of Sciences, Guangming Tan Chinese Academy of Sciences(CAS) | ||
13:45 - 15:30 | |||
13:45 15mTalk | A Unifying Approach to Product Constructions for Quantitative Temporal Inference OOPSLA Kazuki Watanabe National Institute of Informatics; SOKENDAI, Sebastian Junges Radboud University, Jurriaan Rot Radboud University Nijmegen, Ichiro Hasuo National Institute of Informatics, Japan | ||
14:00 15mTalk | Contract System Metatheories à la Carte: A Transition-System View of Contracts OOPSLA Shu-Hung You Northwestern University, USA, Christos Dimoulas Northwestern University, Robert Bruce Findler Northwestern University | ||
14:15 15mTalk | Incremental Bidirectional Typing via Order Maintenance OOPSLA Thomas J. Porter University of Michigan, Marisa Kirisame University of Utah, Ivan Wei University of Michigan, Pavel Panchekha University of Utah, Cyrus Omar University of Michigan | ||
14:30 15mTalk | The Power of Regular Constraint Propagation OOPSLA Matthew Hague Royal Holloway University of London, Artur Jez University of Wroclaw, Anthony Widjaja Lin RPTU Kaiserslautern-Landau and Max-Planck Institute for Software Systems, Oliver Markgraf RPTU Kaiserslautern-Landau, Philipp Ruemmer University of Regensburg and Uppsala University | ||
14:45 15mTalk | Orax: A Feedback-Driven Framework for Efficiently Solving Satisfiability Modulo Theories and Oracles OOPSLA Zhineng Zhong Key Laboratory of High-Confidence Software Technologies (MOE), School of Computer Science, Peking University, Ziqi Zhang University of Illinois Urbana-Champaign, Hanqin Guan Peking University, Ding Li Peking University | ||
15:00 15mTalk | Software Model Checking via Summary-Guided Search OOPSLA Ruijie Fang University of Texas at Austin, Zachary Kincaid Princeton University, Thomas Reps University of Wisconsin-Madison DOI Pre-print | ||
16:00 - 17:30 | |||
16:00 15mTalk | 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 15mTalk | 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 15mTalk | 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 15mTalk | 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 15mTalk | 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 15mTalk | 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 | ||
16:00 - 17:30 | |||
16:00 15mTalk | Compressed and Parallelized Structured Tensor Algebra OOPSLA Mahdi Ghorbani University of Edinburgh, Emilien Bauer , Tobias Grosser University of Cambridge, Amir Shaikhha University of Edinburgh | ||
16:15 15mTalk | Exploring the Theory and Practice of Concurrency in the Entity-Component-System Pattern OOPSLA Patrick Redmond University of California, Santa Cruz, Jonathan Castello University of California, Santa Cruz, Jose Calderon Galois, Inc., Lindsey Kuper University of California, Santa Cruz Pre-print | ||
16:30 15mTalk | HieraSynth: A Parallel Framework for Complete Super-Optimization with Hierarchical Space Decomposition OOPSLA | ||
16:45 15mTalk | Lilo: A Higher-Order, Relational Concurrent Separation Logic for Liveness OOPSLA Dongjae Lee Massachusetts Institute of Technology, Janggun Lee KAIST, Taeyoung Yoon Seoul National University, Minki Cho Seoul National University, Jeehoon Kang FuriosaAI, Chung-Kil Hur Seoul National University | ||
17:00 15mTalk | Opportunistically Parallel Lambda Calculus OOPSLA Stephen Mell University of Pennsylvania, Konstantinos Kallas University of California, Los Angeles, Steve Zdancewic University of Pennsylvania, Osbert Bastani University of Pennsylvania | ||
17:15 15mTalk | Soundness of Predictive Concurrency Analyses OOPSLA Shuyang Liu , Doug Lea State University of New York (SUNY) Oswego, Jens Palsberg University of California, Los Angeles (UCLA) | ||
Fri 17 OctDisplayed time zone: Perth change
Fri 17 Oct
Displayed time zone: Perth change
09:00 - 10:00 | |||
09:00 60mKeynote | The Quest Toward that Perfect Compiler SPLASH Keynotes | ||
10:00 - 10:30 | |||
10:00 30mCoffee break | Break ICFP/SPLASH Catering | ||
10:30 - 12:15 | |||
10:30 15mTalk | 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 15mTalk | 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 15mTalk | Automatic Linear Resource Bound Analysis for Rust via Prophecy Potentials OOPSLA Pre-print | ||
11:15 15mTalk | Denotational Foundations for Expected Cost Analysis OOPSLA Pedro Henrique Azevedo de Amorim Cornell University | ||
11:30 15mTalk | IncIDFA: An Efficient and Generic Algorithm for Incremental Iterative Dataflow Analysis OOPSLA | ||
11:45 15mTalk | 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 15mTalk | 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 | ||
10:30 - 12:15 | |||
10:30 15mTalk | Efficient Algorithms for the Uniform Tokenization Problem OOPSLA | ||
10:45 15mTalk | REPTILE: Performant Tiling of Recurrences OOPSLA Muhammad Usman Tariq Stanford University, Shiv Sundram Stanford University, Fredrik Kjolstad Stanford University | ||
11:00 15mTalk | SPLAT: A framework for optimised GPU code-generation for SParse reguLar ATtention OOPSLA Ahan Gupta University of Illinois at Urbana-Champaign, Yueming Yuan University of Illinois Urbana-Champaign, Devansh Jain University of Illinois at Urbana-Champaign, Yuhao Ge University of Illinois at Urbana-Champaign, David Aponte Microsoft, Yanqi Zhou Google, Charith Mendis University of Illinois at Urbana-Champaign | ||
11:15 15mTalk | Statically Analyzing the Dataflow of R Programs OOPSLA | ||
11:30 15mTalk | Static Inference of Regular Grammars for Ad Hoc Parsers OOPSLA Pre-print | ||
11:45 15mTalk | Syntactic Completions with Material Obligations OOPSLA David Moon University of Michigan, Andrew Blinn University of Michigan, Thomas J. Porter University of Michigan, Cyrus Omar University of Michigan DOI Pre-print | ||
10:30 - 12:15 | |||
10:30 15mTalk | Fast Client-Driven CFL-Reachability via Regularization-Based Graph Simplification OOPSLA Chenghang Shi SKLP, Institute of Computing Technology, CAS, Dongjie He Chongqing University, China, Haofeng Li SKLP, Institute of Computing Technology, CAS, Jie Lu SKLP, Institute of Computing Technology, CAS, China, Lian Li Institute of Computing Technology at Chinese Academy of Sciences; University of Chinese Academy of Sciences, Jingling Xue University of New South Wales | ||
10:45 15mTalk | Flexible and Expressive Typed Path Patterns for GQL OOPSLA Wenjia Ye National University of Singapore, Matías Toro University of Chile, Tomás Diaz University of Chile, Bruno C. d. S. Oliveira University of Hong Kong, Manuel Rigger National University of Singapore, Claudio Gutierrez DCC, Universidad de Chile & IMFD, Domagoj Vrgoč Pontificia Universidad Católica de Chile & IMFD Chile | ||
11:00 15mTalk | Quantified Underapproximation via Labeled Bunches OOPSLA Lang Liu Illinois Institute of Technology, Farzaneh Derakhshan Illinois Institute of Technology, Limin Jia Carnegie Mellon University, Gabriel A. Moreno Carnegie Mellon University Software Engineering Institute, Mark Klein Carnegie Mellon University | ||
11:15 15mTalk | HpC: A Calculus for Hybrid and Mobile Systems OOPSLA Xiong Xu Institute of Software, Chinese Academy of Sciences, Jean-Pierre Talpin INRIA, France, Shuling Wang Institute of Software, Chinese Academy of Sciences, Bohua Zhan Huawei Technologies Co., Ltd., Xinxin Liu Institute of software, Chinese academy of sciences, Naijun Zhan Peking University | ||
11:30 15mTalk | Notions of Stack-manipulating Computation and Relative Monads OOPSLA Yuchen Jiang University of Michigan, Runze Xue University of Michigan; University of Cambridge; Indiana University, Max S. New University of Michigan | ||
11:45 15mTalk | Peepco: Batch-Based Consistency Optimization OOPSLA Ivan Kuraj Massachusetts Institute of Technology, Jack Feser Basis, Nadia Polikarpova University of California at San Diego, Armando Solar-Lezama Massachusetts Institute of Technology | ||
13:45 - 15:30 | |||
13:45 15mTalk | An Empirical Evaluation of Property-Based Testing in Python OOPSLA | ||
14:00 15mTalk | Fray: An Efficient General-Purpose Concurrency Testing Platform for the JVM OOPSLA Ao Li Carnegie Mellon University, Byeongjee Kang Carnegie Mellon University, Vasudev Vikram Carnegie Mellon University, Isabella Laybourn Carnegie Mellon University, Samvid Dharanikota Efficient Computer, Shrey Tiwari Carnegie Mellon University, Rohan Padhye Carnegie Mellon University Pre-print Media Attached | ||
14:15 15mTalk | Fuzzing C++ Compilers via Type-Driven Mutation OOPSLA Bo Wang Beijing Jiaotong University, Chong Chen Beijing Jiaotong University, Ming Deng Beijing Jiaotong University, Junjie Chen Tianjin University, Xing Zhang Peking University, Youfang Lin Beijing Jiaotong University, Dan Hao Peking University, Jun Sun Singapore Management University | ||
14:30 15mTalk | Interleaving Large Language Models for Compiler Testing OOPSLA | ||
14:45 15mTalk | Model-guided Fuzzing of Distributed Systems OOPSLA Ege Berkay Gulcan Delft University of Technology, Burcu Kulahcioglu Ozkan Delft University of Technology, Rupak Majumdar MPI-SWS, Srinidhi Nagendra IRIF, Chennai Mathematical Institute | ||
15:00 15mTalk | Tuning Random Generators: Property-Based Testing as Probabilistic Programming OOPSLA Ryan Tjoa University of Washington; Jane Street, Poorva Garg University of California, Los Angeles, Harrison Goldstein University at Buffalo, the State University of New York at Buffalo, Todd Millstein University of California at Los Angeles, Benjamin C. Pierce University of Pennsylvania, Guy Van den Broeck University of California at Los Angeles Pre-print | ||
15:15 15mTalk | Understanding and Improving Flaky Test Classification OOPSLA Shanto Rahman The University of Texas at Austin, Saikat Dutta Cornell University, August Shi The University of Texas at Austin | ||
13:45 - 15:30 | |||
13:45 15mTalk | A complete formal semantics of eBPF instruction set architecture for Solana OOPSLA Shenghao Yuan Zhejiang University, Zhuoruo Zhang Zhejiang University, Jiayi Lu Zhejiang University, David Sanan Singapore Institute of Technology, Rui Chang Zhejiang University, Yongwang Zhao Zhejiang University | ||
14:00 15mTalk | Adequacy for Algebraic Effects Revisited OOPSLA Alex Kavvos University of Bristol | ||
14:15 15mTalk | A Mechanized Semantics for Dataflow Circuits OOPSLA Tony Law Univ Rennes, Inria, CNRS, IRISA, Delphine Demange Univ Rennes, Inria, CNRS, IRISA, Sandrine Blazy University of Rennes | ||
14:30 15mTalk | Dynamic Wind for Effect Handlers OOPSLA David Voigt University of Tübingen, Philipp Schuster University of Tübingen, Jonathan Immanuel Brachthäuser University of Tübingen Pre-print | ||
14:45 15mTalk | React-tRace: A Semantics for Understanding React Hooks OOPSLA Jay Lee Seoul National University, Joongwon Ahn Seoul National University, Kwangkeun Yi Seoul National University Pre-print | ||
15:00 15mTalk | Semantics of Sets of Programs OOPSLA Jinwoo Kim University of Wisconsin-Madison; Seoul National University, Shaan Nagy University of Wisconsin-Madison, Thomas Reps University of Wisconsin-Madison, Loris D'Antoni University of California at San Diego | ||
15:15 15mTalk | Zero-Overhead Lexical Effect Handlers OOPSLA Cong Ma University of Waterloo, Zhaoyi Ge University of Waterloo, Max Jung University of Waterloo, Yizhou Zhang University of Waterloo | ||
16:00 - 17:30 | |||
16:00 15mTalk | Bennet: Randomized Specification Testing for Heap-Manipulating Programs OOPSLA | ||
16:15 15mTalk | DepFuzz: Efficient Smart Contract Fuzzing with Function Dependence Guidance OOPSLA Chenyang Ma Nanjing University of Science and Technology, Wei Song Nanjing University of Science and Technology, Jeff Huang Texas A&M University | ||
16:30 15mTalk | Extraction and Mutation at a High Level: Template-Based Fuzzing for JavaScript Engines OOPSLA Wai Kin Wong Hong Kong University of Science and Technology, Dongwei Xiao Hong Kong University of Science and Technology, Cheuk Tung LAI VX Research Limited, Yiteng Peng Hong Kong University of Science and Technology, Daoyuan Wu Lingnan University, Shuai Wang Hong Kong University of Science and Technology | ||
16:45 15mTalk | Finding Compiler Bugs through Cross-Language Code Generator and Differential Testing OOPSLA Qiong Feng Nanjing University of Science and Technology, Xiaotian Ma Nanjing University of Science and Technology, Ziyuan Feng Nanjing University of Science and Technology, Marat Akhin JetBrains, Wei Song Nanjing University of Science and Technology, Peng Liang Wuhan University, China | ||
17:00 15mTalk | Formalizing Linear Motion G-code for Invariant Checking and Differential Testing of Fabrication Tools OOPSLA | ||
16:00 - 17:30 | |||
16:00 15mTalk | Debugging WebAssembly? Put some Whamm on it! OOPSLA Elizabeth Gilbert Carnegie Mellon University, Matthew Schneider Carnegie Mellon University, Zixi An , Suhas Thalanki Carnegie Mellon University, Wavid Bowman University of Florida, Alexander Bai New York University, Ben L. Titzer Carnegie Mellon University, Heather Miller Carnegie Mellon University and Two Sigma | ||
16:15 15mTalk | MIO: Multiverse Debugging in the face of Input/Output OOPSLA Tom Lauwaerts Universiteit Gent, Belgium, Maarten Steevens Ghent University, Belgium, Christophe Scholliers Universiteit Gent, Belgium | ||
16:30 15mTalk | PReMM: LLM-Based Program Repair for Multi-Method Bugs via Divide and Conquer OOPSLA Linna Xie Nanjing University, Zhong Li Nanjing University, Yu Pei Hong Kong Polytechnic University, Zhongzhen Wen Nanjing University, Kui Liu Huawei, Tian Zhang Nanjing University, Xuandong Li Nanjing University | ||
16:45 15mTalk | Show Me Why It's Correct: Saving 1/3 of Debugging Time in Program Repair with Interactive Runtime Comparison OOPSLA Ruixin Wang Purdue University, Zhongkai Zhao National University of Singapore, Le Fang Purdue University, Nan Jiang Purdue University, Yiling Lou Fudan University, Lin Tan Purdue University, Tianyi Zhang Purdue University | ||
17:00 15mTalk | Translation Validation for LLVM's AArch64 Backend OOPSLA Ryan Berger Nvidia, Mitch Briles University of Utah, Nader Boushehrinejad Moradi University of Utah, Nicholas Coughlin Defence Science and Technology Group, Australia, Kait Lam Defence Science and Technology Group / School of EECS, University of Queensland, Nuno P. Lopes INESC-ID; Instituto Superior Técnico - University of Lisbon, Stefan Mada University of Utah, Tanmay Tirpankar University of Utah, John Regehr University of Utah | ||
17:15 15mTalk | Validating SMT Rewriters via Rewrite Space Exploration Supported by Generative Equality Saturation OOPSLA Maolin Sun Nanjing University, Yibiao Yang Nanjing University, Jiangchang Wu State Key Laboratory for Novel Software Technology, Nanjing University, Yuming Zhou Nanjing University | ||
16:00 - 17:30 | |||
16:00 15mTalk | A Domain-Specific Probabilistic Programming Language for Reasoning about Reasoning (or: a memo on memo) OOPSLA Kartik Chandra MIT, Tony Chen MIT, Joshua B. Tenenbaum Massachusetts Institute of Technology, Jonathan Ragan-Kelley Massachusetts Institute of Technology | ||
16:15 15mTalk | ROSpec: A Domain-Specific Language for ROS-based Robot Software OOPSLA Paulo Canelas Carnegie Mellon University, Bradley Schmerl School of Computer Science, Carnegie Mellon University, Alcides Fonseca LASIGE; University of Lisbon, Christopher Steven Timperley Carnegie Mellon University DOI Pre-print Media Attached | ||
16:30 15mTalk | Large Language Model powered Symbolic Execution OOPSLA Yihe Li National University of Singapore, Ruijie Meng National University of Singapore, Singapore, Gregory J. Duck National University of Singapore | ||
16:45 15mTalk | Multi-Language Probabilistic Programming OOPSLA Sam Stites Northeastern University, John Li Northeastern University, Steven Holtzen Northeastern University | ||
17:00 15mTalk | Polymorphic Records for Dynamic Languages OOPSLA | ||
17:30 - 18:15 | |||
17:30 15mAwards | SPLASH Awards OOPSLA S: Alex Potanin Australian National University, S: Charles Zhang The Hong Kong University of Science and Technology | ||
Sat 18 OctDisplayed time zone: Perth change
Sat 18 Oct
Displayed time zone: Perth change
09:00 - 10:00 | |||
09:00 60mKeynote | Software Stacks for Confidential Computing Hardware SPLASH Keynotes | ||
10:00 - 10:30 | |||
10:00 30mCoffee break | Break ICFP/SPLASH Catering | ||
10:30 - 12:15 | |||
10:30 15mTalk | 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 15mTalk | 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 15mTalk | 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 15mTalk | 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 15mTalk | 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 15mTalk | The Simple Essence of Overloading: Making ad-hoc polymorphism more algebraic with flow-based variational type-checking OOPSLA Pre-print | ||
12:00 15mTalk | 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 | ||
10:30 - 12:15 | |||
10:30 15mTalk | Abstraction Refinement-guided Program Synthesis for Robot Learning from Demonstrations OOPSLA Guofeng Cui Rutgers University, Yuning Wang Rutgers University, Wensen Mao Rutgers University, Yuanlin Duan Rutgers University, He Zhu Rutgers University, USA | ||
10:45 15mTalk | API-guided Dataset Synthesis to Finetune Large Code Models OOPSLA Li Zongjie Hong Kong University of Science and Technology, Daoyuan Wu Lingnan University, Shuai Wang Hong Kong University of Science and Technology, Zhendong Su ETH Zurich | ||
11:00 15mTalk | Fast Constraint Synthesis for C++ Function Templates OOPSLA | ||
11:15 15mTalk | Hambazi: Spatial Coordination Synthesis for Augmented Reality OOPSLA Yi-Zhen Tsai University of California, Riverside, Jiasi Chen University of Michigan, Mohsen Lesani University of California at Santa Cruz | ||
11:30 15mTalk | Inductive Synthesis of Inductive Heap Predicates OOPSLA | ||
11:45 15mTalk | LOUD: Synthesizing Strongest and Weakest Specifications OOPSLA Kanghee Park University of Wisconsin-Madison, Xuanyu Peng University of California, San Diego, Loris D'Antoni University of California at San Diego | ||
12:00 15mTalk | Metamorph: Synthesizing Large Objects from Dafny Specifications OOPSLA Aleksandr Fedchin Tufts University, Alexander Bai New York University, Jeffrey S. Foster Tufts University | ||
10:30 - 12:15 | |||
10:30 15mTalk | AccelerQ: Accelerating Quantum Eigensolvers With Machine Learning on Quantum Simulators OOPSLA Avner Bensoussan King's College London, Elena Chachkarova Kings College London, Karine Even-Mendoza King’s College London, Sophie Fortz King's College London, Connor Lenihan King's College London | ||
10:45 15mTalk | A Language for Quantifying Quantum Network Behavior OOPSLA Anita Buckley USI Lugano, Pavel Chuprikov Télécom Paris, Institut Polytechnique de Paris, Rodrigo Otoni USI Lugano, Robert Soulé Yale University, Robert Rand University of Chicago, Patrick Eugster USI Lugano, Switzerland | ||
11:00 15mTalk | Compositional Quantum Control Flow with Efficient Compilation in Qunity OOPSLA Mikhail Mints California Institute of Technology, Finn Voichick University of Maryland, Leonidas Lampropoulos University of Maryland, College Park, Robert Rand University of Chicago | ||
11:15 15mTalk | Dependency-Aware Compilation for Surface Code Quantum Architectures OOPSLA Abtin Molavi University of Wisconsin-Madison, Amanda Xu University of Wisconsin-Madison, Swamit Tannu University of Wisconsin-Madison, Aws Albarghouthi University of Wisconsin-Madison | ||
11:30 15mTalk | QbC: Quantum Correctness by Construction OOPSLA | ||
11:45 15mTalk | qblaze: An Efficient and Scalable Sparse Quantum Simulator OOPSLA Hristo Venev INSAIT, Sofia University "St. Kliment Ohridski", Thien Udomsrirungruang University of Oxford, Dimitar Dimitrov INSAIT, Sofia University "St. Kliment Ohridski", Timon Gehr ETH Zurich, Martin Vechev ETH Zurich | ||
12:00 15mTalk | Shaking Up Quantum Simulators with Fuzzing and Rigour OOPSLA Vasileios Klimis Queen Mary University of London, Karine Even-Mendoza King’s College London, Avner Bensoussan King's College London, Elena Chachkarova Kings College London, Sophie Fortz King's College London, Connor Lenihan King's College London | ||
10:30 - 12:15 | |||
10:30 15mTalk | FO-Complete Program Verification for Heap Logics OOPSLA Adithya Murali University of Illinois at Urbana-Champaign, Hrishikesh Balakrishnan University of Illinois Urbana-Champaign, Aaron Councilman Univ of Illinois Urbana-Champaign, P. Madhusudan University of Illinois at Urbana-Champaign | ||
10:45 15mTalk | Foundations for Deductive Verification of Continuous Probabilistic Programs: From Lebesgue to Riemann and Back OOPSLA Kevin Batz RWTH Aachen University, Joost-Pieter Katoen RWTH Aachen University, Francesca Randone Department of Mathematics, Informatics and Geosciences, University of Trieste, Italy, Tobias Winkler RWTH Aachen University | ||
11:00 15mTalk | Guarding the Privacy of Label-Only Access to Neural Network Classifiers via Formal Verification OOPSLA | ||
11:15 15mTalk | KestRel: Relational Verification Using E-Graphs for Program Alignment OOPSLA Robert Dickerson Purdue University, Prasita Mukherjee Purdue University, Benjamin Delaware Purdue University | ||
11:30 15mTalk | Laurel: Unblocking Automated Verification with Large Language Models OOPSLA Eric Mugnier University of California San Diego, Emmanuel Anaya Gonzalez UCSD, Nadia Polikarpova University of California at San Diego, Ranjit Jhala University of California at San Diego, Zhou Yuanyuan UCSD | ||
11:45 15mTalk | Scaling Instruction-Selection Verification against Authoritative ISA Semantics OOPSLA Michael McLoughlin Carnegie Mellon University, Ashley Sheng Wellesley College, Chris Fallin F5, Bryan Parno Carnegie Mellon University, Fraser Brown CMU, Alexa VanHattum Wellesley College | ||
12:00 15mTalk | Verification of Bit-Flip Attacks against Quantized Neural Networks OOPSLA Yedi Zhang National University of Singapore, Lei Huang ShanghaiTech University, Pengfei Gao ByteDance, Fu Song Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences; Nanjing Institute of Software Technology, Jun Sun Singapore Management University, Jin Song Dong National University of Singapore | ||
13:45 - 15:30 | |||
13:45 15mTalk | 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 15mTalk | Destination calculus: A linear λ-calculus for purely functional memory writes OOPSLA | ||
14:15 15mTalk | Divining Profiler Accuracy: An Approach to Approximate Profiler Accuracy Through Machine Code-Level Slowdown OOPSLA | ||
14:30 15mTalk | 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 15mTalk | im2im: Automatically Converting In-Memory Image Representations using A Knowledge Graph Approach OOPSLA Fei Chen German Research Center for Artificial Intelligence (DFKI), Saarland University, 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 15mTalk | 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 15mTalk | 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 | ||
13:45 - 15:30 | |||
13:45 15mTalk | Tunneling Through the Hill: Multi-Way Intersection for Version-Space Algebras in Program Synthesis OOPSLA Guanlin Chen Peking University, Ruyi Ji Peking University, Shuhao Zhang Peking University, Yingfei Xiong Peking University | ||
14:00 15mTalk | Language-Parametric Reference Synthesis OOPSLA Daniel A. A. Pelsmaeker Delft University of Technology, Netherlands, Aron Zwaan Delft University of Technology, Casper Bach University of Southern Denmark, Arjan J. Mooij Zürich University of Applied Sciences | ||
14:15 15mTalk | Multi-Modal Sketch-based Behavior Tree Synthesis OOPSLA Wenmeng Zhang College of Computer Science and Technology, National University of Defense Technology, Changsha, China, Zhenbang Chen College of Computer, National University of Defense Technology, Weijiang Hong National University of Defense Technology, Changsha, China | ||
14:30 15mTalk | Synthesizing DSLs for Few-Shot Learning OOPSLA Paul Krogmeier University of Illinois at Urbana-Champaign, P. Madhusudan University of Illinois at Urbana-Champaign | ||
14:45 15mTalk | Synthesizing Implication Lemmas for Interactive Theorem Proving OOPSLA Ana Brendel University of California Los Angeles, Aishwarya Sivaraman Meta, Todd Millstein University of California at Los Angeles | ||
15:00 15mTalk | Synthesizing Sound and Precise Abstract Transformers for Nonlinear Hyperbolic PDE Solvers OOPSLA Jacob Laurel Georgia Institute of Technology, Ignacio Laguna Lawrence Livermore National Laboratory, Jan Hueckelheim Argonne National Laboratory | ||
15:15 15mTalk | UTFix: Change Aware Unit Test Repairing using LLM OOPSLA Shanto Rahman The University of Texas at Austin, Sachit Kuhar Amazon Web Services, Berk Cirisci Amazon Web Services, Pranav Garg AWS, Shiqi Wang AWS AI Labs, Xiaofei Ma AWS AI Labs, Anoop Deoras AWS AI Labs, Baishakhi Ray Columbia University | ||
13:45 - 15:30 | |||
13:45 15mTalk | Adaptive Shielding via Parametric Safety Proofs OOPSLA Yao Feng Tsinghua University, Jun Zhu Nankai University, André Platzer Karlsruhe Institute of Technology (KIT), Jonathan Laurent Carnegie Mellon University / Karlsruhe Institute of Technology | ||
14:00 15mTalk | Certified Decision Procedures for Width-Independent Bitvector Predicates OOPSLA Siddharth Bhat University of Cambridge, Leo Stefanesco University of Cambridge, Chris Hughes Independent Researcher, Tobias Grosser University of Cambridge | ||
14:15 15mTalk | Checking $\delta$-Satisfiability of Reals with Integrals OOPSLA Cody Rivera University of Illinois, Urbana-Champaign, Bishnu Bhusal University of Missouri, Rohit Chadha University of Missouri, A. Prasad Sistla University of Illinois at Chicago, Mahesh Viswanathan University of Illinois at Urbana-Champaign | ||
14:30 15mTalk | Coinductive Proofs of Regular Expression Equivalence in Zero Knowledge OOPSLA John C. Kolesar Yale University, Shan Ali Yale University, Timos Antonopoulos Yale University, Ruzica Piskac Yale University | ||
14:45 15mTalk | Incremental Certified Programming OOPSLA Tomás Diaz University of Chile, Kenji Maillard Inria – LS2N, Université de Nantes, Nicolas Tabareau Inria, Éric Tanter University of Chile | ||
15:00 15mTalk | Pathological Cases for a Class of Reachability-Based Garbage Collectors OOPSLA Matthew Sotoudeh Stanford University Link to publication | ||
15:15 15mTalk | SafeTree: Expressive Tree Policies for Microservices OOPSLA | ||
16:00 - 17:30 | |||
16:00 15mTalk | A Refinement Methodology for Distributed Programs in Rust OOPSLA | ||
16:15 15mTalk | AutoVerus: Automated Proof Generation for Rust Code OOPSLA Chenyuan Yang University of Illinois Urbana-Champaign, Xuheng Li Columbia University, Md Rakib Hossain Misu University of California Irvine, Jianan Yao University of Toronto, Weidong Cui Microsoft Research, Yeyun Gong Microsoft Research, Chris Hawblitzel Microsoft Research, Shuvendu K. Lahiri Microsoft Research, Jacob R. Lorch Microsoft Research, n.n., Shuai Lu Microsoft Research, Fan Yang Microsoft Research Asia, Ziqiao Zhou Microsoft Research, Shan Lu Microsoft; University of Chicago | ||
16:30 15mTalk | Carapace: Static–Dynamic Information Flow Control in Rust OOPSLA Vincent James Beardsley , Chris Xiong Ohio State University, Ada Lamba Ohio State University, Michael D. Bond Ohio State University | ||
16:45 15mTalk | From Linearity to Borrowing OOPSLA Andrew Wagner Northeastern University, Olek Gierczak Northeastern University, Brianna Marshall Northeastern University, John Li Northeastern University, Amal Ahmed Northeastern University, USA | ||
17:00 15mTalk | Garbage Collection for Rust: The Finalizer Frontier OOPSLA | ||
17:15 15mTalk | Place Capability Graphs: A General-Purpose Model of Rust’s Ownership and Borrowing Guarantees OOPSLA Zachary Grannan University of British Columbia, Aurel Bílý ETH Zurich, Jonas Fiala ETH Zürich, Jasper Geer University of British Columbia, Markus de Medeiros New York University, Peter Müller ETH Zurich, Alexander J. Summers University of British Columbia | ||
16:00 - 17:30 | |||
16:00 15mTalk | (TOPLAS) Polynomial Bounds of CFLOBDDs against BDDs OOPSLA DOI | ||
16:15 15mTalk | (TOPLAS) Type-Safe Compilation of Dynamic Inheritance via Merging OOPSLA Yaozhu Sun National Institute of Informatics, Xuejing Huang IRIF, Bruno C. d. S. Oliveira University of Hong Kong | ||
16:30 15mTalk | Detecting and explaining (in-)equivalence of context-free grammars OOPSLA Marko Schmellenkamp Ruhr University Bochum, Thomas Zeume Ruhr University Bochum, Sven Argo Ruhr University Bochum, Sandra Kiefer University of Oxford, Cedric Siems Ruhr University Bochum, Fynn Stebel Ruhr University Bochum | ||
16:45 15mTalk | Modal Abstractions for Virtualizing Memory Addresses OOPSLA | ||
17:00 15mTalk | Agora: Trust Less and Open More in Verification for Confidential Computing OOPSLA Hongbo Chen Indiana University Bloomington, Quan Zhou Penn State University, Sen Yang Yale University, Dang Sixuan Duke University, Xing Han The Hong Kong University of Science and Technology, Danfeng Zhang Duke University, Fan Zhang Yale University, XiaoFeng Wang Nanyang Technological University | ||
17:15 15mTalk | QED in Context: An Observation Study of Proof Assistant Users OOPSLA Jessica Shi University of Pennsylvania, Cassia Torczon University of Pennsylvania, Harrison Goldstein University at Buffalo, the State University of New York at Buffalo, Benjamin C. Pierce University of Pennsylvania, Andrew Head University of Pennsylvania | ||
16:00 - 17:30 | |||
16:00 15mTalk | Products of Recursive Programs for Hypersafety Verification OOPSLA | ||
16:15 15mTalk | Embedding Quantum Program Verification into Dafny OOPSLA Feifei Cheng Iowa State University, Sushen Vangeepuram Iowa State University, Henry Allard Iowa State University, Seyed Mohammad Reza Jafari Iowa State University, Alex Potanin Australian National University, Liyi Li Iowa State University | ||
16:30 15mTalk | Faster Explicit-Trace Monitoring-Oriented Programming for Runtime Verification of Software Tests OOPSLA Kevin Guan Cornell University, Marcelo d'Amorim North Carolina State University, Owolabi Legunsen Cornell University | ||
16:45 15mTalk | Interactive Bit Vector Reasoning using Verified Bitblasting OOPSLA Henrik Böving Lean FRO, Siddharth Bhat University of Cambridge, Alex Keizer University of Cambridge, Luisa Cicolini University of Cambridge, Leon Frenot ENS Lyon, Abdalrhman Mohamed Stanford University, Leo Stefanesco University of Cambridge, Harun Khan Stanford University, Josh Clune Carnegie Mellon University, Clark Barrett Stanford University, Tobias Grosser University of Cambridge | ||