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 SPLASH 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 SPLASH 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 SPLASH 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 SPLASH 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 SPLASH 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 SPLASH 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 SPLASH 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 SPLASH OOPSLA | ||
11:00 15mTalk | Boosting Program Reduction with the Missing Piece of Syntax-Guided Transformations SPLASH 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 SPLASH OOPSLA | ||
11:30 15mTalk | Enhancing APR with PRISM: A Semantic-Based Approach to Overfitting Patch Detection SPLASH OOPSLA | ||
11:45 15mTalk | PAFL: Enhancing Fault Localizers by Leveraging Project-Specific Fault Patterns SPLASH OOPSLA | ||
12:00 15mTalk | Stencil-Lifting: Hierarchical Recursive Lifting System for Extracting Summary of Stencil Kernel in Legacy Codes SPLASH OOPSLA Mingyi Li Institute of Computing Technology, CAS, 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 SPLASH 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 SPLASH 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 SPLASH 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 SPLASH 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 SPLASH 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 SPLASH 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 SPLASH 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 SPLASH 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 SPLASH 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 SPLASH 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 SPLASH 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 SPLASH 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 SPLASH 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 SPLASH 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 SPLASH OOPSLA | ||
16:45 15mTalk | Lilo: A Higher-Order, Relational Concurrent Separation Logic for Liveness SPLASH 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 SPLASH 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 SPLASH 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 SPLASH 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 SPLASH 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 SPLASH OOPSLA Pre-print | ||
11:15 15mTalk | Denotational Foundations for Expected Cost Analysis SPLASH OOPSLA Pedro Henrique Azevedo de Amorim Cornell University | ||
11:30 15mTalk | IncIDFA: An Efficient and Generic Algorithm for Incremental Iterative Dataflow Analysis SPLASH OOPSLA | ||
11:45 15mTalk | Revealing Sources of (Memory) Errors via Backward Analysis SPLASH 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 SPLASH 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 | Syntactic Completions with Material Obligations SPLASH 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:45 15mTalk | REPTILE: Performant Tiling of Recurrences SPLASH 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 SPLASH 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 SPLASH OOPSLA | ||
11:30 15mTalk | Static Inference of Regular Grammars for Ad Hoc Parsers SPLASH OOPSLA Pre-print | ||
10:30 - 12:15 | |||
10:30 15mTalk | Fast Client-Driven CFL-Reachability via Regularization-Based Graph Simplification SPLASH 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 SPLASH 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 SPLASH 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 SPLASH 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 SPLASH 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 SPLASH 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 SPLASH OOPSLA | ||
14:00 15mTalk | Fray: An Efficient General-Purpose Concurrency Testing Platform for the JVM SPLASH 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 SPLASH 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 SPLASH OOPSLA | ||
14:45 15mTalk | Model-guided Fuzzing of Distributed Systems SPLASH 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 SPLASH 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 SPLASH 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 SPLASH 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 SPLASH OOPSLA Alex Kavvos University of Bristol | ||
14:15 15mTalk | A Mechanized Semantics for Dataflow Circuits SPLASH 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 SPLASH 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 SPLASH 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 SPLASH 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 SPLASH 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 | A Flow-Sensitive Refinement Type System for Verifying eBPF Programs SPLASH 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 15mTalk | Automatically Verifying Replication-aware Linearizability SPLASH OOPSLA Vimala Soundarapandian IIT Madras, Kartik Nagar IIT Madras, Aseem Rastogi Microsoft Research, KC Sivaramakrishnan IIT Madras and Tarides | ||
16:30 15mTalk | On the Impact of Formal Verification on Software Development SPLASH 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 15mTalk | Towards Verifying Crash Consistency SPLASH OOPSLA Keonho Lee University of California, Irvine, Conan Truong University of California, Irvine, Brian Demsky University of California at Irvine | ||
17:00 15mTalk | TraceLinking Implementations with their Verified Designs SPLASH OOPSLA Pre-print | ||
17:15 15mTalk | Pyrosome: Verified Compilation for Modular Metatheory SPLASH OOPSLA | ||
16:00 - 17:30 | |||
16:00 15mTalk | Bennet: Randomized Specification Testing for Heap-Manipulating Programs SPLASH OOPSLA | ||
16:15 15mTalk | DepFuzz: Efficient Smart Contract Fuzzing with Function Dependence Guidance SPLASH 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 SPLASH 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 SPLASH 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 SPLASH OOPSLA | ||
16:00 - 17:30 | |||
16:00 15mTalk | Debugging WebAssembly? Put some Whamm on it! SPLASH 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 SPLASH 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 SPLASH 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 SPLASH 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 SPLASH 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 SPLASH 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) SPLASH 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 SPLASH 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 SPLASH 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 SPLASH OOPSLA Sam Stites Northeastern University, John Li Northeastern University, Steven Holtzen Northeastern University | ||
17:00 15mTalk | Polymorphic Records for Dynamic Languages SPLASH OOPSLA | ||
17:30 - 18:15 | |||
17:30 15mAwards | SPLASH Awards SPLASH 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 SPLASH 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 SPLASH 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 SPLASH 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 SPLASH 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 SPLASH 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 SPLASH OOPSLA Pre-print | ||
12:00 15mTalk | We’ve Got You Covered: Type-Guided Repair of Incomplete Input Generators SPLASH 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 SPLASH 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 SPLASH 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 SPLASH OOPSLA | ||
11:15 15mTalk | Hambazi: Spatial Coordination Synthesis for Augmented Reality SPLASH 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 SPLASH OOPSLA | ||
11:45 15mTalk | LOUD: Synthesizing Strongest and Weakest Specifications SPLASH 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 SPLASH 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 SPLASH 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 SPLASH 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 SPLASH 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 SPLASH 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 SPLASH OOPSLA | ||
11:45 15mTalk | qblaze: An Efficient and Scalable Sparse Quantum Simulator SPLASH 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 SPLASH 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 SPLASH 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 SPLASH 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 SPLASH OOPSLA | ||
11:15 15mTalk | KestRel: Relational Verification Using E-Graphs for Program Alignment SPLASH OOPSLA Robert Dickerson Purdue University, Prasita Mukherjee Purdue University, Benjamin Delaware Purdue University | ||
11:30 15mTalk | Laurel: Unblocking Automated Verification with Large Language Models SPLASH 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 SPLASH 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 SPLASH 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 SPLASH 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 SPLASH OOPSLA | ||
14:15 15mTalk | Divining Profiler Accuracy: An Approach to Approximate Profiler Accuracy Through Machine Code-Level Slowdown SPLASH OOPSLA DOI | ||
14:30 15mTalk | HeapBuffers: Why not just using a binary serialization format for your managed memory? SPLASH 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 SPLASH 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 SPLASH 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 SPLASH 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 SPLASH OOPSLA Guanlin Chen Peking University, Ruyi Ji Peking University, Shuhao Zhang Peking University, Yingfei Xiong Peking University | ||
14:00 15mTalk | Language-Parametric Reference Synthesis SPLASH 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 SPLASH 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 SPLASH 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 SPLASH 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 SPLASH 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 SPLASH 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 SPLASH 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 SPLASH 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 SPLASH 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 SPLASH OOPSLA John C. Kolesar Yale University, Shan Ali Yale University, Timos Antonopoulos Yale University, Ruzica Piskac Yale University | ||
14:45 15mTalk | Incremental Certified Programming SPLASH 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 SPLASH OOPSLA Matthew Sotoudeh Stanford University Link to publication | ||
15:15 15mTalk | SafeTree: Expressive Tree Policies for Microservices SPLASH OOPSLA | ||
13:45 - 15:30 | |||
13:45 15mTalk | Automated Verification of Soundness of DNN Certifiers SPLASH OOPSLA Avaljot Singh UIUC, Yasmin Chandini Sarita UIUC, Charith Mendis University of Illinois at Urbana-Champaign, Gagandeep Singh University of Illinois at Urbana-Champaign; VMware Research | ||
14:00 15mTalk | Bolt-On Strong Consistency: Specification, Implementation, and Verification SPLASH OOPSLA Nicholas V. Lewchenko University of Colorado Boulder, Gowtham Kaki University of Colorado at Boulder, Bor-Yuh Evan Chang University of Colorado Boulder & Amazon | ||
14:15 15mTalk | Memory-Safety Verification of Open Programs With Angelic Assumptions SPLASH OOPSLA Gourav Takhar Indian Institute of Technology - Kanpur, Baldip Bijlani Indian Institute of Technology Kanpur, Prantik Chatterjee MathWorks, Akash Lal Microsoft Research, Subhajit Roy IIT Kanpur | ||
14:30 15mTalk | Mini-Batch Robustness Verification of Deep Neural Networks SPLASH OOPSLA | ||
14:45 15mTalk | Revamping Verilog Semantics for Foundational Verification SPLASH OOPSLA | ||
15:00 15mTalk | Scalable Equivalence Checking and Verification of Shallow Quantum Circuits SPLASH OOPSLA Nengkun Yu Stony Brook University, USA, Xuan Du Trinh Stony Brook University, Thomas Reps University of Wisconsin-Madison | ||
15:15 15mTalk | Structural temporal logic for mechanized program verification SPLASH OOPSLA Lef Ioannidis University of Pennsylvania, Yannick Zakowski Inria, Steve Zdancewic University of Pennsylvania, Sebastian Angel University of Pennsylvania | ||
16:00 - 17:30 | |||
16:00 15mTalk | Abstract Interpretation of Temporal Safety Effects of Higher Order Programs SPLASH 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 15mTalk | A Hoare Logic For Symmetry Properties SPLASH OOPSLA | ||
16:30 15mTalk | Efficient Abstract Interpretation via Selective Widening SPLASH OOPSLA | ||
16:45 15mTalk | Encode the $\forall\exists$ Relational Hoare Logic into Standard Hoare Logic SPLASH OOPSLA Shushu Wu Shanghai Jiao Tong University, Xiwei Wu Shanghai Jiao Tong University, Qinxiang Cao Shanghai Jiao Tong University | ||
17:00 15mTalk | Structural Abstraction and Refinement for Probabilistic Programs SPLASH 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 15mTalk | Work Packets: A New Abstraction for GC Software Engineering, Optimization, and Innovation SPLASH OOPSLA Wenyu Zhao Australian National University, Stephen M. Blackburn Google; Australian National University, Kathryn S McKinley Google | ||
16:00 - 17:30 | |||
16:00 15mTalk | A Refinement Methodology for Distributed Programs in Rust SPLASH OOPSLA | ||
16:15 15mTalk | AutoVerus: Automated Proof Generation for Rust Code SPLASH 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 SPLASH 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 SPLASH 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 SPLASH OOPSLA | ||
17:15 15mTalk | Place Capability Graphs: A General-Purpose Model of Rust’s Ownership and Borrowing Guarantees SPLASH 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 SPLASH OOPSLA DOI | ||
16:15 15mTalk | (TOPLAS) Type-Safe Compilation of Dynamic Inheritance via Merging SPLASH 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 SPLASH 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 SPLASH OOPSLA | ||
17:00 15mTalk | Agora: Trust Less and Open More in Verification for Confidential Computing SPLASH 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 SPLASH 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 SPLASH OOPSLA | ||
16:15 15mTalk | Embedding Quantum Program Verification into Dafny SPLASH 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 SPLASH 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 SPLASH 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 | ||