Program - SPLASH 2025

Detailed Table Session Timeline Detailed Timeline

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

Sun 12 Oct
Displayed time zone: Perth change


Room	9:00	15		30	45	10:00		15	30	45	11:00	15		30	45	12:00	15	30	45	13:00	15	30	45	14:00	15		30	45	15:00	15	30	45	16:00	15	30	45	17:00	15	30	45	18:00	15	30	45	19:00	15	30	45	20:00	15	30	45
COM1 Level 2 Foyer									ICFP/SPLASH Catering Break 10:30 - 11:00									ICFP/SPLASH Catering Lunch 12:30 - 14:00													ICFP/SPLASH Catering Break 15:30 - 16:00
Concert Hall																										SPLASH FARM Computers & Music AND Computer Music— An Unlikely [Ongoing] Journey 19:00 - 21:00 Concert: Merzmania 19:00 - 21:00 Concert: Mitosis 19:00 - 21:00 Concert: Sonic Earth 19:00 - 21:00 Concert: Girard’s Paradox 19:00 - 21:00 Concert: RocqNRoll 19:00 - 21:00 Concert: Mirages 19:00 - 21:00 Concert: False Awakening on a Mediterranean Island 19:00 - 21:00 Concert: The River Oycus 19:00 - 21:00
Seminar Room 10	ICFP/SPLASH Tutorials WebAssembly Research Tools Tutorial 09:00 - 10:30										ICFP/SPLASH Tutorials WebAssembly Research Tools Tutorial 11:00 - 12:30													ICFP/SPLASH Tutorials A guided tour through Oxidized OCaml 14:00 - 15:30									ICFP/SPLASH Tutorials A guided tour through Oxidized OCaml 16:00 - 17:30
Seminar Room 5	ICFP/SPLASH Tutorials Testing concurrent code on JVM with Lincheck 09:00 - 10:30										ICFP/SPLASH Tutorials Testing concurrent code on JVM with Lincheck 11:00 - 12:30													ICFP/SPLASH Tutorials Concurrent Algorithms under the hood of Kotlin Coroutines 14:00 - 15:30									ICFP/SPLASH Tutorials Concurrent Algorithms under the hood of Kotlin Coroutines 16:00 - 17:30
Seminar Room 6	ICFP/SPLASH Tutorials Compiling Quantum Circuits 09:00 - 10:30										ICFP/SPLASH Tutorials Compiling Quantum Circuits 11:00 - 12:30													ICFP/SPLASH Tutorials End-to-End Compiler Infrastructure for Emerging Tensor Accelerators 14:00 - 15:30									ICFP/SPLASH Tutorials End-to-End Compiler Infrastructure for Emerging Tensor Accelerators 16:00 - 17:30
Seminar Room 9	ICFP/SPLASH Tutorials Metaprogramming in Rhombus 09:00 - 10:30										ICFP/SPLASH Tutorials Metaprogramming in Rhombus 11:00 - 12:30													ICFP/SPLASH Tutorials How to secure a distributed database such as OpenRiak with open-source ... 14:00 - 15:30									ICFP/SPLASH Tutorials How to secure a distributed database such as OpenRiak with open-source ... 16:00 - 17:30
Video Conference Room (VCR)	SPLASH FARM Type-safe Blazon - Enforcing Pedantry in Heraldic Design 09:00 - 09:22		SPLASH FARM How to Score in the Art Racket 09:22 - 09:45		SPLASH FARM Rocq N'Roll 09:45 - 10:07		SPLASH FARM I Am Your Co-Pilot 10:07 - 10:30				SPLASH FARM Cellular Automata as a Model For 1-bit Synthesis in Mitosis 11:00 - 11:22		SPLASH FARM Girard's Paradox as Structure Music 11:22 - 11:45		SPLASH FARM Sonic Earth - An Algorithmic Performance Approach to Real-Time Environm ... 11:45 - 12:20									SPLASH FARM Weft—Enabling Tidal on the Web 14:00 - 14:22		SPLASH FARM Generalizing Turtle Geometry: An Extensible Language for Vector Graphic ... 14:22 - 14:44		SPLASH FARM Software-defined declarative synthesizer live-coding in a jupyter notebook 14:44 - 15:07

Mon 13 Oct
Displayed time zone: Perth change


Room	9:00			15	30	45	10:00		15	30	45		11:00		15	30			45	12:00		15	30	45	13:00	15	30		45	14:00		15		30		45			15:00	15		30	45	16:00	15			30		45		17:00	15		30	45	18:00	15	30	45	19:00	15	30	45
Garden Walk																																	ICFP Student Research Competition ICFP SRC Poster Session 18:00 - 20:00
Orchid Dining Hall								ICFP/SPLASH Catering Break 10:10 - 10:50													ICFP/SPLASH Catering Lunch 12:10 - 13:40																				ICFP/SPLASH Catering Break 15:20 - 16:00
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
Orchid Plenary Ballroom	ICFP Papers Opening 09:00 - 09:05	ICFP Papers JFP Announcement 09:05 - 09:10	ICFP Keynotes Functional Programming for Hardware Design 09:10 - 10:10									ICFP Papers 2-Functoriality of Initial Semantics, and Applications 10:50 - 11:15			ICFP Papers Bialgebraic Reasoning on Stateful Languages 11:15 - 11:40			ICFP Papers Frex: Dependently Typed Algebraic Simplification 11:40 - 12:05										ICFP PapersDistinguished Paper Call-Guarded Abstract Definitional Interpreters 13:40 - 14:05			ICFP PapersDistinguished Paper Effectful Lenses: There and Back with Different Monads 14:05 - 14:30			ICFP PapersDistinguished Paper First-Order Laziness 14:30 - 14:55				ICFP PapersDistinguished Paper Multi-stage Programming with Splice Variables 14:55 - 15:20						ICFP Papers Pushing the Information-Theoretic Limits of Random Access Lists 16:00 - 16:25			ICFP Papers Truly Functional Solutions to the Longest Uptrend Problem (Functional P ... 16:25 - 16:50				ICFP JFP First Papers Bottom-up computation using trees of sublists 16:50 - 17:15		ICFP JFP First PapersRemote You could have invented Fenwick trees 17:15 - 17:40
Orchid West												ICFP Papers Environment-Sharing Analysis and Caller-Provided Environments for Highe ... 10:50 - 11:15			ICFP Papers Multiple Resumptions and Local Mutable State, Directly 11:15 - 11:40			ICFP JFP First Papers OCaml Blockly 11:40 - 12:05																										ICFP JFP First Papers A contextual formalization of structural coinduction 16:00 - 16:25			ICFP JFP First Papers A practical formalization of monadic equational reasoning in dependent- ... 16:25 - 16:50				ICFP Papers Almost Fair Simulations 16:50 - 17:15		ICFP Papers Big Steps in Higher-Order Mathematical Operational Semantics 17:15 - 17:40
Peony SE												SPLASH Doctoral Symposium Introductions 10:50 - 10:55	SPLASH Doctoral Symposium A Multi-Layer Dynamic Security Framework for DeFi Smart Contracts 11:00 - 11:30				SPLASH Doctoral Symposium Lexical Effect Handler: Fast by Design, Correct by Proof 11:35 - 12:05											SPLASH Doctoral Symposium How to Synthesize Quantum-Circuit Optimizers 13:40 - 14:10				SPLASH Doctoral Symposium Separation Logics for Probability, Concurrency, and Security 14:15 - 14:45					SPLASH Doctoral Symposium Towards Compiler-Guided Static Analysis 14:50 - 15:20							SPLASH Doctoral Symposium Practical compositional diagramming 16:00 - 16:30				SPLASH Doctoral Symposium [Closed Session] Adjudication meeting for SIGPLAN's John Vlissides award 16:30 - 17:20						SPLASH Doctoral Symposium First announcement of SIGPLAN's John Vlissides award; Closing Remarks 17:20 - 17:40

Tue 14 Oct
Displayed time zone: Perth change


Room	9:00	15	30	45	10:00		15	30	45		11:00	15	30		45	12:00		15	30	45	13:00	15	30		45	14:00		15	30		45		15:00	15		30	45	16:00	15		30			45		17:00		15		30	45
Orchid Dining Hall						ICFP/SPLASH Catering Break 10:10 - 10:50											ICFP/SPLASH Catering Lunch 12:10 - 13:40																		ICFP/SPLASH Catering Break 15:20 - 16:00
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
Orchid Plenary Ballroom	ICFP Keynotes The Rational Programmer, A Method for Investigating Programming Languag ... 09:00 - 10:10									ICFP Papers Robust Dynamic Embedding for Gradual Typing 10:50 - 11:15		ICFP JFP First Papers A simple blame calculus for explicit nulls 11:15 - 11:40		ICFP Papers SecRef*: Securely Sharing Mutable References between Verified and Unver ... 11:40 - 12:05										ICFP Papers Fulls Seldom Differ 13:40 - 14:05			ICFP Papers Normalization by Evaluation for Non-cumulativity 14:05 - 14:30		ICFP Papers Type Theory in Type Theory using a Strictified Syntax 14:30 - 14:55			ICFP Papers Type Universes as Kripke Worlds 14:55 - 15:20						ICFP Papers ICFP Contest Report 16:00 - 16:15	ICFP Papers Award Ceremony 16:15 - 16:35			ICFP Student Research Competition SRC Awards 16:35 - 16:45		ICFP Papers SIGPLAN AV Report 16:45 - 16:55	ICFP Papers PC Chair Report 16:55 - 17:10		ICFP Papers General Chair Report 17:10 - 17:20		ICFP Papers ICFP 2026 Announcement 17:20 - 17:30
Orchid West										ICFP Papers Compiling with Generating Functions 10:50 - 11:15		ICFP PapersRemote Correctness Meets Performance: From Agda to Futhark 11:15 - 11:40		ICFP JFP First Papers Domain-specific tensor languages 11:40 - 12:05										ICFP Papers A Haskell Adiabatic DSL: Solving Classical Optimization Problems on Qua ... 13:40 - 14:05			ICFP Papers Functional Networking for Millions of Docker Desktops (Experience Report) 14:05 - 14:30		ICFP Papers Polynomial-Time Program Equivalence for Machine Knitting 14:30 - 14:55			ICFP Student Research Competition SRC Talks 14:55 - 15:25

Wed 15 Oct
Displayed time zone: Perth change


Room	9:00	15	30	45	10:00		15	30	45		11:00	15	30		45	12:00		15	30	45	13:00	15	30		45	14:00		15	30	45		15:00	15		30	45
Orchid Dining Hall						ICFP/SPLASH Catering Break 10:10 - 10:50											ICFP/SPLASH Catering Lunch 12:10 - 13:40																	ICFP/SPLASH Catering Break 15:20 - 16:00
Orchid Plenary Ballroom	ICFP Keynotes Proof-Carrying Neuro-Symbolic Code 09:00 - 10:10									ICFP Papers A Bargain for Mergesorts: How to Prove Your Mergesort Correct and Stabl ... 10:50 - 11:15		ICFP Papers CRDT Emulation, Simulation, and Representation Independence 11:15 - 11:40		ICFP JFP First Papers How much is in a square? Calculating functional programs with squares 11:40 - 12:05										ICFP Papers Formal Semantics and Program Logics for a Fragment of OCaml 13:40 - 14:05			ICFP Papers Verified Interpreters for Dynamic Languages with Applications to the Ni ... 14:05 - 14:30		ICFP Papers Verifying Graph Algorithms in Separation Logic: A Case for an Algebraic ... 14:30 - 14:55		ICFP Papers Reasoning about Weak Isolation Levels in Separation Logic 14:55 - 15:20
Orchid West										ICFP Papers Fusing Session-Typed Concurrent Programming into Functional Programming 10:50 - 11:15		ICFP Papers Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs 11:15 - 11:40		ICFP Papers Relax! The Semilenient Core of Choreographic Programming (Functional Pearl) 11:40 - 12:05										ICFP Papers McTT: A Verified Kernel for a Proof Assistant 13:40 - 14:05			ICFP PapersRemote Linear Types with Dynamic Multiplicities in Dependent Type Theory (Func ... 14:05 - 14:30		ICFP JFP First Papers Binary search—think positive 14:30 - 14:55		ICFP Papers Teaching Software Specification (Experience Report) 14:55 - 15:20

Thu 16 Oct
Displayed time zone: Perth change


Room	9:00	15	30	45	10:00	15	30		45	11:00		15	30		45	12:00	15	30	45	13:00	15	30	45	14:00	15			30	45	15:00	15	30	45	16:00	15	30	45	17:00	15	30	45	18:00	15	30	45	19:00	15	30	45
Garden Walk																										SPLASH Student Research Competition SPLASH SRC Poster Session 18:00 - 20:00
Orchid Dining Hall					ICFP/SPLASH Catering Break 10:00 - 10:30												ICFP/SPLASH Catering Lunch 12:15 - 13:45															ICFP/SPLASH Catering Break 15:30 - 16:00										SPLASH Posters Toward Automated Verification of Static Analysis Results of Android App ... 18:00 - 20:00 Existentialize your Generics 18:00 - 20:00 View Types in Rust 18:00 - 20:00 Simplifying Lifter-generated Emulation Style LLVM IR for Analysis Suita ... 18:00 - 20:00 Verifying Extract Method Refactoring in Rust 18:00 - 20:00 Reproducibility Debt in Scientific Software 18:00 - 20:00 Lemma Discovery for Inductive Equational Proofs via Recursive Function ... 18:00 - 20:00 Logically Qualified Types for Scala 18:00 - 20:00 Incremental and Unbounded Loop Analysis 18:00 - 20:00 Type Checking for Python Using Intersection Types 18:00 - 20:00 Current Practices for Building LLM-Powered Reasoning Tools Are Ad Hoc—a ... 18:00 - 20:00
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
Orchid Plenary Ballroom	SPLASH Keynotes Automating maintenance of the Linux kernel: a perspective over 20 years 09:00 - 10:00						SPLASH OOPSLA ABC: Towards a Universal Code Styler through Model Merging 10:30 - 10:45		SPLASH OOPSLA Binary Cryptographic Function Identification via Similarity Analysis wi ... 10:45 - 11:00	SPLASH OOPSLA Boosting Program Reduction with the Missing Piece of Syntax-Guided Tran ... 11:00 - 11:15		SPLASH OOPSLA Code Style Sheets: CSS for Code 11:15 - 11:30	SPLASH OOPSLA Enhancing APR with PRISM: A Semantic-Based Approach to Overfitting Patc ... 11:30 - 11:45		SPLASH OOPSLA PAFL: Enhancing Fault Localizers by Leveraging Project-Specific Fault P ... 11:45 - 12:00	SPLASH OOPSLA Stencil-Lifting: Hierarchical Recursive Lifting System for Extracting S ... 12:00 - 12:15							SPLASH OOPSLA A Unifying Approach to Product Constructions for Quantitative Temporal ... 13:45 - 14:00	SPLASH OOPSLA Contract System Metatheories à la Carte: A Transition-System View of C ... 14:00 - 14:15	SPLASH OOPSLA Incremental Bidirectional Typing via Order Maintenance 14:15 - 14:30			SPLASH OOPSLA The Power of Regular Constraint Propagation 14:30 - 14:45	SPLASH OOPSLA Orax: A Feedback-Driven Framework for Efficiently Solving Satisfiabilit ... 14:45 - 15:00	SPLASH OOPSLA Software Model Checking via Summary-Guided Search 15:00 - 15:15				SPLASH OOPSLA Compressed and Parallelized Structured Tensor Algebra 16:00 - 16:15	SPLASH OOPSLA Exploring the Theory and Practice of Concurrency in the Entity-Componen ... 16:15 - 16:30	SPLASH OOPSLA HieraSynth: A Parallel Framework for Complete Super-Optimization with H ... 16:30 - 16:45	SPLASH OOPSLA Lilo: A Higher-Order, Relational Concurrent Separation Logic for Liveness 16:45 - 17:00	SPLASH OOPSLA Opportunistically Parallel Lambda Calculus 17:00 - 17:15	SPLASH OOPSLA Soundness of Predictive Concurrency Analyses 17:15 - 17:30
Orchid West							SPLASH OOPSLA Automated Discovery of Tactic Libraries for Interactive Theorem Proving 10:30 - 10:45		SPLASH OOPSLA Choreographic Quick Changes: First-Class Location (Set) Polymorphism 10:45 - 11:00	SPLASH OOPSLA Divide and Conquer: A Compositional Approach to Game-Theoretic Security 11:00 - 11:15		SPLASH OOPSLA Efficient Decrease-And-Conquer Linearizability Monitoring 11:15 - 11:30	SPLASH OOPSLA Liberating Merges via Apartness and Guarded Subtyping 11:30 - 11:45		SPLASH OOPSLA The Simple Essence of Monomorphization 11:45 - 12:00	SPLASH OOPSLA What's in the Box: Ergonomic and Expressive Capture Tracking over Gener ... 12:00 - 12:15							SPLASH OOPSLA Characterizing Implementability of Global Protocols with Infinite State ... 13:45 - 14:00	SPLASH OOPSLA Checking Observational Correctness of Database Systems 14:00 - 14:15	SPLASH OOPSLA Correct Black-Box Monitors for Distributed Deadlock Detection: Formalis ... 14:15 - 14:30			SPLASH OOPSLA Correct-By-Construction: Certified Individual Fairness through Neural N ... 14:30 - 14:45	SPLASH OOPSLA Modular Reasoning about Global Variables and Their Initialization 14:45 - 15:00	SPLASH OOPSLA P³: Reasoning about Patches via Product Programs 15:00 - 15:15	SPLASH OOPSLA Reasoning about External Calls 15:15 - 15:30			SPLASH OOPSLA Convex Hull Approximation for Activation Functions 16:00 - 16:15	SPLASH OOPSLA Cost of Soundness in Mixed-Precision Tuning 16:15 - 16:30	SPLASH OOPSLA Finch: Sparse and Structured Tensor Programming with Control Flow 16:30 - 16:45	SPLASH OOPSLA MetaKernel: Enabling Efficient Encrypted Neural Network Inference Throu ... 16:45 - 17:00	SPLASH OOPSLA Quantization with Guaranteed Floating-Point Neural Network Classifications 17:00 - 17:15	SPLASH OOPSLA The Continuous Tensor Abstraction: Where Indices are Real 17:15 - 17:30
Peony SE							SPLASH Onward! Papers Opening 10:30 - 10:40	SPLASH Onward! Papers Sharing is Scaring: Linking Cloud File-Sharing to Programming Language ... 10:40 - 11:10			SPLASH Onward! Papers On Collective Control over User Interfaces in the Face of Network Eﬀects 11:10 - 11:40			SPLASH Onward! Papers Foundational Design Principles and Patterns for Building Robust & Adapt ... 11:40 - 12:10									SPLASH Onward! EssaysRemote The Proof Must Go On: Formal Methods in the Theater of Secure Software ... 13:45 - 14:25				SPLASH Onward! Essays The Unix Executable as a Smalltalk Method 14:25 - 15:05							SPLASH Onward! Papers Semantics-preserving Transformation of Context-free Grammars into LL(1) ... 16:00 - 16:30		SPLASH Onward! Papers An Argument for the Practicality of Entity Component Systems as the Pri ... 16:30 - 17:00		SPLASH Onward! Papers TideScript: A Domain Specific Language for Peptide Chemistry 17:00 - 17:30

Fri 17 Oct
Displayed time zone: Perth change


Room	9:00	15	30	45	10:00	15	30	45	11:00	15	30	45	12:00	15	30	45	13:00	15	30	45	14:00	15		30	45	15:00	15	30	45	16:00	15	30	45	17:00	15	30		45	18:00	15	30	45
Orchid Dining Hall					ICFP/SPLASH Catering Break 10:00 - 10:30									ICFP/SPLASH Catering Lunch 12:15 - 13:45														ICFP/SPLASH Catering Break 15:30 - 16:00
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
Orchid Plenary Ballroom	SPLASH Keynotes The Quest Toward that Perfect Compiler 09:00 - 10:00						SPLASH OOPSLA Syntactic Completions with Material Obligations 10:30 - 10:45	SPLASH OOPSLA REPTILE: Performant Tiling of Recurrences 10:45 - 11:00	SPLASH OOPSLA SPLAT: A framework for optimised GPU code-generation for SParse reguLar ... 11:00 - 11:15	SPLASH OOPSLA Statically Analyzing the Dataflow of R Programs 11:15 - 11:30	SPLASH OOPSLA Static Inference of Regular Grammars for Ad Hoc Parsers 11:30 - 11:45									SPLASH OOPSLA An Empirical Evaluation of Property-Based Testing in Python 13:45 - 14:00	SPLASH OOPSLA Fray: An Efficient General-Purpose Concurrency Testing Platform for the JVM 14:00 - 14:15	SPLASH OOPSLA Fuzzing C++ Compilers via Type-Driven Mutation 14:15 - 14:30		SPLASH OOPSLA Interleaving Large Language Models for Compiler Testing 14:30 - 14:45	SPLASH OOPSLA Model-guided Fuzzing of Distributed Systems 14:45 - 15:00	SPLASH OOPSLA Tuning Random Generators: Property-Based Testing as Probabilistic Progr ... 15:00 - 15:15	SPLASH OOPSLA Understanding and Improving Flaky Test Classification 15:15 - 15:30			SPLASH OOPSLA Bennet: Randomized Specification Testing for Heap-Manipulating Programs 16:00 - 16:15	SPLASH OOPSLA DepFuzz: Efficient Smart Contract Fuzzing with Function Dependence Guidance 16:15 - 16:30	SPLASH OOPSLA Extraction and Mutation at a High Level: Template-Based Fuzzing for Jav ... 16:30 - 16:45	SPLASH OOPSLA Finding Compiler Bugs through Cross-Language Code Generator and Differe ... 16:45 - 17:00	SPLASH OOPSLA Formalizing Linear Motion G-code for Invariant Checking and Differentia ... 17:00 - 17:15		SPLASH OOPSLA OOPSLA Awards 17:30 - 17:40	SPLASH OOPSLA SPLASH Organisers Discussion and AMA 17:40 - 18:15
Orchid Small																				SPLASH OOPSLA A complete formal semantics of eBPF instruction set architecture for Solana 13:45 - 14:00	SPLASH OOPSLA Adequacy for Algebraic Effects Revisited 14:00 - 14:15	SPLASH OOPSLA A Mechanized Semantics for Dataflow Circuits 14:15 - 14:30		SPLASH OOPSLA Dynamic Wind for Effect Handlers 14:30 - 14:45	SPLASH OOPSLA React-tRace: A Semantics for Understanding React Hooks 14:45 - 15:00	SPLASH OOPSLA Semantics of Sets of Programs 15:00 - 15:15	SPLASH OOPSLA Zero-Overhead Lexical Effect Handlers 15:15 - 15:30			SPLASH OOPSLA Debugging WebAssembly? Put some Whamm on it! 16:00 - 16:15	SPLASH OOPSLA MIO: Multiverse Debugging in the face of Input/Output 16:15 - 16:30	SPLASH OOPSLA PReMM: LLM-Based Program Repair for Multi-Method Bugs via Divide and Co ... 16:30 - 16:45	SPLASH OOPSLA Show Me Why It's Correct: Saving 1/3 of Debugging Time in Program Repai ... 16:45 - 17:00	SPLASH OOPSLA Translation Validation for LLVM's AArch64 Backend 17:00 - 17:15	SPLASH OOPSLA Validating SMT Rewriters via Rewrite Space Exploration Supported by Gen ... 17:15 - 17:30
Orchid West							SPLASH OOPSLA Fast Client-Driven CFL-Reachability via Regularization-Based Graph Simp ... 10:30 - 10:45	SPLASH OOPSLA Flexible and Expressive Typed Path Patterns for GQL 10:45 - 11:00	SPLASH OOPSLA Quantified Underapproximation via Labeled Bunches 11:00 - 11:15	SPLASH OOPSLA HpC: A Calculus for Hybrid and Mobile Systems 11:15 - 11:30	SPLASH OOPSLA Notions of Stack-manipulating Computation and Relative Monads 11:30 - 11:45									SPLASH OOPSLA A Lightweight Type-and-Effect System for Invalidation Safety: Tracking ... 13:45 - 14:00	SPLASH OOPSLA MTP: A Meaning-Typed Language Abstraction for AI-Integrated Programming 14:00 - 14:15	SPLASH OOPSLA Modeling Reachability Types with Logical Relations -- Semantic Type Sou ... 14:15 - 14:30		SPLASH OOPSLA Qualified Types with Boolean Algebras 14:30 - 14:45	SPLASH OOPSLA RestPi: Path-Sensitive Type Inference for REST APIs 14:45 - 15:00	SPLASH OOPSLA Type-Outference with Label-Listeners: Foundations for Decidable Type-Co ... 15:00 - 15:15	SPLASH OOPSLA Type-Preserving Flat Closure Optimization 15:15 - 15:30			SPLASH OOPSLA A Domain-Specific Probabilistic Programming Language for Reasoning abou ... 16:00 - 16:15	SPLASH OOPSLA ROSpec: A Domain-Specific Language for ROS-based Robot Software 16:15 - 16:30	SPLASH OOPSLA Large Language Model powered Symbolic Execution 16:30 - 16:45	SPLASH OOPSLA Multi-Language Probabilistic Programming 16:45 - 17:00	SPLASH OOPSLA Polymorphic Records for Dynamic Languages 17:00 - 17:15
Peony SE							SPLASH Onward! Papers What You See Is What It Does: A Structural Pattern for Legible Software 10:30 - 11:00		SPLASH Onward! Papers Literate Tracing 11:00 - 11:30		SPLASH Onward! Papers ScooPy: Enhancing Program Synthesis with Nested Example Specifications 11:30 - 12:00									SPLASH Onward! Essays Carving Text at Its Joints: A New Perspective on Writing and Computers 13:45 - 14:25			SPLASH Onward! Essays Let's Take Esoteric Programming Languages Seriously 14:25 - 15:05							SPLASH Onward! Papers Exploring The Design Space For Runtime Enforcement of Dynamic Capabilities 16:00 - 16:30		SPLASH Onward! Papers Synchronous Programming for Kids: A Manifesto 16:30 - 17:00

Sat 18 Oct
Displayed time zone: Perth change


Room	9:00	15	30	45	10:00	15	30	45	11:00	15	30		45		12:00	15	30	45	13:00	15	30	45		14:00	15	30		45	15:00		15	30	45	16:00		15	30		45	17:00	15	30	45
Orchid Dining Hall					ICFP/SPLASH Catering Break 10:00 - 10:30											ICFP/SPLASH Catering Lunch 12:15 - 13:45																ICFP/SPLASH Catering Break 15:30 - 16:00
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
Orchid Plenary Ballroom	SPLASH Keynotes Software Stacks for Confidential Computing Hardware 09:00 - 10:00						SPLASH OOPSLA Abstraction Refinement-guided Program Synthesis for Robot Learning from ... 10:30 - 10:45	SPLASH OOPSLA API-guided Dataset Synthesis to Finetune Large Code Models 10:45 - 11:00	SPLASH OOPSLA Fast Constraint Synthesis for C++ Function Templates 11:00 - 11:15	SPLASH OOPSLA Hambazi: Spatial Coordination Synthesis for Augmented Reality 11:15 - 11:30	SPLASH OOPSLA Inductive Synthesis of Inductive Heap Predicates 11:30 - 11:45		SPLASH OOPSLA LOUD: Synthesizing Strongest and Weakest Specifications 11:45 - 12:00		SPLASH OOPSLA Metamorph: Synthesizing Large Objects from Dafny Specifications 12:00 - 12:15							SPLASH OOPSLA Tunneling Through the Hill: Multi-Way Intersection for Version-Space Al ... 13:45 - 14:00		SPLASH OOPSLA Language-Parametric Reference Synthesis 14:00 - 14:15	SPLASH OOPSLA UTFix: Change Aware Unit Test Repairing using LLM 14:15 - 14:30	SPLASH OOPSLA Synthesizing DSLs for Few-Shot Learning 14:30 - 14:45		SPLASH OOPSLA Synthesizing Implication Lemmas for Interactive Theorem Proving 14:45 - 15:00	SPLASH OOPSLA Synthesizing Sound and Precise Abstract Transformers for Nonlinear Hype ... 15:00 - 15:15					SPLASH OOPSLA A Refinement Methodology for Distributed Programs in Rust 16:00 - 16:15		SPLASH OOPSLA AutoVerus: Automated Proof Generation for Rust Code 16:15 - 16:30	SPLASH OOPSLA Carapace: Static–Dynamic Information Flow Control in Rust 16:30 - 16:45		SPLASH OOPSLA From Linearity to Borrowing 16:45 - 17:00	SPLASH OOPSLA Garbage Collection for Rust: The Finalizer Frontier 17:00 - 17:15	SPLASH OOPSLA Place Capability Graphs: A General-Purpose Model of Rust’s Ownership an ... 17:15 - 17:30
Orchid Small							SPLASH OOPSLA AccelerQ: Accelerating Quantum Eigensolvers With Machine Learning on Qu ... 10:30 - 10:45	SPLASH OOPSLA A Language for Quantifying Quantum Network Behavior 10:45 - 11:00	SPLASH OOPSLA Compositional Quantum Control Flow with Efficient Compilation in Qunity 11:00 - 11:15	SPLASH OOPSLA Dependency-Aware Compilation for Surface Code Quantum Architectures 11:15 - 11:30	SPLASH OOPSLA QbC: Quantum Correctness by Construction 11:30 - 11:45		SPLASH OOPSLA qblaze: An Efficient and Scalable Sparse Quantum Simulator 11:45 - 12:00		SPLASH OOPSLA Shaking Up Quantum Simulators with Fuzzing and Rigour 12:00 - 12:15							SPLASH OOPSLA Adaptive Shielding via Parametric Safety Proofs 13:45 - 14:00		SPLASH OOPSLA Certified Decision Procedures for Width-Independent Bitvector Predicates 14:00 - 14:15	SPLASH OOPSLA Checking $\delta$-Satisfiability of Reals with Integrals 14:15 - 14:30	SPLASH OOPSLA Coinductive Proofs of Regular Expression Equivalence in Zero Knowledge 14:30 - 14:45		SPLASH OOPSLA Incremental Certified Programming 14:45 - 15:00	SPLASH OOPSLA Pathological Cases for a Class of Reachability-Based Garbage Collectors 15:00 - 15:15		SPLASH OOPSLA SafeTree: Expressive Tree Policies for Microservices 15:15 - 15:30			SPLASH OOPSLA (TOPLAS) Polynomial Bounds of CFLOBDDs against BDDs 16:00 - 16:15		SPLASH OOPSLA (TOPLAS) Type-Safe Compilation of Dynamic Inheritance via Merging 16:15 - 16:30	SPLASH OOPSLA Detecting and explaining (in-)equivalence of context-free grammars 16:30 - 16:45		SPLASH OOPSLA Modal Abstractions for Virtualizing Memory Addresses 16:45 - 17:00	SPLASH OOPSLA Agora: Trust Less and Open More in Verification for Confidential Computing 17:00 - 17:15	SPLASH OOPSLA QED in Context: An Observation Study of Proof Assistant Users 17:15 - 17:30
Orchid West							SPLASH OOPSLA FO-Complete Program Verification for Heap Logics 10:30 - 10:45	SPLASH OOPSLA Foundations for Deductive Verification of Continuous Probabilistic Prog ... 10:45 - 11:00	SPLASH OOPSLA Guarding the Privacy of Label-Only Access to Neural Network Classifiers ... 11:00 - 11:15	SPLASH OOPSLA KestRel: Relational Verification Using E-Graphs for Program Alignment 11:15 - 11:30	SPLASH OOPSLA Laurel: Unblocking Automated Verification with Large Language Models 11:30 - 11:45		SPLASH OOPSLA Scaling Instruction-Selection Verification against Authoritative ISA Se ... 11:45 - 12:00		SPLASH OOPSLA Verification of Bit-Flip Attacks against Quantized Neural Networks 12:00 - 12:15							SPLASH OOPSLA Automated Verification of Soundness of DNN Certifiers 13:45 - 14:00		SPLASH OOPSLA Bolt-On Strong Consistency: Specification, Implementation, and Verification 14:00 - 14:15	SPLASH OOPSLA Memory-Safety Verification of Open Programs With Angelic Assumptions 14:15 - 14:30	SPLASH OOPSLA Mini-Batch Robustness Verification of Deep Neural Networks 14:30 - 14:45		SPLASH OOPSLA Revamping Verilog Semantics for Foundational Verification 14:45 - 15:00	SPLASH OOPSLA Scalable Equivalence Checking and Verification of Shallow Quantum Circuits 15:00 - 15:15		SPLASH OOPSLA Structural temporal logic for mechanized program verification 15:15 - 15:30			SPLASH OOPSLA Products of Recursive Programs for Hypersafety Verification 16:00 - 16:15		SPLASH OOPSLA Embedding Quantum Program Verification into Dafny 16:15 - 16:30	SPLASH OOPSLA Faster Explicit-Trace Monitoring-Oriented Programming for Runtime Verif ... 16:30 - 16:45		SPLASH OOPSLA Interactive Bit Vector Reasoning using Verified Bitblasting 16:45 - 17:00
Peony NW							SPLASH -E Daisy: An Exercise Environment for Learning Information Modeling 10:30 - 11:00		SPLASH -E Porpoise: An LLM-Based Sandbox for Novices to Practice Writing Purpose ... 11:00 - 11:30		SPLASH -E Evolving How We Teach Memory Models 11:30 - 11:50			SPLASH -E How Computer Science Was Introduced at Yale-NUS College 11:50 - 12:30									SPLASH -E An Interactive Learning Environment for Program Design 13:50 - 14:15		SPLASH -E Continuations for All: Language Design Considerations for Accessible Co ... 14:15 - 14:40		SPLASH -E Involving Students in Design and Implementation of ECMAScript (JavaScri ... 14:40 - 15:05			SPLASH -E An Exploration of How Generative AI Affects Workflow and Collaboration ... 15:05 - 15:30			SPLASH -E Derivation Visualization for Context-Free Grammar Design: Helping Stude ... 15:45 - 16:10		SPLASH -E Interactive Theorem Provers for Proof Education 16:10 - 16:35			SPLASH -E Waddle: A Serious Game to Teach Writing, Reading, and Debugging Programs 16:35 - 17:00		SPLASH -E Personalization of Programming Education: An NLP-based Bi-dimensional C ... 17:00 - 17:25
Peony SE							SPLASH Onward! Papers X-by-Construction: Towards Ensuring Non-Functional Properties in by-Con ... 10:30 - 11:00		SPLASH Onward! Essays Gauguin, Descartes, Bayes: A Diurnal Golem's Brain 11:00 - 11:40			SPLASH Onward! Papers Closing 11:40 - 11:50

SPLASH 2025 Program

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

Tracks

ICFP/SPLASH 2025

Co-hosted Conferences

Workshops

Co-hosted Symposia

SPLASH 2025 Program

Switch Program View

Program Display Configuration

Sun 12 OctDisplayed time zone: Perth change

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

Get Calendar (iCal)

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