SPLASH 2025 Contributors - SPLASH 2025

SPLASH 2025 Contributors - SPLASH 2025
SPLASH 2025
Sun 12 - Sat 18 October 2025
Singapore
co-located with
ICFP/SPLASH 2025
Attending
Venue (Sunday Workshops): NUS School of Computing
Venue (FARM Performance): Yong Siew Toh Conservatory
Venue (Main Conference): Marina Bay Sands Convention Centre
Hotels: Concorde Hotel Singapore
Hotels: Wyndham Singapore Hotel
Hotels: Rendezvous Hotel Singapore
ICFP/SPLASH 2025
Code of Conduct
Call for Sponsorship
Registration
Travel Information
Explore Singapore
Outdoor Activities
Information for Presenters at National University of Singapore
Information for Presenters at Marina Bay Sands
Information for Session Chairs
Information for Attendees
ICFP/SPLASH Live Streams
Program
ICFP/SPLASH Program
Your Program
Filter by Day
Sun 12 Oct
Mon 13 Oct
Tue 14 Oct
Wed 15 Oct
Thu 16 Oct
Fri 17 Oct
Sat 18 Oct
Tracks
SPLASH 2025
Doctoral Symposium
FARM
OOPSLA
OOPSLA Artifacts
Onward! Essays
Onward! Papers
Posters
SPLASH Keynotes
SPLASH-E
Student Research Competition
ICFP/SPLASH 2025
Tutorials
Volunteers
Workshops
Co-hosted Conferences
ICFP
ICFP
ICFP
Artifacts
ICFP
Keynotes
ICFP
Papers
ICFP
Student Research Competition
ICFP
JFP First Papers
ICFP
Diversity, Equity, and Inclusion
MPLR
Workshops
Erlang
FARM
FUNARCH
HATRA
HOPE
IWACO
LMPL
miniKanren
ML Family Workshop
OCaml
OlivierFest
PAINT
PLMW @ ICFP/SPLASH
PROPL
REBASE
Scheme
Sponsor Invited Talks
The Scala Workshop
The Scala Workshop
- Where Are We With Scala's Capabilities?
- Simpler Scala Builds with Functional and Object-Oriented Programming
TyDe
VMIL
WebAssembly Workshop
@ ICFP/SPLASH
Co-hosted Symposia
Haskell
SAS
SAS
SAS
Artifact
Organization
SPLASH 2025 Committees
Organizing Committee
Steering Committee
Track Committees
Doctoral Symposium
FARM
Organizing Committee
Program Committee
OOPSLA
OOPSLA Review Committee
External Review / Artifact Evaluation Committee
OOPSLA Artifacts
Onward! Essays
Program Committee
Onward! Steering Committee
Onward! Papers
Program Committee
Steering Committee
Posters
SPLASH-E
Program Commitee
Steering Committee
Student Research Competition
Competition Judges
Review Committee
ICFP/SPLASH
Volunteers
Workshops
Contributors
People Index
Co-hosted Conferences
ICFP
Organizing Committee
Steering Committee
Distinguished Papers Committee
ICFP Artifacts
ICFP Papers
ICFP Student Research Competition
MPLR
Program Committee
Steering Committee
Workshops
Erlang
Organizing Committee
Program Committee
FARM
Organizing Committee
FUNARCH
Program Committee
HATRA
Organizing Committee
Program Committee
HOPE
Program Committee
IWACO
Organizing Committee
LMPL
Organizing Committee
Keynote Speaker
Program Committee
miniKanren
Organizing Committee
Program Committee
ML Family Workshop
Program Committee
OCaml
Program Committee
OlivierFest
Program Committee
PAINT
Organizing Committee
Program Committee
PLMW @ ICFP/SPLASH
Program Committee
PROPL
Program Committee
Organising Committee
REBASE
Organizing Committee
Scheme
Organizing Committee
Program Committee
Sponsor Invited Talks
Organizing Committee
The Scala Workshop
Organizing Committee
Program Committee
TyDe
Organising Committee
Program Committee
VMIL
Organizing Committee
Program Committee
WebAssembly Workshop
Organizers
Program Committee
Co-hosted Symposia
Haskell
Program Committee
SAS
SAS 2025
Program Committee
SAS 2025
Steering Committee
SAS Artifact
Series
Series
SPLASH 2026
SPLASH 2025
SPLASH 2024
SPLASH 2023
SPLASH 2022
SPLASH 2021
SPLASH 2020
SPLASH 2019
SPLASH 2018
SPLASH 2017
SPLASH 2016
SPLASH 2015
SPLASH 2014
SPLASH 2013
SPLASH 2012
SPLASH 2011
SPLASH 2010
OOPSLA 2009
OOPSLA 2008
OOPSLA 2007
OOPSLA 2006
OOPSLA 2005
OOPSLA 2004
OOPSLA 2003
OOPSLA 2002
OOPSLA 2001
OOPSLA 2000
SPLASH 2025 Contributors
Filter
Role Type
Contributing to
Number of Roles
Country
Results
1388
Zain K Aamer
Aamer, Zain K
University of Pennsylvania
United States
Bennet: Randomized Specification Testing for Heap-Manipulating Programs
Neha Abbas
Abbas, Neha
University of California, Santa Cruz
SafeRace: Assessing and Addressing WebGPU Memory Safety in the Presence of Data Races
Andreas Abel
Abel, Andreas
Gothenburg University
Sweden
Committee Member in ICFP Programme Committee within the ICFP Papers-track
Coşku Acay
Acay, Coşku
Observe, Inc.
United States
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Michael D. Adams
Adams, Michael D.
National University of Singapore
United States
Pushing the Information-Theoretic Limits of Random Access Lists
Nicholas Adams
Adams, Nicholas
None
How to secure a distributed database such as OpenRiak with open-source tools
Eddie Aftandilian
Aftandilian, Eddie
GitHub Next
United States
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Chaitanya Agarwal
Agarwal, Chaitanya
New York University
Abstract Interpretation of Temporal Safety Effects of Higher Order Programs
Alejandro Aguirre
Aguirre, Alejandro
Aarhus University
Denmark
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs
Danel Ahman
Ahman, Danel
University of Ljubljana
Slovenia
SecRef*: Securely Sharing Mutable References between Verified and Unverified Code in F*
Amal Ahmed
Ahmed, Amal
Northeastern University, USA
United States
Steering Committee Member in Steering Committee for SPLASH 2025
[Closed Session] Adjudication meeting for SIGPLAN's John Vlissides award
Committee Member in Program Committee and Panel within the SPLASH Doctoral Symposium-track
From Linearity to Borrowing
Joongwon Ahn
Ahn, Joongwon
Seoul National University
React-tRace: A Semantics for Understanding React Hooks
Benedikt Ahrens
Ahrens, Benedikt
Delft University of Technology
Netherlands
2-Functoriality of Initial Semantics, and Applications
Willow Ahrens
Ahrens, Willow
Massachusetts Institute of Technology
United States
Finch: Sparse and Structured Tensor Programming with Control Flow
The Continuous Tensor Abstraction: Where Indices are Real
Marat Akhin
Akhin, Marat
JetBrains
Netherlands
Finding Compiler Bugs through Cross-Language Code Generator and Differential Testing
Aws Albarghouthi
Albarghouthi, Aws
University of Wisconsin-Madison
United States
Dependency-Aware Compilation for Surface Code Quantum Architectures
Checking Observational Correctness of Database Systems
Compiling Quantum Circuits
Jonathan Aldrich
Aldrich, Jonathan
Carnegie Mellon University
United States
Structural Information Flow: A Fresh Look at Types for Non-Interference
Mark W. Aldrich
Aldrich, Mark W.
Tufts University
United States
RestPi: Path-Sensitive Type Inference for REST APIs
Karim Ali
Ali, Karim
NYU Abu Dhabi
United Arab Emirates
Committee Member in Program Committee within the SAS -track
Shan Ali
Ali, Shan
Yale University
Coinductive Proofs of Regular Expression Equivalence in Zero Knowledge
Guillaume Allais
Allais, Guillaume
University of Strathclyde
United Kingdom
Frex: Dependently Typed Algebraic Simplification
Committee Member in ICFP Programme Committee within the ICFP Papers-track
Henry Allard
Allard, Henry
Iowa State University
United States
Embedding Quantum Program Verification into Dafny
Anders Alnor Mathiasen
Alnor Mathiasen, Anders
Aarhus University
Denmark
Reasoning about Weak Isolation Levels in Separation Logic
Dalal Alrajeh
Alrajeh, Dalal
Imperial College London
United Kingdom
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Saman Amarasinghe
Amarasinghe, Saman
Massachusetts Institute of Technology
United States
Finch: Sparse and Structured Tensor Programming with Control Flow
The Continuous Tensor Abstraction: Where Indices are Real
Nada Amin
Amin, Nada
Harvard University
United States
Committee Member in ICFP Programme Committee within the ICFP Papers-track
Junwen An
An, Junwen
Singapore
LLM-assisted Dialect-Agnostic SQL Query Parsing
Yujin An
An, Yujin
Chungnam National University
Simplifying Lifter-generated Emulation Style LLVM IR for Analysis Suitability
Zixi An
An, Zixi
Debugging WebAssembly? Put some Whamm on it!
Aditya Anand
Anand, Aditya
Indian Institute of Technology Bombay
India
CoSSJIT: Combining Static Analysis and Speculation in JIT Compilers
Emmanuel Anaya Gonzalez
Anaya Gonzalez, Emmanuel
UCSD
Laurel: Unblocking Automated Verification with Large Language Models
Carolyn Jane Anderson
Anderson, Carolyn Jane
Wellesley College
United States
PC Member in Program Committee within the SPLASH Onward! Essays-track
Cezar-Constantin Andrici
Andrici, Cezar-Constantin
MPI-SP
Germany
SecRef*: Securely Sharing Mutable References between Verified and Unverified Code in F*
Sebastian Angel
Angel, Sebastian
University of Pennsylvania
United States
Structural temporal logic for mechanized program verification
Anastasios Antoniadis
Antoniadis, Anastasios
University of Athens, Greece
Greece
Universal Scalability in Declarative Program Analysis (with Choice-Based Combination Pruning)
Timos Antonopoulos
Antonopoulos, Timos
Yale University
United States
Coinductive Proofs of Regular Expression Equivalence in Zero Knowledge
Meghana Aparna Sistla
Aparna Sistla, Meghana
The University of Texas at Austin
United States
Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
David Aponte
Aponte, David
Microsoft
SPLAT: A framework for optimised GPU code-generation for SParse reguLar ATtention
Vincenzo Arceri
Arceri, Vincenzo
University of Parma, Italy
Italy
Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Blair Archibald
Archibald, Blair
University of Glasgow
United Kingdom
TideScript: A Domain Specific Language for Peptide Chemistry
Sven Argo
Argo, Sven
Ruhr University Bochum
Detecting and explaining (in-)equivalence of context-free grammars
Kenichi Asai
Asai, Kenichi
Ochanomizu University
Japan
Session Chair of Morning Paper Session (part of SPLASH -E)
Committee Member in Program Commitee within the SPLASH -E-track
Flavio Ascari
Ascari, Flavio
University of Pisa
Revealing Sources of (Memory) Errors via Backward Analysis
Eric Atkinson
Atkinson, Eric
Binghamton University
Artifact Evaluation Co-Chair in Organizing Committee for SPLASH 2025
Artifact Evaluation Co-Chair in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
OOPSLA Artifact Awards
Skyler Austen
Austen, Skyler
Brown University
Sharing is Scaring: Linking Cloud File-Sharing to Programming Language Semantics
Charles Averill
Averill, Charles
University of Texas at Dallas
United States
The Proof Must Go On: Formal Methods in the Theater of Secure Software Development of the Future
Jessy Ayala
Ayala, Jessy
University of California, Irvine
United States
Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Sacha-Élie Ayoun
Ayoun, Sacha-Élie
Imperial College London
United Kingdom
Compositional Symbolic Execution for the Next 700 Memory Models
Pedro Henrique Azevedo de Amorim
Azevedo de Amorim, Pedro Henrique
Cornell University
Denotational Foundations for Expected Cost Analysis
Timur Babakol
Babakol, Timur
SUNY Binghamton, USA
Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Casper Bach
Bach, Casper
University of Southern Denmark
Denmark
Language-Parametric Reference Synthesis
Jakub Bachurski
Bachurski, Jakub
University of Cambridge
United Kingdom
Mind the Abstraction Gap: Bringing Equality Saturation to Real-World ML Compilers
Kyungmin Bae
Bae, Kyungmin
POSTECH
South Korea
Formal Analysis of Networked PLC Controllers Interacting with Physical Environments
Committee Member in Program Committee within the SAS -track
Thomas BAGREL
BAGREL, Thomas
Tweag, LORIA/INRIA
Destination calculus: A linear λ-calculus for purely functional memory writes
Alexander Bai
Bai, Alexander
New York University
United States
Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Debugging WebAssembly? Put some Whamm on it!
Metamorph: Synthesizing Large Objects from Dafny Specifications
Guangdong Bai
Bai, Guangdong
University of Queensland
Australia
Convex Hull Approximation for Activation Functions
Hrishikesh Balakrishnan
Balakrishnan, Hrishikesh
University of Illinois Urbana-Champaign
FO-Complete Program Verification for Heap Logics
Lucas Bang
Bang, Lucas
Harvey Mudd College
PLMW Co-Chair in Organizing Committee for SPLASH 2025
Elisa Baniassad
Baniassad, Elisa
University of British Columbia
Canada
Committee Member in Program Commitee within the SPLASH -E-track
Peihua Bao
Bao, Peihua
University of Chinese Academy of Sciences
Stencil-Lifting: Hierarchical Recursive Lifting System for Extracting Summary of Stencil Kernel in Legacy Codes
Yuyan Bao
Bao, Yuyan
Augusta University
United States
Modeling Reachability Types with Logical Relations -- Semantic Type Soundness, Termination, Effect Safety, and Equational Theory
Complete the Cycle: Reachability Types with Expressive Cyclic References
Mikhail Barash
Barash, Mikhail
University of Bergen
Norway
Session Chair of Afternoon Paper Session 2 (part of SPLASH -E)
Involving Students in Design and Implementation of ECMAScript (JavaScript) Proposals
Sébastien Bardin
Bardin, Sébastien
CEA LIST, University Paris-Saclay
France
Committee Member in Program Committee within the SAS -track
Shraddha Barke
Barke, Shraddha
Microsoft Research, Redmond
United States
PC Member in Program Committee within the SPLASH Onward! Essays-track
Celeste Barnaby
Barnaby, Celeste
University of Texas at Austin
United States
Active Learning for Neurosymbolic Program Synthesis
Dan Barowy
Barowy, Dan
Williams College
United States
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Clark Barrett
Barrett, Clark
Stanford University
United States
Interactive Bit Vector Reasoning using Verified Bitblasting
Aurèle Barrière
Barrière, Aurèle
EPFL
Switzerland
Committee Member in ICFP Programme Committee within the ICFP Papers-track
Antranig Basman
Basman, Antranig
Raising the Floor - International
United Kingdom
Committee Member in Program Committee within the SPLASH Onward! Papers-track
Matteo Basso
Basso, Matteo
Università della Svizzera italiana (USI)
HeapBuffers: Why not just using a binary serialization format for your managed memory?
Heap-Snapshot Matching and Ordering using CAHPs: A Context-Augmented Heap-Path Representation for Exact and Partial Path Matching using Prefix Trees
Osbert Bastani
Bastani, Osbert
University of Pennsylvania
United States
Opportunistically Parallel Lambda Calculus
Active Learning for Neurosymbolic Program Synthesis
Mark Batty
Batty, Mark
University of Kent
United Kingdom
Symbolic MRD: Dynamic Memory, Undefined Behaviour, and Extrinsic Choice
Kevin Batz
Batz, Kevin
RWTH Aachen University
Germany
Foundations for Deductive Verification of Continuous Probabilistic Programs: From Lebesgue to Riemann and Back
Guillaume Baudart
Baudart, Guillaume
Inria
France
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Emilien Bauer
Bauer, Emilien
University of Edinburgh
Compressed and Parallelized Structured Tensor Algebra
Rohan Bavishi
Bavishi, Rohan
Amazon
United States
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Committee Member in Review Committee within the SPLASH Student Research Competition-track
Julia Belyakova
Belyakova, Julia
Purdue University
United States
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Aaron Bembenek
Bembenek, Aaron
The University of Melbourne
Australia
Current Practices for Building LLM-Powered Reasoning Tools Are Ad Hoc—and We Can do Better
Dorra Ben Khalifa
Ben Khalifa, Dorra
ENAC - University of Toulouse
France
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Jiří Beneš
Beneš, Jiří
University of Tübingen
The Simple Essence of Overloading: Making ad-hoc polymorphism more algebraic with flow-based variational type-checking
Avner Bensoussan
Bensoussan, Avner
King's College London
United Kingdom
Shaking Up Quantum Simulators with Fuzzing and Rigour
AccelerQ: Accelerating Quantum Eigensolvers With Machine Learning on Quantum Simulators
Nick Benton
Benton, Nick
Meta
United Kingdom
Committee Member in ICFP Programme Committee within the ICFP Papers-track
Ryan Berger
Berger, Ryan
Nvidia
Translation Validation for LLVM's AArch64 Backend
Simon Berlinger
Berlinger, Simon
Ulm University, Germany
Waddle: A Serious Game to Teach Writing, Reading, and Debugging Programs
Jean-Philippe Bernardy
Bernardy, Jean-Philippe
University of Gothenburg, Sweden
Committee Member in ICFP Programme Committee within the ICFP Papers-track
Quentin Bernet
Bernet, Quentin
EPFL
Logically Qualified Types for Scala
Gilbert Louis Bernstein
Bernstein, Gilbert Louis
University of Washington
United States
Committee Member in Program Committee within the SPLASH FARM-track
Polynomial-Time Program Equivalence for Machine Knitting
Ivan Beschastnikh
Beschastnikh, Ivan
The University of British Columbia
Canada
TraceLinking Implementations with their Verified Designs
Raven Beutner
Beutner, Raven
CISPA Helmholtz Center for Information Security, Germany
Verifying Asynchronous Hyperproperties in Reactive Systems
Siddharth Bhat
Bhat, Siddharth
University of Cambridge
Certified Decision Procedures for Width-Independent Bitvector Predicates
Interactive Bit Vector Reasoning using Verified Bitblasting
Bishnu Bhusal
Bhusal, Bishnu
University of Missouri
United States
Checking $\delta$-Satisfiability of Reals with Integrals
Annette Bieniusa
Bieniusa, Annette
RPTU Kaiserslautern-Landau
Germany
PC Member in Program Committee within the SPLASH Onward! Essays-track
Baldip Bijlani
Bijlani, Baldip
Indian Institute of Technology Kanpur
Memory-Safety Verification of Open Programs With Angelic Assumptions
Vladyslav Bilyk
Bilyk, Vladyslav
Semantics-preserving Transformation of Context-free Grammars into LL(1) Form
Walter Binder
Binder, Walter
USI Lugano
Switzerland
HeapBuffers: Why not just using a binary serialization format for your managed memory?
Heap-Snapshot Matching and Ordering using CAHPs: A Context-Augmented Heap-Path Representation for Exact and Partial Path Matching using Prefix Trees
Lars Birkedal
Birkedal, Lars
Aarhus University
Denmark
Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs
Reasoning about Weak Isolation Levels in Separation Logic
Stephen M. Blackburn
Blackburn, Stephen M.
Google; Australian National University
Australia
Advancing Performance via a Systematic Application of Research and Industrial Best Practice
Work Packets: A New Abstraction for GC Software Engineering, Optimization, and Innovation
Steve Blackburn
Blackburn, Steve
Google and Australian National University
Australia
Session Chair of Abstraction (part of SPLASH OOPSLA)
Jasmin Blanchette
Blanchette, Jasmin
Ludwig-Maximilians-Universität München
Germany
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Sandrine Blazy
Blazy, Sandrine
University of Rennes
France
A Mechanized Semantics for Dataflow Circuits
Committee Member in ICFP Programme Committee within the ICFP Papers-track
Kelly Blincoe
Blincoe, Kelly
University of Auckland
New Zealand
PC Member in Program Committee within the SPLASH Onward! Essays-track
Andrew Blinn
Blinn, Andrew
University of Michigan
United States
Syntactic Completions with Material Obligations
Polina Bobrova
Bobrova, Polina
Restoring Data Sovereignty: A Human-Centered Approach Blockchain Health Technology
Ivana Bocevska
Bocevska, Ivana
TU Wien
Divide and Conquer: A Compositional Approach to Game-Theoretic Security
Sean Bocirnea
Bocirnea, Sean
University of British Columbia
Type-Preserving Flat Closure Optimization
Rastislav Bodík
Bodík, Rastislav
Google Research, Brain Team
United States
HieraSynth: A Parallel Framework for Complete Super-Optimization with Hierarchical Space Decomposition
Rose Bohrer
Bohrer, Rose
National Institute of Advanced Industrial Science and Technology (AIST), Japan
Japan
Committee Member in Program Committee within the SPLASH FARM-track
Giacomo Boldini
Boldini, Giacomo
Ca' Foscari University of Venice
Italy
Committee Member in SAS Artifact Evaluation Committee within the SAS Artifact-track
CF Bolz-Tereick
Bolz-Tereick, CF
Heinrich-Heine-Universität Düsseldorf
Germany
Tracing Just-in-time Compilation for Effects and Handlers
Michael D. Bond
Bond, Michael D.
Ohio State University
Carapace: Static–Dynamic Information Flow Control in Rust
Daniele Bonetta
Bonetta, Daniele
VU Amsterdam
Netherlands
HeapBuffers: Why not just using a binary serialization format for your managed memory?
Tabea Bordis
Bordis, Tabea
Karlsruhe Institute of Technology
X-by-Construction: Towards Ensuring Non-Functional Properties in by-Construction Engineering
Cândida Borges
Borges, Cândida
Concert: The River Oycus
Nader Boushehrinejad Moradi
Boushehrinejad Moradi, Nader
University of Utah
United States
Translation Validation for LLVM's AArch64 Backend
Matt Bovel
Bovel, Matt
EPFL
Existentialize your Generics
Logically Qualified Types for Scala
Wavid Bowman
Bowman, Wavid
University of Florida
United States
Debugging WebAssembly? Put some Whamm on it!
William J. Bowman
Bowman, William J.
University of British Columbia
Canada
PC Member in Program Committee within the SPLASH Onward! Essays-track
Type-Preserving Flat Closure Optimization
Type Universes as Kripke Worlds
Committee Member in ICFP Programme Committee within the ICFP Papers-track
Jonathan Immanuel Brachthäuser
Brachthäuser, Jonathan Immanuel
University of Tübingen
Germany
The Simple Essence of Overloading: Making ad-hoc polymorphism more algebraic with flow-based variational type-checking
Dynamic Wind for Effect Handlers
Tracing Just-in-time Compilation for Effects and Handlers
Compiling Classical Sequent Calculus to Stock Hardware: The Duality of Compilation
The Simple Essence of Monomorphization
Multiple Resumptions and Local Mutable State, Directly
Committee Member in ICFP Programme Committee within the ICFP Papers-track
Edwin Brady
Brady, Edwin
University of St. Andrews
United Kingdom
Frex: Dependently Typed Algebraic Simplification
Oliver Bračevac
Bračevac, Oliver
EPFL, LAMP
Switzerland
Modeling Reachability Types with Logical Relations -- Semantic Type Soundness, Termination, Effect Safety, and Equational Theory
What's in the Box: Ergonomic and Expressive Capture Tracking over Generic Data Structures
Joachim Breitner
Breitner, Joachim
Lean FRO, LLC
Germany
Committee Member in ICFP Programme Committee within the ICFP Papers-track
Ana Brendel
Brendel, Ana
University of California Los Angeles
United States
Synthesizing Implication Lemmas for Interactive Theorem Proving
Mitch Briles
Briles, Mitch
University of Utah
Translation Validation for LLVM's AArch64 Backend
Matthew Britton
Britton, Matthew
The Australian National University
Verifying Extract Method Refactoring in Rust
Rutger Broekhoff
Broekhoff, Rutger
Radboud University Nijmegen
Netherlands
Verified Interpreters for Dynamic Languages with Applications to the Nix Expression Language
Fraser Brown
Brown, Fraser
CMU
Scaling Instruction-Selection Verification against Authoritative ISA Semantics
Roberto Bruni
Bruni, Roberto
University of Pisa
Italy
Revealing Sources of (Memory) Errors via Backward Analysis
Committee Member in Program Committee within the SAS -track
Anita Buckley
Buckley, Anita
USI Lugano
A Language for Quantifying Quantum Network Behavior
Humphrey Burchell
Burchell, Humphrey
University of Kent
United Kingdom
Divining Profiler Accuracy: An Approach to Approximate Profiler Accuracy Through Machine Code-Level Slowdown
Roger Burtonpatel
Burtonpatel, Roger
University of Pennsylvania
United States
Rocq N'Roll
Concert: RocqNRoll
William E. Byrd
Byrd, William E.
University of Alabama at Birmingham
United States
Committee Member in ICFP Programme Committee within the ICFP Papers-track
Aurea Bílá
Bílá, Aurea
ETH Zurich
Switzerland
Place Capability Graphs: A General-Purpose Model of Rust’s Ownership and Borrowing Guarantees
A Refinement Methodology for Distributed Programs in Rust
Henrik Böving
Böving, Henrik
Lean FRO
Interactive Bit Vector Reasoning using Verified Bitblasting
Joanna C. S. Santos
C. S. Santos, Joanna
University of Notre Dame
United States
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Cristian Cadar
Cadar, Cristian
Imperial College London
United Kingdom
P³: Reasoning about Patches via Product Programs
Jessica Belicia Cahyono
Cahyono, Jessica Belicia
Institute of Science Tokyo
Japan
Daisy: An Exercise Environment for Learning Information Modeling
Jose Calderon
Calderon, Jose
Galois, Inc.
United States
Exploring the Theory and Practice of Concurrency in the Entity-Component-System Pattern
José Pablo Cambronero
Cambronero, José Pablo
Google, USA
United States
Committee Member in Review Committee within the SPLASH Student Research Competition-track
Marco Campion
Campion, Marco
Sorbonne Université
France
Session Chair of Abstract Interpretation (part of SAS )
Relating Distances and Abstractions: An Abstract Interpretation Perspective
Paulo Canelas
Canelas, Paulo
Carnegie Mellon University
United States
ROSpec: A Domain-Specific Language for ROS-based Robot Software
Man Cao
Cao, Man
Google
Advancing Performance via a Systematic Application of Research and Industrial Best Practice
Qinxiang Cao
Cao, Qinxiang
Shanghai Jiao Tong University
China
Encode the $\forall\exists$ Relational Hoare Logic into Standard Hoare Logic
Cristina Carbunaru
Carbunaru, Cristina
National University of Singapore, Singapore
Singapore
Evolving How We Teach Memory Models
Jacques Carette
Carette, Jacques
McMaster University
Canada
Committee Member in Program Committee within the SPLASH Onward! Papers-track
J. Carr
Carr, J.
University of Chicago
United States
Environment-Sharing Analysis and Caller-Provided Environments for Higher-Order Languages
Chris Casinghino
Casinghino, Chris
Jane Street
A guided tour through Oxidized OCaml
Giuseppe Castagna
Castagna, Giuseppe
CNRS; Université Paris Cité
France
Polymorphic Records for Dynamic Languages
Jonathan Castello
Castello, Jonathan
University of California, Santa Cruz
United States
Exploring the Theory and Practice of Concurrency in the Entity-Component-System Pattern
CRDT Emulation, Simulation, and Representation Independence
Ethan Cecchetti
Cecchetti, Ethan
University of Wisconsin-Madison
United States
Choreographic Quick Changes: First-Class Location (Set) Polymorphism
Sooyoung Cha
Cha, Sooyoung
Sungkyunkwan University
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Elena Chachkarova
Chachkarova, Elena
Kings College London
Shaking Up Quantum Simulators with Fuzzing and Rigour
AccelerQ: Accelerating Quantum Eigensolvers With Machine Learning on Quantum Simulators
Rohit Chadha
Chadha, Rohit
University of Missouri
Checking $\delta$-Satisfiability of Reals with Integrals
Kartik Chandra
Chandra, Kartik
MIT
United States
Gauguin, Descartes, Bayes: A Diurnal Golem's Brain
A Domain-Specific Probabilistic Programming Language for Reasoning about Reasoning (or: a memo on memo)
Bor-Yuh Evan Chang
Chang, Bor-Yuh Evan
University of Colorado Boulder & Amazon
United States
Steering Committee Member in Steering Committee for SPLASH 2025
Session Chair of Analysis 1 (part of SPLASH OOPSLA)
Bolt-On Strong Consistency: Specification, Implementation, and Verification
Committee Member in Steering Committee within the SAS -track
Rui Chang
Chang, Rui
Zhejiang University
A complete formal semantics of eBPF instruction set architecture for Solana
Prantik Chatterjee
Chatterjee, Prantik
MathWorks
India
Memory-Safety Verification of Open Programs With Angelic Assumptions
Chong Chen
Chen, Chong
Beijing Jiaotong University
Fuzzing C++ Compilers via Type-Driven Mutation
Dong Chen
Chen, Dong
Huawei Technologies Co., Ltd
Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Fei Chen
Chen, Fei
German Research Center for Artificial Intelligence (DFKI), Saarland University
Germany
im2im: Automatically Converting In-Memory Image Representations using A Knowledge Graph Approach
Guanlin Chen
Chen, Guanlin
Peking University
Tunneling Through the Hill: Multi-Way Intersection for Version-Space Algebras in Program Synthesis
Hongbo Chen
Chen, Hongbo
Indiana University Bloomington
United States
Agora: Trust Less and Open More in Verification for Confidential Computing
Hongzheng Chen
Chen, Hongzheng
Cornell University
United States
Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Jiasi Chen
Chen, Jiasi
University of Michigan
Hambazi: Spatial Coordination Synthesis for Augmented Reality
Jocelyn Qiaochu Chen
Chen, Jocelyn Qiaochu
New York University, University of Alberta
United States
Automated Discovery of Tactic Libraries for Interactive Theorem Proving
Active Learning for Neurosymbolic Program Synthesis
Junjie Chen
Chen, Junjie
Tianjin University
China
DESIL: Detecting Silent Bugs in MLIR Compiler Infrastructure
Fuzzing C++ Compilers via Type-Driven Mutation
Liqian Chen
Chen, Liqian
NUDT
China
Committee Member in Program Committee within the SAS -track
Menglong Chen
Chen, Menglong
Nanjing University
China
Committee Member in SAS Artifact Evaluation Committee within the SAS Artifact-track
Mingyi Chen
Chen, Mingyi
University of California, Irvine
Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Sen Chen
Chen, Sen
Nankai University
China
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Siyan Chen
Chen, Siyan
Institute of Computing Technology, Chinese Academy of Sciences
Stencil-Lifting: Hierarchical Recursive Lifting System for Extracting Summary of Stencil Kernel in Legacy Codes
Tony Chen
Chen, Tony
MIT
A Domain-Specific Probabilistic Programming Language for Reasoning about Reasoning (or: a memo on memo)
Weijun Chen
Chen, Weijun
Shanghai Jiao Tong University, China
A Programming Language for Feasible Solutions
Weiyi Chen
Chen, Weiyi
Purdue University
Probabilistic Inference for Datalog with Correlated Inputs
Xi Chen
Chen, Xi
Institute of Computing Technology, Chinese Academy of Sciences
Stencil-Lifting: Hierarchical Recursive Lifting System for Extracting Summary of Stencil Kernel in Legacy Codes
Yanju Chen
Chen, Yanju
University of California, San Diego
United States
Tabby: A Synthesis-Aided Compiler for High-Performance Zero-Knowledge Proof Circuits
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Yanning Chen
Chen, Yanning
University of Toronto
Tabby: A Synthesis-Aided Compiler for High-Performance Zero-Knowledge Proof Circuits
Yitong Chen
Chen, Yitong
School of Computer Science and Engineering, College of Software Engineering, School of Artificial Intelligence, Southeast University
ABC: Towards a Universal Code Styler through Model Merging
Zhenbang Chen
Chen, Zhenbang
College of Computer, National University of Defense Technology
China
Multi-Modal Sketch-based Behavior Tree Synthesis
Zhiyang Chen
Chen, Zhiyang
University of Toronto
Canada
A Multi-Layer Dynamic Security Framework for DeFi Smart Contracts
Ellie Y. Cheng
Cheng, Ellie Y.
MIT
United States
Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Feifei Cheng
Cheng, Feifei
Iowa State University
Embedding Quantum Program Verification into Dafny
Luyu Cheng
Cheng, Luyu
Hong Kong University of Science and Technology
Hong Kong SAR China
Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Ruotong Cheng
Cheng, Ruotong
University of Toronto
Canada
Products of Recursive Programs for Hypersafety Verification
Xiao Cheng
Cheng, Xiao
Macquarie University
Australia
Efficient Abstract Interpretation via Selective Widening
SRC Judge & Co-Organizer in Competition Judges within the SPLASH Student Research Competition-track
Alvin Cheung
Cheung, Alvin
University of California at Berkeley
United States
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Tsung-Ju Chiang
Chiang, Tsung-Ju
University of Toronto
Canada
Multi-stage Programming with Splice Variables
Michele Chiari
Chiari, Michele
TU Wien
Austria
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Shigeru Chiba
Chiba, Shigeru
The University of Tokyo
Japan
Steering Committee Member in Steering Committee for SPLASH 2025
Onward! Papers Co-chair in Organizing Committee for SPLASH 2025
Steering Committee Member in Onward! Steering Committee within the SPLASH Onward! Essays-track
Session Chair of Design (part of SPLASH Onward! Papers)
Co-chair in Program Committee within the SPLASH Onward! Papers-track
Steering Committee Member in Steering Committee within the SPLASH Onward! Papers-track
Zakaria Chihani
Chihani, Zakaria
CEA, LIST, France
Verifying Neural Networks with PyRAT
Wei-Ngan Chin
Chin, Wei-Ngan
National University of Singapore
Singapore
Specifying and Verifying Future Conditions
Shardul Chiplunkar
Chiplunkar, Shardul
EPFL
Switzerland
Practical compositional diagramming
Adam Chlipala
Chlipala, Adam
Massachusetts Institute of Technology
United States
Session Chair of Reasoning (part of SPLASH OOPSLA)
Adam Chlipala
Chlipala, Adam
MIT CSAIL
Pyrosome: Verified Compilation for Modular Metatheory
Minki Cho
Cho, Minki
Seoul National University
South Korea
Lilo: A Higher-Order, Relational Concurrent Separation Logic for Liveness
Minsung Cho
Cho, Minsung
United States
Scaling Optimization Over Uncertainty via Compilation
Joonwon Choi
Choi, Joonwon
Amazon Web Services
United States
Revamping Verilog Semantics for Foundational Verification
Eloise Christian
Christian, Eloise
Rochester Institute of Technology
United States
SIGPLAN AV Report
Ravi Chugh
Chugh, Ravi
University of Chicago
Code Style Sheets: CSS for Code
Benjamin Chung
Chung, Benjamin
JuliaHub
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Pavel Chuprikov
Chuprikov, Pavel
Télécom Paris, Institut Polytechnique de Paris
A Language for Quantifying Quantum Network Behavior
Luke Church
Church, Luke
University of Cambridge | Candela Inc
United Kingdom
Committee Member in Program Committee within the SPLASH Onward! Papers-track
Luisa Cicolini
Cicolini, Luisa
University of Cambridge
United Kingdom
Interactive Bit Vector Reasoning using Verified Bitblasting
Cristina Cifuentes
Cifuentes, Cristina
Oracle Software Assurance
Australia
PC Member in Program Committee within the SPLASH Onward! Essays-track
Berk Cirisci
Cirisci, Berk
Amazon Web Services
UTFix: Change Aware Unit Test Repairing using LLM
Jürgen Cito
Cito, Jürgen
TU Wien
Austria
Static Inference of Regular Grammars for Ad Hoc Parsers
Peter Clark
Clark, Peter
None
How to secure a distributed database such as OpenRiak with open-source tools
Christopher Clarke
Clarke, Christopher
University of Michigan
MTP: A Meaning-Typed Language Abstraction for AI-Integrated Programming
Siobhán Clarke
Clarke, Siobhán
Trinity College Dublin, Ireland
Ireland
Committee Member in Program Committee within the SPLASH Onward! Papers-track
Josh Clune
Clune, Josh
Carnegie Mellon University
Interactive Bit Vector Reasoning using Verified Bitblasting
Michael Coblenz
Coblenz, Michael
University of California, San Diego
United States
DEI Chair in Organizing Committee for SPLASH 2025
PC Member in Program Committee within the SPLASH Onward! Essays-track
RestPi: Path-Sensitive Type Inference for REST APIs
On the Impact of Formal Verification on Software Development
An Empirical Evaluation of Property-Based Testing in Python
Session Chair of Onward! Essays 1 (part of SPLASH Onward! Papers)
Tiago Cogumbreiro
Cogumbreiro, Tiago
University of Massachusetts Boston
United States
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Albert Cohen
Cohen, Albert
Google DeepMind
France
Mind the Abstraction Gap: Bringing Equality Saturation to Real-World ML Compilers
Cyril Cohen
Cohen, Cyril
Inria - CNRS - ENS Lyon - Université Claude Bernard Lyon 1 - LIP - UMR 5668
France
A Bargain for Mergesorts: How to Prove Your Mergesort Correct and Stable, Almost for Free
Sam Cohen
Cohen, Sam
University of Chicago
Code Style Sheets: CSS for Code
Youyou Cong
Cong, Youyou
Institute of Science Tokyo
Japan
An Interactive Learning Environment for Program Design
Continuations for All: Language Design Considerations for Accessible Continuations
Daisy: An Exercise Environment for Learning Information Modeling
Organizing Chair in Organizing Committee within the SPLASH FARM-track
Committee Member in Program Committee within the SPLASH FARM-track
Simon Cooksey
Cooksey, Simon
Symbolic MRD: Dynamic Memory, Undefined Behaviour, and Extrinsic Choice
Nathan Corbyn
Corbyn, Nathan
University of Oxford
United Kingdom
Frex: Dependently Typed Algebraic Simplification
Lucas C. Cordeiro
Cordeiro, Lucas C.
University of Manchester, UK
United Kingdom
Committee Member in Program Committee within the SAS -track
Arthur Correnson
Correnson, Arthur
CISPA Helmholtz Center for Information Security
Germany
Almost Fair Simulations
Nicholas Coughlin
Coughlin, Nicholas
Defence Science and Technology Group, Australia
Translation Validation for LLVM's AArch64 Backend
Aaron Councilman
Councilman, Aaron
Univ of Illinois Urbana-Champaign
FO-Complete Program Verification for Heap Logics
Patrick Cousot
Cousot, Patrick
Committee Member in Steering Committee within the SAS -track
Douglas A. Creager
Creager, Douglas A.
Astral
United States
Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Will Crichton
Crichton, Will
Brown University
United States
A guided tour through Oxidized OCaml
Guofeng Cui
Cui, Guofeng
Rutgers University
Abstraction Refinement-guided Program Synthesis for Robot Learning from Demonstrations
Weidong Cui
Cui, Weidong
Microsoft Research
AutoVerus: Automated Proof Generation for Rust Code
Marcelo d'Amorim
d'Amorim, Marcelo
North Carolina State University
United States
Faster Explicit-Trace Monitoring-Oriented Programming for Runtime Verification of Software Tests
Loris D'Antoni
D'Antoni, Loris
University of California at San Diego
United States
LOUD: Synthesizing Strongest and Weakest Specifications
Semantics of Sets of Programs
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Kyle D. Chin
D. Chin, Kyle
An Exploration of How Generative AI Affects Workflow and Collaboration in a Software Engineering Course
Francesco Dagnino
Dagnino, Francesco
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Joshua Dahl
Dahl, Joshua
University of Nevada, Reno
An Argument for the Practicality of Entity Component Systems as the Primary Data Structure for an Interpreter or Compiler
Tim Dahmen
Dahmen, Tim
Aalen University, Aalen, Germany; German Research Center for Artificial Intelligence (DFKI), Saarbrücken, Germany
im2im: Automatically Converting In-Memory Image Representations using A Knowledge Graph Approach
Jiarun Dai
Dai, Jiarun
Fudan University
China
ApkDiffer: Accurate and Scalable Cross-Version Diffing Analysis for Android Applications
Ting Dai
Dai, Ting
IBM Research
Artemis: Toward Accurate Detection of Server-Side Request Forgeries through LLM-Assisted Inter-Procedural Path-Sensitive Taint Analysis
Ugo Dal Lago
Dal Lago, Ugo
University of Bologna & INRIA Sophia Antipolis
Italy
On Higher-Order Model Checking of Effectful Answer-Type-Polymorphic Programs
Committee Member in ICFP Programme Committee within the ICFP Papers-track
Mila Dalla Preda
Dalla Preda, Mila
University of Verona
Italy
Committee Member in Program Committee within the SAS -track
Jayanaka Dantanarayana
Dantanarayana, Jayanaka
University of Michigan
Sri Lanka
MTP: A Meaning-Typed Language Abstraction for AI-Integrated Programming
Olivier Danvy
Danvy, Olivier
National University of Singapore
Singapore
How Computer Science Was Introduced at Yale-NUS College
Session Chair of Verification (part of SAS )
On a simple problem due to Yves Bertot
David Darais
Darais, David
Galois
United States
Committee Member in ICFP Programme Committee within the ICFP Papers-track
Anupam Das
Das, Anupam
University of Birmingham, UK
United Kingdom
Committee Member in ICFP Programme Committee within the ICFP Papers-track
Dylan Davis
Davis, Dylan
Swinburne University
I Am Your Co-Pilot
Charles de Haro
de Haro, Charles
École Normale Supérieure | Université PSL
France
Committee Member in SAS Artifact Evaluation Committee within the SAS Artifact-track
Markus de Medeiros
de Medeiros, Markus
New York University
United States
Place Capability Graphs: A General-Purpose Model of Rust’s Ownership and Borrowing Guarantees
Wolfgang De Meuter
De Meuter, Wolfgang
Vrije Universiteit Brussel
Belgium
Steering Committee Member in Onward! Steering Committee within the SPLASH Onward! Essays-track
Steering Committee Member in Steering Committee within the SPLASH Onward! Papers-track
Coen De Roover
De Roover, Coen
Vrije Universiteit Brussel
Belgium
Steering Committee Member in Steering Committee for SPLASH 2025
Abstracting Concolic Execution for Soft Contract Verification
Delta Store Semantics: Abstract Garbage Collection for Abstract Definitional Interpreters
Monarch: A Modular Framework for Abstract Definitional Interpreters in Haskell
Kyle Deeds
Deeds, Kyle
University of Washington
Finch: Sparse and Structured Tensor Programming with Control Flow
Maryam Mehri Dehnavi
Dehnavi, Maryam Mehri
University of Toronto
Canada
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Benjamin Delaware
Delaware, Benjamin
Purdue University
United States
We’ve Got You Covered: Type-Guided Repair of Incomplete Input Generators
KestRel: Relational Verification Using E-Graphs for Program Alignment
Delphine Demange
Demange, Delphine
Univ Rennes, Inria, CNRS, IRISA
France
A Mechanized Semantics for Dataflow Circuits
Brian Demsky
Demsky, Brian
University of California at Irvine
Towards Verifying Crash Consistency
Haotian Deng
Deng, Haotian
Purdue University
Complete the Cycle: Reachability Types with Expressive Cyclic References
Ming Deng
Deng, Ming
Beijing Jiaotong University
Fuzzing C++ Compilers via Type-Driven Mutation
Anoop Deoras
Deoras, Anoop
AWS AI Labs
UTFix: Change Aware Unit Test Repairing using LLM
Farzaneh Derakhshan
Derakhshan, Farzaneh
Illinois Institute of Technology
United States
Quantified Underapproximation via Labeled Bunches
Committee Member in ICFP Programme Committee within the ICFP Papers-track
Ankush Desai
Desai, Ankush
Amazon Web Services
United States
Checking Observational Correctness of Database Systems
Dominique Devriese
Devriese, Dominique
KU Leuven
Belgium
Session Chair of Distinguished Papers (part of ICFP Papers)
PC Chair Report
Award Ceremony
PC Chair in ICFP Programme Committee within the ICFP Papers-track
Session Chair of Wednesday ICFP Keynote (part of ICFP Keynotes)
Samvid Dharanikota
Dharanikota, Samvid
Efficient Computer
United States
Fray: An Efficient General-Purpose Concurrency Testing Platform for the JVM
Tomás Diaz
Diaz, Tomás
University of Chile
Chile
Flexible and Expressive Typed Path Patterns for GQL
Incremental Certified Programming
Robert Dickerson
Dickerson, Robert
Purdue University
United States
KestRel: Relational Verification Using E-Graphs for Program Alignment
Işıl Dillig
Dillig, Işıl
University of Texas at Austin
United States
Steering Committee Member in Steering Committee for SPLASH 2025
Automated Discovery of Tactic Libraries for Interactive Theorem Proving
Probabilistic Inference for Datalog with Correlated Inputs
Homomorphism Calculus for User-Defined Aggregations
Active Learning for Neurosymbolic Program Synthesis
Associate Chair in OOPSLA Review Committee within the SPLASH OOPSLA-track
Dimitar Dimitrov
Dimitrov, Dimitar
INSAIT, Sofia University "St. Kliment Ohridski"
Bulgaria
qblaze: An Efficient and Scalable Sparse Quantum Simulator
Christos Dimoulas
Dimoulas, Christos
Northwestern University
United States
Contract System Metatheories à la Carte: A Transition-System View of Contracts
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
The Rational Programmer, A Method for Investigating Programming Language Pragmatics
Shuo Ding
Ding, Shuo
Georgia Institute of Technology
China
Fast Constraint Synthesis for C++ Function Templates
Alexander Dinges
Dinges, Alexander
RPTU Kaiserslautern-Landau
Germany
Truly Functional Solutions to the Longest Uptrend Problem (Functional Pearl)
Chandeepa Dissanayake
Dissanayake, Chandeepa
Iowa State University
United States
A Haskell Adiabatic DSL: Solving Classical Optimization Problems on Quantum Hardware
Stephen Dolan
Dolan, Stephen
Jane Street
United Kingdom
Modal Effect Types
Jin Song Dong
Dong, Jin Song
National University of Singapore
Singapore
Verification of Bit-Flip Attacks against Quantized Neural Networks
Rui Dong
Dong, Rui
University of Michigan
United States
Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Maximilian Doré
Doré, Maximilian
University of Oxford
Linear Types with Dynamic Multiplicities in Dependent Type Theory (Functional Pearl)
Dana Drachsler Cohen
Drachsler Cohen, Dana
Technion
Israel
Quantization with Guaranteed Floating-Point Neural Network Classifications
Mini-Batch Robustness Verification of Deep Neural Networks
Guarding the Privacy of Label-Only Access to Neural Network Classifiers via Formal Verification
Enhancing Neural Network Robustness via Synthesis of Repair Programs
Steve Draper
Draper, Steve
University of Glasgow
Let's Take Esoteric Programming Languages Seriously
Alexandre Drewery
Drewery, Alexandre
INRIA
Contextual Equality Saturation
Derek Dreyer
Dreyer, Derek
MPI-SWS
Germany
JFP Announcement
Sophia Drossopoulou
Drossopoulou, Sophia
Imperial College London
United Kingdom
Reasoning about External Calls
Cezara Drăgoi
Drăgoi, Cezara
AWS / ENS
Committee Member in Steering Committee within the SAS -track
Xuan Du Trinh
Du Trinh, Xuan
Stony Brook University
United States
Scalable Equivalence Checking and Verification of Shallow Quantum Circuits
Xiaoning Du
Du, Xiaoning
Monash University
Australia
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Yuanlin Duan
Duan, Yuanlin
Rutgers University
Abstraction Refinement-guided Program Synthesis for Robot Learning from Demonstrations
Christophe Dubach
Dubach, Christophe
McGill University
Canada
Sound and Modular Activity Analysis for Automatic Differentiation in MLIR
Stéphane Ducasse
Ducasse, Stéphane
Inria; University of Lille; CNRS; Centrale Lille; CRIStAL
France
Committee Member in Program Committee within the SPLASH Onward! Papers-track
Gregory J. Duck
Duck, Gregory J.
National University of Singapore
Singapore
Large Language Model powered Symbolic Execution
Léon Ducruet
Ducruet, Léon
Aarhus University
Denmark
Reasoning about Weak Isolation Levels in Separation Logic
Arpita Dutta
Dutta, Arpita
National University of Singapore
Singapore
Incremental and Unbounded Loop Analysis
Saikat Dutta
Dutta, Saikat
Cornell University
United States
Understanding and Improving Flaky Test Classification
Saikat Dutta
Dutta, Saikat
University of Illinois at Urbana-Champaign
United States
Precise Abstract Interpretation of Probabilistic Programs with Interval Data Uncertainty
Harley D. Eades III
Eades III, Harley D.
Augusta University
United States
Committee Member in ICFP Programme Committee within the ICFP Papers-track
Jonathan Edwards
Edwards, Jonathan
Independent
United States
Steering Committee Member in Steering Committee for SPLASH 2025
Steering Committee Member in Onward! Steering Committee within the SPLASH Onward! Essays-track
Steering Committee Member in Steering Committee within the SPLASH Onward! Papers-track
Marco Eilers
Eilers, Marco
ETH Zurich
Switzerland
Modular Reasoning about Global Variables and Their Initialization
Susan Eisenbach
Eisenbach, Susan
Imperial College London
United Kingdom
Reasoning about External Calls
Richard A. Eisenberg
Eisenberg, Richard A.
Jane Street
United States
Session Chair of Type 2 (part of SPLASH OOPSLA)
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
A guided tour through Oxidized OCaml
Martin Elsman
Elsman, Martin
University of Copenhagen
Denmark
Session Chair of Applications and SRC Talks (part of ICFP Papers)
Joel S Emer
Emer, Joel S
MIT/NVIDIA
United States
The Continuous Tensor Abstraction: Where Indices are Real
Madeline Endres
Endres, Madeline
University of Massachusetts Amherst
United States
PC Member in Program Committee within the SPLASH Onward! Essays-track
Constantin Enea
Enea, Constantin
LIX, CNRS, Ecole Polytechnique
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Sebastian Erdweg
Erdweg, Sebastian
KIT
Germany
Associate Chair in OOPSLA Review Committee within the SPLASH OOPSLA-track
Guilherme Espada
Espada, Guilherme
LASIGE, University of Lisbon
Portugal
SIGPLAN AV Report
Patrick Eugster
Eugster, Patrick
USI Lugano, Switzerland
Switzerland
A Language for Quantifying Quantum Network Behavior
Tae Eun Kim
Eun Kim, Tae
KAIST
South Korea
Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Karine Even-Mendoza
Even-Mendoza, Karine
King’s College London
United Kingdom
Session Chair of Testing 1 (part of SPLASH OOPSLA)
Session Chair of Compilation 2 (part of SPLASH OOPSLA)
Shaking Up Quantum Simulators with Fuzzing and Rigour
AccelerQ: Accelerating Quantum Eigensolvers With Machine Learning on Quantum Simulators
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Teodoro F. Collin
F. Collin, Teodoro
MIT CSAIL
Finch: Sparse and Structured Tensor Programming with Control Flow
The Continuous Tensor Abstraction: Where Indices are Real
Luis F. Gomes
F. Gomes, Luis
Carnegie Mellon University
Portugal
Student Volunteer Co-Chair in Organizing Committee for SPLASH 2025
Chris Fallin
Fallin, Chris
F5
United States
Scaling Instruction-Selection Verification against Authoritative ISA Semantics
Max Fan
Fan, Max
Cornell University
Proof Repair across Quotient Type Equivalences
Le Fang
Fang, Le
Purdue University
Show Me Why It's Correct: Saving 1/3 of Debugging Time in Program Repair with Interactive Runtime Comparison
Ruijie Fang
Fang, Ruijie
University of Texas at Austin
United States
Software Model Checking via Summary-Guided Search
Homomorphism Calculus for User-Defined Aggregations
Umar Farooq
Farooq, Umar
Louisiana State University
United States
Publicity Co-Chair, Web Co-Chair in Organizing Committee for SPLASH 2025
Azadeh Farzan
Farzan, Azadeh
University of Toronto
Canada
Products of Recursive Programs for Hypersafety Verification
Andrew Fawcett
Fawcett, Andrew
Victoria University of Wellington
New Zealand
Exploring The Design Space For Runtime Enforcement of Dynamic Capabilities
Aleksandr Fedchin
Fedchin, Aleksandr
Tufts University
United States
Metamorph: Synthesizing Large Objects from Dafny Specifications
Grigory Fedyukovich
Fedyukovich, Grigory
Florida State University
United States
A Flow-Sensitive Refinement Type System for Verifying eBPF Programs
Marc Feeley
Feeley, Marc
Université de Montréal
Canada
Float Self-Tagging
Joan Feigenbaum
Feigenbaum, Joan
Yale
On Collective Control over User Interfaces in the Face of Network Effects
Qiong Feng
Feng, Qiong
Nanjing University of Science and Technology
China
Finding Compiler Bugs through Cross-Language Code Generator and Differential Testing
Yang Feng
Feng, Yang
Nanjing University
China
An Empirical Study of Bugs in the rustc Compiler
Yao Feng
Feng, Yao
Tsinghua University
Adaptive Shielding via Parametric Safety Proofs
Yu Feng
Feng, Yu
University of California at Santa Barbara
United States
Tabby: A Synthesis-Aided Compiler for High-Performance Zero-Knowledge Proof Circuits
Ziyuan Feng
Feng, Ziyuan
Nanjing University of Science and Technology
Finding Compiler Bugs through Cross-Language Code Generator and Differential Testing
Pietro Ferrara
Ferrara, Pietro
Ca’ Foscari University of Venice
Italy
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Patrick Ferris
Ferris, Patrick
University of Cambridge, UK
United Kingdom
Functional Networking for Millions of Docker Desktops (Experience Report)
Jack Feser
Feser, Jack
Basis
United States
Peepco: Batch-Based Consistency Optimization
Jonáš Fiala
Fiala, Jonáš
ETH Zürich
Place Capability Graphs: A General-Purpose Model of Rust’s Ownership and Borrowing Guarantees
David Anthony K. Fields
Fields, David Anthony K.
Seton Hall University
Automata Visualization for Validation and Verification: Helping Develop Correctness Arguments for Nondeterministic Machines
Andrzej Filinski
Filinski, Andrzej
DIKU, University of Copenhagen
Committee Member in ICFP Programme Committee within the ICFP Papers-track
Robert Bruce Findler
Findler, Robert Bruce
Northwestern University
United States
Contract System Metatheories à la Carte: A Transition-System View of Contracts
Metaprogramming in Rhombus
Committee Member in ICFP Programme Committee within the ICFP Papers-track
Bernd Finkbeiner
Finkbeiner, Bernd
CISPA Helmholtz Center for Information Security
Germany
Verifying Asynchronous Hyperproperties in Reactive Systems
Almost Fair Simulations
Patricia Firlejczyk
Firlejczyk, Patricia
ETH Zurich
Switzerland
Modular Reasoning about Global Variables and Their Initialization
Emily First
First, Emily
University of California, San Diego
United States
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Kathi Fisler
Fisler, Kathi
Brown University
United States
Sharing is Scaring: Linking Cloud File-Sharing to Programming Language Semantics
Matthew Flatt
Flatt, Matthew
University of Utah
United States
Session Chair of Systems (part of SPLASH OOPSLA)
Metaprogramming in Rhombus
Krisztian Flautner
Flautner, Krisztian
University of Michigan
MTP: A Meaning-Typed Language Abstraction for AI-Integrated Programming
Cyril Flurin Moser
Flurin Moser, Cyril
ETH Zurich
Validating Soundness and Completeness in Pattern-Match Coverage Analyzers
Alcides Fonseca
Fonseca, Alcides
LASIGE; University of Lisbon
Portugal
ROSpec: A Domain-Specific Language for ROS-based Robot Software
Darius Foo
Foo, Darius
National University of Singapore
Specifying and Verifying Future Conditions
Sophie Fortz
Fortz, Sophie
King's College London
United Kingdom
Shaking Up Quantum Simulators with Fuzzing and Rigour
AccelerQ: Accelerating Quantum Eigensolvers With Machine Learning on Quantum Simulators
Jeffrey S. Foster
Foster, Jeffrey S.
Tufts University
United States
Session Chair of Synthesis 2 (part of SPLASH OOPSLA)
RestPi: Path-Sensitive Type Inference for REST APIs
Metamorph: Synthesizing Large Objects from Dafny Specifications
Nate Foster
Foster, Nate
Cornell University; Jane Street
United States
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Adrian Francalanza
Francalanza, Adrian
University of Malta
Malta
Correct Black-Box Monitors for Distributed Deadlock Detection: Formalisation and Implementation
Michael Franz
Franz, Michael
University of California, Irvine
United States
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Leon Frenot
Frenot, Leon
ENS Lyon
Interactive Bit Vector Reasoning using Verified Bitblasting
Marco Frigo
Frigo, Marco
University of Illinois at Urbana-Champaign
End-to-End Compiler Infrastructure for Emerging Tensor Accelerators
Thomas Fritz
Fritz, Thomas
University of Zurich
Switzerland
An Exploration of How Generative AI Affects Workflow and Collaboration in a Software Engineering Course
Daniel Frumin
Frumin, Daniel
University of Groningen
Netherlands
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Hongfei Fu
Fu, Hongfei
Shanghai Jiao Tong University
China
Structural Abstraction and Refinement for Probabilistic Programs
Yuxi Fu
Fu, Yuxi
Shanghai Jiao Tong University, China
A Programming Language for Feasible Solutions
Marcial Gaißert
Gaißert, Marcial
University of Tübingen
Germany
Tracing Just-in-time Compilation for Effects and Handlers
Pierre Ganty
Ganty, Pierre
IMDEA Software Institute, Spain
Committee Member in Program Committee within the SAS -track
Cunyuan Gao
Gao, Cunyuan
HKUST
A Lightweight Type-and-Effect System for Invalidation Safety: Tracking Permanent and Temporary Invalidation With Constraint-Based Subtype Inference
Miao Gao
Gao, Miao
School of Computer Science and Engineering, College of Software Engineering, School of Artifical Intelligence, Southeast University
ABC: Towards a Universal Code Styler through Model Merging
Pengfei Gao
Gao, Pengfei
ByteDance
Verification of Bit-Flip Attacks against Quantized Neural Networks
Yanfeng Gao
Gao, Yanfeng
Nanjing University
HybridPersist: A Compiler Support for User-Friendly and Efficient PM Programming
Zhiqiang Gao
Gao, Zhiqiang
School of Computer Science and Engineering, College of Software Engineering, School of Artifical Intelligence, Southeast University
ABC: Towards a Universal Code Styler through Model Merging
Andrés M. Garced
Garced, Andrés M.
Seton Hall University
Derivation Visualization for Context-Free Grammar Design: Helping Students Understand Context-Free Grammars
Ronald Garcia
Garcia, Ronald
University of British Columbia
Canada
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Philippa Gardner
Gardner, Philippa
Imperial College London
United Kingdom
Compositional Symbolic Execution for the Next 700 Memory Models
Deepak Garg
Garg, Deepak
MPI-SWS
Germany
Non-interference Preserving Optimising Compilation
Fusing Session-Typed Concurrent Programming into Functional Programming
Committee Member in ICFP Programme Committee within the ICFP Papers-track
Harshit Garg
Garg, Harshit
Northeastern University - Khoury College of Computer Sciences
United States
Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Poorva Garg
Garg, Poorva
University of California, Los Angeles
India
Tuning Random Generators: Property-Based Testing as Probabilistic Programming
Pranav Garg
Garg, Pranav
AWS
United States
UTFix: Change Aware Unit Test Repairing using LLM
Antoine Gaulin
Gaulin, Antoine
McGill University
Canada
McTT: A Verified Kernel for a Proof Assistant
François Gauthier
Gauthier, François
Oracle Labs
Australia
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Thomas Gazagnaire
Gazagnaire, Thomas
Tarides
France
Functional Networking for Millions of Docker Desktops (Experience Report)
Yuhao Ge
Ge, Yuhao
University of Illinois at Urbana-Champaign
SPLAT: A framework for optimised GPU code-generation for SParse reguLar ATtention
Zhaoyi Ge
Ge, Zhaoyi
University of Waterloo
Canada
Zero-Overhead Lexical Effect Handlers
Jasper Geer
Geer, Jasper
University of British Columbia
Canada
Place Capability Graphs: A General-Purpose Model of Rust’s Ownership and Borrowing Guarantees
Timon Gehr
Gehr, Timon
ETH Zurich
Switzerland
qblaze: An Efficient and Scalable Sparse Quantum Simulator
Adam T. Geller
Geller, Adam T.
University of British Columbia
Canada
Type-Preserving Flat Closure Optimization
Samir Genaim
Genaim, Samir
Universidad Complutense de Madrid
Spain
Committee Member in Program Committee within the SAS -track
Jared Gentner
Gentner, Jared
None
How to Score in the Art Racket
Aina Linn Georges
Georges, Aina Linn
Max Planck Institute for Software Systems (MPI-SWS)
Committee Member in ICFP Programme Committee within the ICFP Papers-track
Kimball Germane
Germane, Kimball
Brigham Young University
United States
Session Chair of Algorithms (part of ICFP Papers)
Call-Guarded Abstract Definitional Interpreters
Dan Ghica
Ghica, Dan
Huawei Research and University of Birmingham
United Kingdom
Committee Member in ICFP Programme Committee within the ICFP Papers-track
Mahdi Ghorbani
Ghorbani, Mahdi
University of Edinburgh
United Kingdom
Compressed and Parallelized Structured Tensor Algebra
Roberto Giacobazzi
Giacobazzi, Roberto
University of Arizona
United States
Committee Member in Steering Committee within the SAS -track
Ryan Gibb
Gibb, Ryan
University of Cambridge
Functional Networking for Millions of Docker Desktops (Experience Report)
Olek Gierczak
Gierczak, Olek
Northeastern University
From Linearity to Borrowing
Elizabeth Gilbert
Gilbert, Elizabeth
Carnegie Mellon University
United States
Debugging WebAssembly? Put some Whamm on it!
Elena Glassman
Glassman, Elena
Harvard University
United States
PC Member in Program Committee within the SPLASH Onward! Essays-track
Nathan Glover
Glover, Nathan
Carnegie Mellon University
Integrating Resource Analyses via Resource Decomposition
Brighten Godfrey
Godfrey, Brighten
UIUC and Broadcom
SafeTree: Expressive Tree Policies for Microservices
Harrison Goldstein
Goldstein, Harrison
University at Buffalo, the State University of New York at Buffalo
United States
Tuning Random Generators: Property-Based Testing as Probabilistic Programming
QED in Context: An Observation Study of Proof Assistant Users
Sergey Goncharov
Goncharov, Sergey
University of Birmingham
United Kingdom
Bialgebraic Reasoning on Stateful Languages
Big Steps in Higher-Order Mathematical Operational Semantics
Léon Gondelman
Gondelman, Léon
Aalborg University
Denmark
Reasoning about Weak Isolation Levels in Separation Logic
Yeyun Gong
Gong, Yeyun
Microsoft Research
AutoVerus: Automated Proof Generation for Rust Code
Elisa Gonzalez Boix
Gonzalez Boix, Elisa
Vrije Universiteit Brussel
Belgium
Committee Member in Program Committee within the SPLASH Onward! Papers-track
Noah D. Goodman
Goodman, Noah D.
Stanford University
Automated Discovery of Tactic Libraries for Interactive Theorem Proving
Kiran Gopinathan
Gopinathan, Kiran
University of Illinois Urbana Champaign
United States
Committee Member in ICFP Programme Committee within the ICFP Papers-track
Colin Gordon
Gordon, Colin
Drexel University
United States
Steering Committee Member in Steering Committee for SPLASH 2025
Onward! Essays Co-chair in Organizing Committee for SPLASH 2025
Program Chair in Program Committee within the SPLASH Onward! Essays-track
Steering Committee Member in Onward! Steering Committee within the SPLASH Onward! Essays-track
Modal Abstractions for Virtualizing Memory Addresses
Steering Committee Member in Steering Committee within the SPLASH Onward! Papers-track
Roberta Gori
Gori, Roberta
Diaprtimento di Informatica, Universita' di Pisa, Italy
Revealing Sources of (Memory) Errors via Backward Analysis
Alessandra Gorla
Gorla, Alessandra
IMDEA Software Institute
Spain
Committee Member in Steering Committee within the SAS -track
Chester Gould
Gould, Chester
University of British Columbia
Type-Preserving Flat Closure Optimization
Hemant Gouni
Gouni, Hemant
Carnegie Mellon University
United States
Structural Information Flow: A Fresh Look at Types for Non-Interference
Pierre Goutagny
Goutagny, Pierre
Inria and University of Lille
France
Committee Member in SAS Artifact Evaluation Committee within the SAS Artifact-track
John Gouwar
Gouwar, John
Northeastern University
United States
Scaling Optimization Over Uncertainty via Compilation
Kevin Graaf
Graaf, Kevin
Independent Researcher
Carving Text at Its Joints: A New Perspective on Writing and Computers
Marcos Grandury
Grandury, Marcos
IMDEA Software Institute; Universidad Politécnica de Madrid
Spain
Verifying Graph Algorithms in Separation Logic: A Case for an Algebraic Approach
Zachary Grannan
Grannan, Zachary
University of British Columbia
Canada
Place Capability Graphs: A General-Purpose Model of Rust’s Ownership and Borrowing Guarantees
Daniel Gratzer
Gratzer, Daniel
Aarhus University
Denmark
Committee Member in ICFP Programme Committee within the ICFP Papers-track
Eva Graversen
Graversen, Eva
University of Southern Denmark
Committee Member in ICFP Programme Committee within the ICFP Papers-track
James Bryan Graves
Graves, James Bryan
Indiana University
A Haskell Adiabatic DSL: Solving Classical Optimization Problems on Quantum Hardware
Gavin Gray
Gray, Gavin
Brown University
United States
A guided tour through Oxidized OCaml
Neville Grech
Grech, Neville
Dedaub Limited
Malta
Universal Scalability in Declarative Program Analysis (with Choice-Based Combination Pruning)
Michael Greenberg
Greenberg, Michael
Stevens Institute of Technology
United States
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Ben Greenman
Greenman, Ben
University of Utah
United States
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Ben Greenman
Greenman, Ben
University of Utah, USA
Workshops Co-Chair in Workshop Selection Committee within the ICFP/SPLASH Workshops-track
Simon Oddershede Gregersen
Gregersen, Simon Oddershede
New York University
United States
Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs
Karuna Grewal
Grewal, Karuna
Cornell University
SafeTree: Expressive Tree Policies for Microservices
Tobias Grosser
Grosser, Tobias
University of Cambridge
United Kingdom
Certified Decision Procedures for Width-Independent Bitvector Predicates
Interactive Bit Vector Reasoning using Verified Bitblasting
Compressed and Parallelized Structured Tensor Algebra
Alexander Gryzlov
Gryzlov, Alexander
IMDEA Software Institute
Spain
Verifying Graph Algorithms in Separation Logic: A Case for an Algebraic Approach
Dawu Gu
Gu, Dawu
Shanghai Jiao Tong University
Binary Cryptographic Function Identification via Similarity Analysis with Path-insensitive Emulation
Yile Gu
Gu, Yile
University of Washington
Scalable and Accurate Application-level Crash-Consistency Testing via Representative Testing
Hanqin Guan
Guan, Hanqin
Peking University
Orax: A Feedback-Driven Framework for Efficiently Solving Satisfiability Modulo Theories and Oracles
Kevin Guan
Guan, Kevin
Cornell University
United States
Faster Explicit-Trace Monitoring-Oriented Programming for Runtime Verification of Software Tests
Ege Berkay Gulcan
Gulcan, Ege Berkay
Delft University of Technology
Netherlands
Model-guided Fuzzing of Distributed Systems
Ahan Gupta
Gupta, Ahan
University of Illinois at Urbana-Champaign
SPLAT: A framework for optimised GPU code-generation for SParse reguLar ATtention
Arie Gurfinkel
Gurfinkel, Arie
University of Waterloo
Canada
A Flow-Sensitive Refinement Type System for Verifying eBPF Programs
Sankha Narayan Guria
Guria, Sankha Narayan
University of Kansas
United States
Artifact Evaluation Co-Chair in Organizing Committee for SPLASH 2025
Artifact Evaluation Co-Chair in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
OOPSLA Artifact Awards
Claudio Gutierrez
Gutierrez, Claudio
DCC, Universidad de Chile & IMFD
Flexible and Expressive Typed Path Patterns for GQL
Huong Ha
Ha, Huong
RMIT University
Australia
Committee Member in Review Committee within the SPLASH Student Research Competition-track
Andrew Habib
Habib, Andrew
ABB Corporate Research, Germany
Germany
Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Sebastian Hack
Hack, Sebastian
Saarland University, Saarland Informatics Campus
Germany
Non-interference Preserving Optimising Compilation
Finn Hackett
Hackett, Finn
University of British Columbia
Canada
TraceLinking Implementations with their Verified Designs
Kerry Hagan
Hagan, Kerry
University of Illinois, Urbana-Champaign
United States
Cellular Automata as a Model For 1-bit Synthesis in Mitosis
Concert: Mitosis
Matthew Hague
Hague, Matthew
Royal Holloway University of London
United Kingdom
The Power of Regular Constraint Propagation
Shashin Halalingaiah
Halalingaiah, Shashin
UT Austin, IIT Madras
United States
Probabilistic Inference for Datalog with Correlated Inputs
William Hallahan
Hallahan, William
Binghamton
Counterexample-Guided Inference of Modular Specifications
Philipp Haller
Haller, Philipp
KTH Royal Institute of Technology
Sweden
Committee Member in Program Committee within the SPLASH Onward! Papers-track
Sara S. Hamouda
Hamouda, Sara S.
Canva
Advancing Performance via a Systematic Application of Research and Industrial Best Practice
Ameer Hamza
Hamza, Ameer
Florida State University
United States
A Flow-Sensitive Refinement Type System for Verifying eBPF Programs
Xing Han
Han, Xing
The Hong Kong University of Science and Technology
Agora: Trust Less and Open More in Verification for Confidential Computing
Zhilei Han
Han, Zhilei
Tsinghua University
Structural Abstraction and Refinement for Probabilistic Programs
Dan Hao
Hao, Dan
Peking University
China
Fuzzing C++ Compilers via Type-Driven Mutation
Ben Hardekopf
Hardekopf, Ben
University of California at Santa Barbara
United States
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Adi Harif
Harif, Adi
Ductape: Optimizing Dynamically Typed Programs using Ahead-of-Time Compilation and Data-Flow Analysis
Frederick C. Harris Jr.
Harris Jr., Frederick C.
University of Nevada, Reno
United States
An Argument for the Practicality of Entity Component Systems as the Primary Data Structure for an Interpreter or Compiler
Philipp G. Haselwarter
Haselwarter, Philipp G.
Aarhus University
Denmark
Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs
Zara Hassan
Hassan, Zara
Australian National University
Australia
Reproducibility Debt in Scientific Software
Ichiro Hasuo
Hasuo, Ichiro
National Institute of Informatics, Japan
Japan
A Unifying Approach to Product Constructions for Quantitative Temporal Inference
Matthias Hauswirth
Hauswirth, Matthias
USI Lugano
Switzerland
Associate Chair in OOPSLA Review Committee within the SPLASH OOPSLA-track
Chris Hawblitzel
Hawblitzel, Chris
Microsoft Research
United States
AutoVerus: Automated Proof Generation for Rust Code
Musa Haydar
Haydar, Musa
University of Michigan
Scalable and Accurate Application-level Crash-Consistency Testing via Representative Testing
Dongjie He
He, Dongjie
Chongqing University, China
China
Fast Client-Driven CFL-Reachability via Regularization-Based Graph Simplification
Fei He
He, Fei
Tsinghua University
China
Structural Abstraction and Refinement for Probabilistic Programs
Jingzhu He
He, Jingzhu
ShanghaiTech University
China
Artemis: Toward Accurate Detection of Server-Side Request Forgeries through LLM-Assisted Inter-Procedural Path-Sensitive Taint Analysis
Ningyu He
He, Ningyu
Hong Kong Polytechnic University
Hong Kong SAR China
Committee Member in Program Committee within the SAS -track
Pinjia He
He, Pinjia
Chinese University of Hong Kong, Shenzhen
China
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Siyuan He
He, Siyuan
Purdue University
Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Complete the Cycle: Reachability Types with Expressive Cyclic References
Wenyu He
He, Wenyu
Shanghai Jiao Tong University
Binary Cryptographic Function Identification via Similarity Analysis with Path-insensitive Emulation
Yituo He
He, Yituo
Shanghai Jiao Tong University
Binary Cryptographic Function Identification via Similarity Analysis with Path-insensitive Emulation
Yumeng He
He, Yumeng
University of Utah
Formalizing Linear Motion G-code for Invariant Checking and Differential Testing of Fabrication Tools
Andrew Head
Head, Andrew
University of Pennsylvania
QED in Context: An Observation Study of Proof Assistant Users
Fritz Henglein
Henglein, Fritz
University of Copenhagen
Denmark
Committee Member in ICFP Programme Committee within the ICFP Papers-track
Troels Henriksen
Henriksen, Troels
University of Copenhagen
Denmark
Correctness Meets Performance: From Agda to Futhark
Martin Henz
Henz, Martin
National University of Singapore
Singapore
SPLASH-E Co-Chair in Organizing Committee for SPLASH 2025
Session Chair of Afternoon Paper Session 1 (part of SPLASH -E)
SPLASH-E Co-Chair in Program Commitee within the SPLASH -E-track
Kihong Heo
Heo, Kihong
KAIST
South Korea
Co-chair in SAS Artifact Evaluation Committee within the SAS Artifact-track
Felienne Hermans
Hermans, Felienne
Vrije Universiteit Amsterdam
Netherlands
SPLASH-E Co-Chair in Organizing Committee for SPLASH 2025
SPLASH-E Co-Chair in Program Commitee within the SPLASH -E-track
Manuel Hermenegildo
Hermenegildo, Manuel
Technical University of Madrid (UPM) and IMDEA Software Institute
Spain
Committee Member in Steering Committee within the SAS -track
Keara Hill
Hill, Keara
Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Daniel Hillerström
Hillerström, Daniel
Category Labs and The University of Edinburgh
United Kingdom
Modal Effect Types
Ralf Hinze
Hinze, Ralf
RPTU Kaiserslautern-Landau
Truly Functional Solutions to the Longest Uptrend Problem (Functional Pearl)
Andrew K. Hirsch
Hirsch, Andrew K.
University at Buffalo, SUNY
United States
Choreographic Quick Changes: First-Class Location (Set) Polymorphism
Session Chair of Concurrency (part of ICFP Papers)
Robert Hirschfeld
Hirschfeld, Robert
Hasso Plattner Institute; University of Potsdam
Germany
Steering Committee Member in Steering Committee for SPLASH 2025
Steering Committee Member in Onward! Steering Committee within the SPLASH Onward! Essays-track
Steering Committee Member in Steering Committee within the SPLASH Onward! Papers-track
Martin Hirzel
Hirzel, Martin
IBM Research
United States
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Son Ho
Ho, Son
Inria
France
Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Jan Hoffmann
Hoffmann, Jan
Carnegie Mellon University
United States
Integrating Resource Analyses via Resource Decomposition
Committee Member in ICFP Programme Committee within the ICFP Papers-track
Reid Holmes
Holmes, Reid
University of British Columbia
Canada
Committee Member in Program Committee within the SPLASH Onward! Papers-track
An Exploration of How Generative AI Affects Workflow and Collaboration in a Software Engineering Course
Steven Holtzen
Holtzen, Steven
Northeastern University
United States
Multi-Language Probabilistic Programming
Scaling Optimization Over Uncertainty via Compilation
Michael Homer
Homer, Michael
Victoria University of Wellington
New Zealand
Exploring The Design Space For Runtime Enforcement of Dynamic Capabilities
Changwan Hong
Hong, Changwan
Massachusetts Institute of Technology
Finch: Sparse and Structured Tensor Programming with Control Flow
Weijiang Hong
Hong, Weijiang
National University of Defense Technology, Changsha, China
Multi-Modal Sketch-based Behavior Tree Synthesis
Manoel Horta Ribeiro
Horta Ribeiro, Manoel
Interactive Theorem Provers for Proof Education
Tony Hosking
Hosking, Tony
Australian National University
Australia
Session Chair of Parallelism (part of SPLASH OOPSLA)
Cătălin Hriţcu
Hriţcu, Cătălin
MPI-SP
Germany
SecRef*: Securely Sharing Mutable References between Verified and Unverified Code in F*
Committee Member in ICFP Programme Committee within the ICFP Papers-track
Justin Hsu
Hsu, Justin
Cornell University
United States
SafeTree: Expressive Tree Policies for Microservices
A Hoare Logic For Symmetry Properties
Guangyu Hu
Hu, Guangyu
HKUST (The Hong Kong University of Science and Technology)
Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Jason Z. S. Hu
Hu, Jason Z. S.
Amazon
United States
Normalization by Evaluation for Non-cumulativity
McTT: A Verified Kernel for a Proof Assistant
Jingmei Hu
Hu, Jingmei
Amazon
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Yikun Hu
Hu, Yikun
Shanghai Jiao Tong University
China
Binary Cryptographic Function Identification via Similarity Analysis with Path-insensitive Emulation
Zhenjiang Hu
Hu, Zhenjiang
Peking University
China
Associate Chair in OOPSLA Review Committee within the SPLASH OOPSLA-track
Effectful Lenses: There and Back with Different Monads
Heqing Huang
Huang, Heqing
City University of Hong Kong
Publicity Co-Chair, Web Co-Chair in Organizing Committee for SPLASH 2025
Jeff Huang
Huang, Jeff
Texas A&M University
United States
Workshop Co-Chair in Organizing Committee for SPLASH 2025
DepFuzz: Efficient Smart Contract Fuzzing with Function Dependence Guidance
Workshops Co-Chair in Workshop Selection Committee within the ICFP/SPLASH Workshops-track
Lei Huang
Huang, Lei
ShanghaiTech University
Verification of Bit-Flip Attacks against Quantized Neural Networks
Tianshu Huang
Huang, Tianshu
Carnegie Mellon University
Unveiling Heisenbugs with Diversified Execution
Xuejing Huang
Huang, Xuejing
IRIF
France
(TOPLAS) Type-Safe Compilation of Dynamic Inheritance via Merging
Liberating Merges via Apartness and Guarded Subtyping
Zixin Huang
Huang, Zixin
University of Illinois at Urbana-Champaign, USA
Precise Abstract Interpretation of Probabilistic Programs with Interval Data Uncertainty
Jan Hueckelheim
Hueckelheim, Jan
Argonne National Laboratory
Synthesizing Sound and Precise Abstract Transformers for Nonlinear Hyperbolic PDE Solvers
Chris Hughes
Hughes, Chris
Independent Researcher
Certified Decision Procedures for Width-Independent Bitvector Predicates
Jacob Hughes
Hughes, Jacob
King's College London
United Kingdom
Garbage Collection for Rust: The Finalizer Frontier
Chung-Kil Hur
Hur, Chung-Kil
Seoul National University
South Korea
Lilo: A Higher-Order, Relational Concurrent Separation Logic for Liveness
Nathan Hurtig
Hurtig, Nathan
University of Washington
United States
Polynomial-Time Program Equivalence for Machine Knitting
Doha Hwang
Hwang, Doha
Samsung
PAFL: Enhancing Fault Localizers by Leveraging Project-Specific Fault Patterns
Ruxandra Icleanu
Icleanu, Ruxandra
University of Edinburgh
SecRef*: Securely Sharing Mutable References between Verified and Unverified Code in F*
Yuka Ikarashi
Ikarashi, Yuka
Massachusetts Institute of Technology
United States
Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Kazuki Ikemori
Ikemori, Kazuki
Tokyo Institute of Technology
Continuations for All: Language Design Considerations for Accessible Continuations
Lef Ioannidis
Ioannidis, Lef
University of Pennsylvania
United States
Structural temporal logic for mechanized program verification
Anastasia Isychev
Isychev, Anastasia
TU Wien
Austria
Cost of Soundness in Mixed-Precision Tuning
Shachar Itzhaky
Itzhaky, Shachar
Technion
Israel
Ductape: Optimizing Dynamically Typed Programs using Ahead-of-Time Compilation and Data-Flow Analysis
Daniel Jackson
Jackson, Daniel
MIT
What You See Is What It Does: A Structural Pattern for Legible Software
Jules Jacobs
Jacobs, Jules
Jane Street
United States
Committee Member in ICFP Programme Committee within the ICFP Papers-track
Koen Jacobs
Jacobs, Koen
Inria
France
Robust Dynamic Embedding for Gradual Typing
Seyed Mohammad Reza Jafari
Jafari, Seyed Mohammad Reza
Iowa State University
Embedding Quantum Program Verification into Dafny
Joxan Jaffar
Jaffar, Joxan
National University of Singapore
Singapore
Incremental and Unbounded Loop Analysis
Suresh Jagannathan
Jagannathan, Suresh
Purdue University
United States
We’ve Got You Covered: Type-Guided Repair of Incomplete Input Generators
Devansh Jain
Jain, Devansh
University of Illinois at Urbana-Champaign
SPLAT: A framework for optimised GPU code-generation for SParse reguLar ATtention
End-to-End Compiler Infrastructure for Emerging Tensor Accelerators
Joel Jakubovic
Jakubovic, Joel
Charles University in Prague
Czechia
The Unix Executable as a Smalltalk Method
Committee Member in Program Committee within the SPLASH Onward! Papers-track
Vincent James Beardsley
James Beardsley, Vincent
Carapace: Static–Dynamic Information Flow Control in Rust
Dustin Jamner
Jamner, Dustin
MIT CSAIL, USA
Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Dustin Jamner
Jamner, Dustin
MIT CSAIL
Pyrosome: Verified Compilation for Modular Metatheory
Junyoung Jang
Jang, Junyoung
McGill University
Canada
McTT: A Verified Kernel for a Proof Assistant
Sujin Jang
Jang, Sujin
KAIST
South Korea
Committee Member in SAS Artifact Evaluation Committee within the SAS Artifact-track
Nikhil Jayakumar
Jayakumar, Nikhil
University of Texas at Austin
GALA: A High Performance Graph Neural Network Acceleration LAnguage and Compiler
Thomas P. Jensen
Jensen, Thomas P.
INRIA Rennes
Contextual Equality Saturation
Minseok Jeon
Jeon, Minseok
DGIST
South Korea
PAFL: Enhancing Fault Localizers by Leveraging Project-Specific Fault Patterns
Committee Member in ICFP Programme Committee within the ICFP Papers-track
Mingyeong Jeong
Jeong, Mingyeong
Chungnam National University
Type Checking for Python Using Intersection Types
Artur Jez
Jez, Artur
University of Wroclaw
The Power of Regular Constraint Propagation
Ranjit Jhala
Jhala, Ranjit
University of California at San Diego
United States
Counterexample-Guided Inference of Modular Specifications
Ranjit Jhala
Jhala, Ranjit
University of California at San Diego
United States
On the Impact of Formal Verification on Software Development
Laurel: Unblocking Automated Verification with Large Language Models
Ruyi Ji
Ji, Ruyi
Peking University
China
Tunneling Through the Hill: Multi-Way Intersection for Version-Space Algebras in Program Synthesis
Yuchen Ji
Ji, Yuchen
ShanghaiTech University
Artemis: Toward Accurate Detection of Server-Side Request Forgeries through LLM-Assisted Inter-Procedural Path-Sensitive Taint Analysis
Limin Jia
Jia, Limin
Carnegie Mellon University
Session Chair of Verification 1 (part of SPLASH OOPSLA)
Session Chair of Calculus (part of SPLASH OOPSLA)
Limin Jia
Jia, Limin
Carnegie Mellon University
United States
Quantified Underapproximation via Labeled Bunches
Limin Jia
Jia, Limin
Carnegie Mellon University
Associate Chair in OOPSLA Review Committee within the SPLASH OOPSLA-track
Songlin Jia
Jia, Songlin
Purdue University, USA
United States
Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Modeling Reachability Types with Logical Relations -- Semantic Type Soundness, Termination, Effect Safety, and Equational Theory
Complete the Cycle: Reachability Types with Expressive Cyclic References
Jiajun Jiang
Jiang, Jiajun
Tianjin University
China
DESIL: Detecting Silent Bugs in MLIR Compiler Infrastructure
Nan Jiang
Jiang, Nan
Purdue University
United States
Show Me Why It's Correct: Saving 1/3 of Debugging Time in Program Repair with Interactive Runtime Comparison
Shengyi Jiang
Jiang, Shengyi
The University of Hong Kong
China
Normalization by Evaluation for Non-cumulativity
Yuchao Jiang
Jiang, Yuchao
UNSW
Australia
Committee Member in Review Committee within the SPLASH Student Research Competition-track
Yuchen Jiang
Jiang, Yuchen
University of Michigan
United States
Notions of Stack-manipulating Computation and Relative Monads
Mingyu Jo
Jo, Mingyu
Korea University
Lemma Discovery for Inductive Equational Proofs via Recursive Function Synthesis
Iris Johnson
Johnson, Iris
NHL Stenden University of Applied Sciences
Netherlands
Committee Member in Program Committee within the SPLASH FARM-track
Sarah Johnson
Johnson, Sarah
Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Jonghyun Jung
Jung, Jonghyun
University of Waterloo
Zero-Overhead Lexical Effect Handlers
Ralf Jung
Jung, Ralf
ETH Zurich
Switzerland
Committee Member in ICFP Programme Committee within the ICFP Papers-track
Sebastian Junges
Junges, Sebastian
Radboud University
A Unifying Approach to Product Constructions for Quantitative Temporal Inference
Anan Kabaha
Kabaha, Anan
Technion, Israel Institute of Technology
Israel
Quantization with Guaranteed Floating-Point Neural Network Classifications
Guarding the Privacy of Label-Only Access to Neural Network Classifiers via Formal Verification
Rohan Kadekodi
Kadekodi, Rohan
University of Washington
Scalable and Accurate Application-level Crash-Consistency Testing via Representative Testing
Gowtham Kaki
Kaki, Gowtham
University of Colorado at Boulder
United States
Bolt-On Strong Consistency: Specification, Implementation, and Verification
Konstantinos Kallas
Kallas, Konstantinos
University of California, Los Angeles
United States
Opportunistically Parallel Lambda Calculus
Shoaib Kamil
Kamil, Shoaib
Adobe Research
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Arsyad Kamili
Kamili, Arsyad
Singapore
A Concurrency-Testing Approach for Detecting Isolation Level Bugs in Database Systems
Ohad Kammar
Kammar, Ohad
University of Edinburgh
United Kingdom
Frex: Dependently Typed Algebraic Simplification
Committee Member in ICFP Programme Committee within the ICFP Papers-track
Gabriel Kammer
Kammer, Gabriel
MIT
Pyrosome: Verified Compilation for Modular Metatheory
Matthew Kaney
Kaney, Matthew
Weft—Enabling Tidal on the Web
Byeongjee Kang
Kang, Byeongjee
Carnegie Mellon University
United States
Fray: An Efficient General-Purpose Concurrency Testing Platform for the JVM
Eunsuk Kang
Kang, Eunsuk
Carnegie Mellon University
United States
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Jeehoon Kang
Kang, Jeehoon
FuriosaAI
South Korea
Lilo: A Higher-Order, Relational Concurrent Separation Logic for Liveness
Revamping Verilog Semantics for Foundational Verification
Yiping Kang
Kang, Yiping
University of Michigan
MTP: A Meaning-Typed Language Abstraction for AI-Integrated Programming
Ambrus Kaposi
Kaposi, Ambrus
ELTE Eötvös Loránd University, Budapest, Hungary
Hungary
Session Chair of Dependent Types (part of ICFP Papers)
Type Theory in Type Theory using a Strictified Syntax
Savini Kashmira
Kashmira, Savini
University of Michigan
MTP: A Meaning-Typed Language Abstraction for AI-Integrated Programming
Baris Kasikci
Kasikci, Baris
University of Michigan, USA
Scalable and Accurate Application-level Crash-Consistency Testing via Representative Testing
Jun Kato
Kato, Jun
National Institute of Advanced Industrial Science and Technology (AIST)
Japan
Committee Member in Program Committee within the SPLASH Onward! Papers-track
Joost-Pieter Katoen
Katoen, Joost-Pieter
RWTH Aachen University
Germany
Foundations for Deductive Verification of Continuous Probabilistic Programs: From Lebesgue to Riemann and Back
Hiroyuki Katsura
Katsura, Hiroyuki
University of Cambridge
Automated Catamorphism Synthesis for Solving Constrained Horn Clauses over Algebraic Data Types
Tomer Katz
Katz, Tomer
Technion Israel Institute of Technology
ScooPy: Enhancing Program Synthesis with Nested Example Specifications
Ryan Kavanagh
Kavanagh, Ryan
Université du Québec à Montréal
Canada
Fusing Session-Typed Concurrent Programming into Functional Programming
Alex Kavvos
Kavvos, Alex
University of Bristol
United Kingdom
Adequacy for Algebraic Effects Revisited
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Session Chair of Denotational Semantics (part of ICFP Papers)
Committee Member in ICFP Programme Committee within the ICFP Papers-track
Alex Keizer
Keizer, Alex
University of Cambridge
Interactive Bit Vector Reasoning using Verified Bitblasting
Stephen Kell
Kell, Stephen
King's College London
United Kingdom
Steering Committee Member in Steering Committee for SPLASH 2025
Steering Committee Chair in Onward! Steering Committee within the SPLASH Onward! Essays-track
Steering Committee Member in Onward! Steering Committee within the SPLASH Onward! Essays-track
Session Chair of Onward! Papers and Essay (part of SPLASH Onward! Papers)
Steering Committee Member in Steering Committee within the SPLASH Onward! Papers-track
Martin Kellogg
Kellogg, Martin
New Jersey Institute of Technology
United States
Sponsorship Co-Chair in Organizing Committee for SPLASH 2025
Marie Kerjean
Kerjean, Marie
CNRS, Université Sorbonne Paris Nord
France
Committee Member in ICFP Programme Committee within the ICFP Papers-track
Harun Khan
Khan, Harun
Stanford University
Interactive Bit Vector Reasoning using Verified Bitblasting
Raffi Khatchadourian
Khatchadourian, Raffi
CUNY Hunter College
United States
Committee Member in Program Committee within the SPLASH Onward! Papers-track
Kaustubh Khulbe
Khulbe, Kaustubh
University of Illinois at Urbana-Champaign
End-to-End Compiler Infrastructure for Emerging Tensor Accelerators
Sandra Kiefer
Kiefer, Sandra
University of Oxford
Detecting and explaining (in-)equivalence of context-free grammars
Donguk Kim
Kim, Donguk
South Korea
PAFL: Enhancing Fault Localizers by Leveraging Project-Specific Fault Patterns
Hanjun Kim
Kim, Hanjun
Yonsei University
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Hannuri Kim
Kim, Hannuri
Chungnam National University
Toward Automated Verification of Static Analysis Results of Android Applications
Jaewoo Kim
Kim, Jaewoo
KAIST
South Korea
Revamping Verilog Semantics for Foundational Verification
Jieung Kim
Kim, Jieung
Yonsei University
South Korea
Session Chair of Verification 4 (part of SPLASH OOPSLA)
Jinwoo Kim
Kim, Jinwoo
University of Wisconsin-Madison; Seoul National University
United States
Semantics of Sets of Programs
Zachary Kincaid
Kincaid, Zachary
Princeton University
United States
Software Model Checking via Summary-Guided Search
Elad Kinsbruner
Kinsbruner, Elad
Technion
Israel
Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Marisa Kirisame
Kirisame, Marisa
University of Utah
United States
Incremental Bidirectional Typing via Order Maintenance
Fredrik Kjolstad
Kjolstad, Fredrik
Stanford University
United States
REPTILE: Performant Tiling of Recurrences
Mark Klein
Klein, Mark
Carnegie Mellon University
Quantified Underapproximation via Labeled Bunches
Vasileios Klimis
Klimis, Vasileios
Queen Mary University of London
Shaking Up Quantum Simulators with Fuzzing and Rigour
Naoki Kobayashi
Kobayashi, Naoki
University of Tokyo
Japan
Automated Catamorphism Synthesis for Solving Constrained Horn Clauses over Algebraic Data Types
Mark Koch
Koch, Mark
Quantinuum
Fulls Seldom Differ
Maximilian Kodetzki
Kodetzki, Maximilian
Karlsruhe Institute of Technology
Germany
X-by-Construction: Towards Ensuring Non-Functional Properties in by-Construction Engineering
John C. Kolesar
Kolesar, John C.
Yale University
United States
Coinductive Proofs of Regular Expression Equivalence in Zero Knowledge
Ekaterina Komendantskaya
Komendantskaya, Ekaterina
Heriot-Watt University and Southampton University
United Kingdom
Proof-Carrying Neuro-Symbolic Code
Paulette Koronkevich
Koronkevich, Paulette
University of British Columbia
Type-Preserving Flat Closure Optimization
Type Universes as Kripke Worlds
Eric Koskinen
Koskinen, Eric
Stevens Institute of Technology
United States
Abstract Interpretation of Temporal Safety Effects of Higher Order Programs
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Nikita Koval
Koval, Nikita
JetBrains
Netherlands
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Concurrent Algorithms under the hood of Kotlin Coroutines
Testing concurrent code on JVM with Lincheck
András Kovács
Kovács, András
University of Gothenburg and Chalmers University of Technology
Committee Member in ICFP Programme Committee within the ICFP Papers-track
Laura Kovács
Kovács, Laura
TU Wien
Austria
Divide and Conquer: A Compositional Approach to Game-Theoretic Security
Gintas Kraptavičius
Kraptavičius, Gintas
Concert: Merzmania
Anastasiya Kravchuk-Kirilyuk
Kravchuk-Kirilyuk, Anastasiya
Harvard University
United States
Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Robbert Krebbers
Krebbers, Robbert
Radboud University Nijmegen
Netherlands
Verified Interpreters for Dynamic Languages with Applications to the Nix Expression Language
V Krishna Nandivada
Krishna Nandivada, V
IIT Madras
Session Chair of Analysis 2 (part of SPLASH OOPSLA)
IncIDFA: An Efficient and Generic Algorithm for Incremental Iterative Dataflow Analysis
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Shriram Krishnamurthi
Krishnamurthi, Shriram
Brown University
United States
Steering Committee Member in Steering Committee for SPLASH 2025
OOPSLA Review Committee Co-Chair in Organizing Committee for SPLASH 2025
Session Chair of Saturday SPLASH Keynote (part of SPLASH Keynotes)
RC Chair Report
OOPSLA Awards
Co-chair in OOPSLA Review Committee within the SPLASH OOPSLA-track
Sharing is Scaring: Linking Cloud File-Sharing to Programming Language Semantics
Porpoise: An LLM-Based Sandbox for Novices to Practice Writing Purpose Statements
A guided tour through Oxidized OCaml
Paul Krogmeier
Krogmeier, Paul
University of Illinois at Urbana-Champaign
United States
Synthesizing DSLs for Few-Shot Learning
Sachit Kuhar
Kuhar, Sachit
Amazon Web Services
UTFix: Change Aware Unit Test Repairing using LLM
Iona Kuhn
Kuhn, Iona
Saarland University
Germany
Almost Fair Simulations
Burcu Kulahcioglu Ozkan
Kulahcioglu Ozkan, Burcu
Delft University of Technology
Netherlands
Model-guided Fuzzing of Distributed Systems
Kouta Kumamoto
Kumamoto, Kouta
An Interactive Learning Environment for Program Design
Lindsey Kuper
Kuper, Lindsey
University of California, Santa Cruz
United States
Exploring the Theory and Practice of Concurrency in the Entity-Component-System Pattern
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
CRDT Emulation, Simulation, and Representation Independence
Ivan Kuraj
Kuraj, Ivan
Massachusetts Institute of Technology
Peepco: Batch-Based Consistency Optimization
Ismail Kuru
Kuru, Ismail
Drexel University
United States
Modal Abstractions for Virtualizing Memory Addresses
Christian Kästner
Kästner, Christian
Carnegie Mellon University
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Filip Křikava
Křikava, Filip
Czech Technical University in Prague
Czechia
Rebase Chair in Organizing Committee for SPLASH 2025
Ambroise Lafont
Lafont, Ambroise
Inria, France
2-Functoriality of Initial Semantics, and Applications
Patrick LaFontaine
LaFontaine, Patrick
Purdue University
United States
We’ve Got You Covered: Type-Guided Repair of Incomplete Input Generators
Ignacio Laguna
Laguna, Ignacio
Lawrence Livermore National Laboratory
United States
Synthesizing Sound and Precise Abstract Transformers for Nonlinear Hyperbolic PDE Solvers
Shuvendu K. Lahiri
Lahiri, Shuvendu K.
Microsoft Research
United States
AutoVerus: Automated Proof Generation for Rust Code
Sumit Lahiri
Lahiri, Sumit
Indian Institute of Technology Kanpur
India
Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Cheuk Tung LAI
LAI, Cheuk Tung
VX Research Limited
United Kingdom
Extraction and Mutation at a High Level: Template-Based Fuzzing for JavaScript Engines
Jianxin Lai
Lai, Jianxin
Ant Group
MetaKernel: Enabling Efficient Encrypted Neural Network Inference Through Unified MVM and Convolution
Akash Lal
Lal, Akash
Microsoft Research
India
Memory-Safety Verification of Open Programs With Angelic Assumptions
Kait Lam
Lam, Kait
Defence Science and Technology Group / School of EECS, University of Queensland
Translation Validation for LLVM's AArch64 Backend
Patrick Lam
Lam, Patrick
University of Waterloo
Committee Member in Program Committee within the SPLASH Onward! Papers-track
Ada Lamba
Lamba, Ada
Ohio State University
Carapace: Static–Dynamic Information Flow Control in Rust
Thomas Lamiaux
Lamiaux, Thomas
University of Paris-Saclay, Ens Paris-Saclay
2-Functoriality of Initial Semantics, and Applications
Leonidas Lampropoulos
Lampropoulos, Leonidas
University of Maryland, College Park
Greece
Compositional Quantum Control Flow with Efficient Compilation in Qunity
Yingjun Lan
Lan, Yingjun
Formal Verification of Graham's Scan Algorithm
Jens Kanstrup Larsen
Larsen, Jens Kanstrup
DTU
Denmark
Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Jacob Laurel
Laurel, Jacob
Georgia Institute of Technology
United States
Synthesizing Sound and Precise Abstract Transformers for Nonlinear Hyperbolic PDE Solvers
Precise Abstract Interpretation of Probabilistic Programs with Interval Data Uncertainty
Jonathan Laurent
Laurent, Jonathan
Carnegie Mellon University / Karlsruhe Institute of Technology
Adaptive Shielding via Parametric Safety Proofs
Tom Lauwaerts
Lauwaerts, Tom
Universiteit Gent, Belgium
Belgium
MIO: Multiverse Debugging in the face of Input/Output
Tony Law
Law, Tony
Univ Rennes, Inria, CNRS, IRISA
A Mechanized Semantics for Dataflow Circuits
Julia Lawall
Lawall, Julia
Inria
France
Automating maintenance of the Linux kernel: a perspective over 20 years
Alan Lawrence
Lawrence, Alan
Quantinuum
Fulls Seldom Differ
Isabella Laybourn
Laybourn, Isabella
Carnegie Mellon University
United States
Fray: An Efficient General-Purpose Concurrency Testing Platform for the JVM
Tristan Le Gall
Le Gall, Tristan
CEA LIST
Verifying Neural Networks with PyRAT
Quang Loc Le
Le, Quang Loc
University College London
United Kingdom
Committee Member in Program Committee within the SAS -track
Van-Hoang Le
Le, Van-Hoang
The University of Newcastle
Australia
Committee Member in Review Committee within the SPLASH Student Research Competition-track
Doug Lea
Lea, Doug
State University of New York (SUNY) Oswego
United States
Soundness of Predictive Concurrency Analyses
Ashley Lee
Lee, Ashley
University of California, Santa Cruz
SafeRace: Assessing and Addressing WebGPU Memory Safety in the Presence of Data Races
Dongjae Lee
Lee, Dongjae
Massachusetts Institute of Technology
Lilo: A Higher-Order, Relational Concurrent Separation Logic for Liveness
Edward Lee
Lee, Edward
University of Toronto at Scarborough
Canada
Qualified Types with Boolean Algebras
HYEONJIN LEE
LEE, HYEONJIN
On A Multitier Actor Programming Language
Jaeseo Lee
Lee, Jaeseo
POSTECH
South Korea
Formal Analysis of Networked PLC Controllers Interacting with Physical Environments
Janggun Lee
Lee, Janggun
KAIST
Lilo: A Higher-Order, Relational Concurrent Separation Logic for Liveness
Jay Lee
Lee, Jay
Seoul National University
South Korea
React-tRace: A Semantics for Understanding React Hooks
Juneyoung Lee
Lee, Juneyoung
AWS
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Keonho Lee
Lee, Keonho
University of California, Irvine
Towards Verifying Crash Consistency
Leo Seojun Lee
Lee, Leo Seojun
University of Oxford
United Kingdom
Mind the Abstraction Gap: Bringing Equality Saturation to Real-World ML Compilers
Shaun Christopher Lee
Lee, Shaun Christopher
University of Washington
Scalable and Accurate Application-level Crash-Consistency Testing via Representative Testing
Sungho Lee
Lee, Sungho
Chungnam National University, Korea
South Korea
Simplifying Lifter-generated Emulation Style LLVM IR for Analysis Suitability
Type Checking for Python Using Intersection Types
Toward Automated Verification of Static Analysis Results of Android Applications
Woosuk Lee
Lee, Woosuk
Hanyang University
South Korea
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Yunjeong Lee
Lee, Yunjeong
National University of Singapore
Singapore
Student Volunteer Co-Chair in Organizing Committee for SPLASH 2025
Zheng Han Lee
Lee, Zheng Han
National University of Singapore, Singapore
Efficient Decrease-And-Conquer Linearizability Monitoring
Owolabi Legunsen
Legunsen, Owolabi
Cornell University
United States
Session Chair of Testing 2 (part of SPLASH OOPSLA)
Faster Explicit-Trace Monitoring-Oriented Programming for Runtime Verification of Software Tests
Julien Lehmann
Lehmann, Julien
CEA, LIST, France
France
Verifying Neural Networks with PyRAT
Daan Leijen
Leijen, Daan
Microsoft Research
United States
Committee Member in Program Committee within the SPLASH Onward! Papers-track
First-Order Laziness
Augustin Lemesle
Lemesle, Augustin
CEA, LIST, France
Verifying Neural Networks with PyRAT
Caroline Lemieux
Lemieux, Caroline
University of British Columbia
Canada
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Damitha Lenadora
Lenadora, Damitha
University of Illinois at Urbana-Champaign
GALA: A High Performance Graph Neural Network Acceleration LAnguage and Compiler
Connor Lenihan
Lenihan, Connor
King's College London
Shaking Up Quantum Simulators with Fuzzing and Rigour
AccelerQ: Accelerating Quantum Eigensolvers With Machine Learning on Quantum Simulators
Sorin Lerner
Lerner, Sorin
University of California at San Diego
United States
Committee Member in Program Committee within the SPLASH Onward! Papers-track
Mohsen Lesani
Lesani, Mohsen
University of California at Santa Cruz
Hambazi: Spatial Coordination Synthesis for Augmented Reality
Martin Lester
Lester, Martin
University of Reading
United Kingdom
Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Danya Lette
Lette, Danya
Committee Member in SAS Artifact Evaluation Committee within the SAS Artifact-track
Kyla H. Levin
Levin, Kyla H.
University of Massachusetts Amherst, USA
United States
RestPi: Path-Sensitive Type Inference for REST APIs
Reese Levine
Levine, Reese
SafeRace: Assessing and Addressing WebGPU Memory Safety in the Presence of Data Races
Nicholas V. Lewchenko
Lewchenko, Nicholas V.
University of Colorado Boulder
United States
Bolt-On Strong Consistency: Specification, Implementation, and Verification
Ondřej Lhoták
Lhoták, Ondřej
University of Waterloo
Canada
Flix: A Design for Language-Integrated Datalog
Qualified Types with Boolean Algebras
Angela W. Li
Li, Angela W.
Rice University
Efficient Algorithms for the Uniform Tokenization Problem
Ao Li
Li, Ao
Carnegie Mellon University
United States
Fray: An Efficient General-Purpose Concurrency Testing Platform for the JVM
Baichuan Li
Li, Baichuan
University of Michigan
MTP: A Meaning-Typed Language Abstraction for AI-Integrated Programming
Baixuan Li
Li, Baixuan
School of Computer Science and Engineering, College of Software Engineering, School of Artifical Intelligence, Southeast University
ABC: Towards a Universal Code Styler through Model Merging
Chenxi Li
Li, Chenxi
Nanjing University, China
Two Approaches to Fast Bytecode Frontend for Static Analysis
Chenxing Li
Li, Chenxing
Shanghai Tree-Graph Blockchain Research Institute
China
HEMVM: a Heterogeneous Blockchain Framework for Interoperable Virtual Machines
Ding Li
Li, Ding
Peking University
China
Orax: A Feedback-Driven Framework for Efficiently Solving Satisfiability Modulo Theories and Oracles
Elaine Li
Li, Elaine
NYU
United States
Characterizing Implementability of Global Protocols with Infinite States and Data
Guanyan Li
Li, Guanyan
University of Oxford
Structural Abstraction and Refinement for Probabilistic Programs
Haofeng Li
Li, Haofeng
SKLP, Institute of Computing Technology, CAS
China
Fast Client-Driven CFL-Reachability via Regularization-Based Graph Simplification
Haoran Li
Li, Haoran
Shanghai Jiao Tong University
Binary Cryptographic Function Identification via Similarity Analysis with Path-insensitive Emulation
Jianlin Li
Li, Jianlin
University of Waterloo
Canada
Compiling with Generating Functions
John Li
Li, John
Northeastern University
United States
Multi-Language Probabilistic Programming
From Linearity to Borrowing
Juanen Li
Li, Juanen
Beijing Normal University
Structural Abstraction and Refinement for Probabilistic Programs
Kwing Hei Li
Li, Kwing Hei
Aarhus University
Denmark
Separation Logics for Probability, Concurrency, and Security
Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs
Lian Li
Li, Lian
Institute of Computing Technology at Chinese Academy of Sciences; University of Chinese Academy of Sciences
China
Fast Client-Driven CFL-Reachability via Regularization-Based Graph Simplification
Liyi Li
Li, Liyi
Iowa State University
United States
Embedding Quantum Program Verification into Dafny
A Haskell Adiabatic DSL: Solving Classical Optimization Problems on Quantum Hardware
Long Li
Li, Long
Ant Group
MetaKernel: Enabling Efficient Encrypted Neural Network Inference Through Unified MVM and Convolution
Mingyi Li
Li, Mingyi
Institute of Computing Technology, CAS
China
Stencil-Lifting: Hierarchical Recursive Lifting System for Extracting Summary of Stencil Kernel in Legacy Codes
Peilun Li
Li, Peilun
Shanghai Tree-Graph Blockchain Research Institute
HEMVM: a Heterogeneous Blockchain Framework for Interoperable Virtual Machines
Shangyu Li
Li, Shangyu
The Hong Kong University of Science and Technology
A Sound Static Analysis Approach to I/O API Migration
Shaohua Li
Li, Shaohua
The Chinese University of Hong Kong
Hong Kong SAR China
An Empirical Study of Bugs in the rustc Compiler
Interleaving Large Language Models for Compiler Testing
Tianchi Li
Li, Tianchi
Peking University, China
China
Combining Formal and Informal Information in Bayesian Program Analysis via Soft Evidences
Xuandong Li
Li, Xuandong
Nanjing University
China
HybridPersist: A Compiler Support for User-Friendly and Efficient PM Programming
TailTracer: Continuous Tail Tracing for Production Use
PReMM: LLM-Based Program Repair for Multi-Method Bugs via Divide and Conquer
Towards a Theoretically-Backed and Practical Framework for Selective Object-Sensitive Pointer Analysis
Xuheng Li
Li, Xuheng
Columbia University
AutoVerus: Automated Proof Generation for Rust Code
Yi Li
Li, Yi
Nanyang Technological University
Singapore
TailTracer: Continuous Tail Tracing for Production Use
Yihe Li
Li, Yihe
National University of Singapore
Large Language Model powered Symbolic Execution
Yue Li
Li, Yue
Nanjing University
China
Two Approaches to Fast Bytecode Frontend for Static Analysis
Co-chair in SAS Artifact Evaluation Committee within the SAS Artifact-track
Zhong Li
Li, Zhong
Nanjing University
China
PReMM: LLM-Based Program Repair for Multi-Method Bugs via Divide and Conquer
Qihao Lian
Lian, Qihao
Peking University
China
Automatic Linear Resource Bound Analysis for Rust via Prophecy Potentials
Peng Liang
Liang, Peng
Wuhan University, China
China
Finding Compiler Bugs through Cross-Language Code Generator and Differential Testing
Nathan Liittschwager
Liittschwager, Nathan
University of California, Santa Cruz
CRDT Emulation, Simulation, and Representation Independence
Anthony Widjaja Lin
Lin, Anthony Widjaja
RPTU Kaiserslautern-Landau and Max-Planck Institute for Software Systems
The Power of Regular Constraint Propagation
Haoran Lin
Lin, Haoran
Nanjing University, China
Two Approaches to Fast Bytecode Frontend for Static Analysis
Jenny Han Lin
Lin, Jenny Han
University of Utah
United States
Polynomial-Time Program Equivalence for Machine Knitting
Youfang Lin
Lin, Youfang
Beijing Jiaotong University
Fuzzing C++ Compilers via Type-Driven Mutation
Sam Lindley
Lindley, Sam
University of Edinburgh
United Kingdom
Modal Effect Types
First-Order Laziness
Teodors Lisovenko
Lisovenko, Teodors
Ca' Foscari University of Venice
Italy
Committee Member in SAS Artifact Evaluation Committee within the SAS Artifact-track
Kyle Little
Little, Kyle
University of Utah
SafeRace: Assessing and Addressing WebGPU Memory Safety in the Presence of Data Races
Amanda Liu
Liu, Amanda
Massachusetts Institute of Technology
United States
Gauguin, Descartes, Bayes: A Diurnal Golem's Brain
Cyrus Liu
Liu, Cyrus
Samsung Semiconductor
United States
Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Hanzhi Liu
Liu, Hanzhi
University of California, Santa Barbara & Riema Labs
United States
Tabby: A Synthesis-Aided Compiler for High-Performance Zero-Knowledge Proof Circuits
Jie Liu
Liu, Jie
ByteDance
China
Committee Member in SAS Artifact Evaluation Committee within the SAS Artifact-track
Junrui Liu
Liu, Junrui
University of California, Santa Barbara
United States
Tabby: A Synthesis-Aided Compiler for High-Performance Zero-Knowledge Proof Circuits
Kui Liu
Liu, Kui
Huawei
China
PReMM: LLM-Based Program Repair for Multi-Method Bugs via Divide and Conquer
Lang Liu
Liu, Lang
Illinois Institute of Technology
Quantified Underapproximation via Labeled Bunches
Shuyang Liu
Liu, Shuyang
Soundness of Predictive Concurrency Analyses
Tianyi Liu
Liu, Tianyi
Nanjing University
China
TailTracer: Continuous Tail Tracing for Production Use
Xinxin Liu
Liu, Xinxin
Institute of software, Chinese academy of sciences
HpC: A Calculus for Hybrid and Mobile Systems
Yan Liu
Liu, Yan
Ant Group
MetaKernel: Enabling Efficient Encrypted Neural Network Inference Through Unified MVM and Convolution
Yang Liu
Liu, Yang
Nanyang Technological University
Singapore
[Closed Session] Adjudication meeting for SIGPLAN's John Vlissides award
Committee Member in Program Committee and Panel within the SPLASH Doctoral Symposium-track
Yue Liu
Liu, Yue
Data61, CSIRO
Committee Member in Review Committee within the SPLASH Student Research Competition-track
Zixi Liu
Liu, Zixi
Nanjing University
China
An Empirical Study of Bugs in the rustc Compiler
Francesco Logozzo
Logozzo, Francesco
Meta
United States
Revealing Sources of (Memory) Errors via Backward Analysis
Debasmita Lohar
Lohar, Debasmita
Karlsruhe Institute of Technology
Germany
Cost of Soundness in Mixed-Precision Tuning
Tommie Lombarts
Lombarts, Tommie
Eindhoven University of Technology
Personalization of Programming Education: An NLP-based Bi-dimensional Classification of Programming Exercises
Fan Long
Long, Fan
University of Toronto
Canada
HEMVM: a Heterogeneous Blockchain Framework for Interoperable Virtual Machines
Huan Long
Long, Huan
Shanghai Jiao Tong University
A Programming Language for Feasible Solutions
Nuno P. Lopes
Lopes, Nuno P.
INESC-ID; Instituto Superior Técnico - University of Lisbon
Portugal
Translation Validation for LLVM's AArch64 Backend
Jacob R. Lorch
Lorch, Jacob R.
Microsoft Research, n.n.
AutoVerus: Automated Proof Generation for Rust Code
Anton Lorenzen
Lorenzen, Anton
University of Edinburgh
United Kingdom
Modal Effect Types
First-Order Laziness
Yiling Lou
Lou, Yiling
University of Illinois at Urbana-Champaign
United States
Show Me Why It's Correct: Saving 1/3 of Debugging Time in Program Repair with Interactive Runtime Comparison
Jiayi Lu
Lu, Jiayi
Zhejiang University
A complete formal semantics of eBPF instruction set architecture for Solana
Jie Lu
Lu, Jie
SKLP, Institute of Computing Technology, CAS, China
Fast Client-Driven CFL-Reachability via Regularization-Based Graph Simplification
Longlong Lu
Lu, Longlong
State Key Laboratory for Novel Software Technology, Nanjing University, China
Towards a Theoretically-Backed and Practical Framework for Selective Object-Sensitive Pointer Analysis
Shan Lu
Lu, Shan
Microsoft; University of Chicago
United States
AutoVerus: Automated Proof Generation for Rust Code
Shuai Lu
Lu, Shuai
Microsoft Research
China
AutoVerus: Automated Proof Generation for Rust Code
Sirui Lu
Lu, Sirui
OpenAI
United States
HieraSynth: A Parallel Framework for Complete Super-Optimization with Hierarchical Space Decomposition
Yifei Lu
Lu, Yifei
State Key Laboratory for Novel Software Technology, Nanjing University, China
Towards a Theoretically-Backed and Practical Framework for Selective Object-Sensitive Pointer Analysis
Yunping Lu
Lu, Yunping
Fudan University
JavART: a Lightweight Rule-Based JIT Compiler Using Translation Rules Extracted from a Learning Approach
Mingyuan Luo
Luo, Mingyuan
Fudan University
ApkDiffer: Accurate and Scalable Cross-Version Diffing Analysis for Android Applications
Ning Luo
Luo, Ning
UIUC
United States
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Matthew Lutze
Lutze, Matthew
Aarhus University
The Simple Essence of Monomorphization
Type-safe Blazon - Enforcing Pedantry in Heraldic Design
Pedro López-García
López-García, Pedro
IMDEA Software Institute
Committee Member in Program Committee within the SAS -track
Júnior Löff
Löff, Júnior
Università della Svizzera italiana
HeapBuffers: Why not just using a binary serialization format for your managed memory?
Andreas Lööw
Lööw, Andreas
Imperial College London
United Kingdom
The Simulation Semantics of Synthesisable Verilog
Compositional Symbolic Execution for the Next 700 Memory Models
Chenyang Ma
Ma, Chenyang
Nanjing University of Science and Technology
DepFuzz: Efficient Smart Contract Fuzzing with Function Dependence Guidance
Cong Ma
Ma, Cong
University of Waterloo
Canada
Lexical Effect Handler: Fast by Design, Correct by Proof
Zero-Overhead Lexical Effect Handlers
Hui Ma
Ma, Hui
Institute of Computing Technology, Chinese Academy of Sciences
Stencil-Lifting: Hierarchical Recursive Lifting System for Extracting Summary of Stencil Kernel in Legacy Codes
Xiaofei Ma
Ma, Xiaofei
AWS AI Labs
UTFix: Change Aware Unit Test Repairing using LLM
Xiaotian Ma
Ma, Xiaotian
Nanjing University of Science and Technology
China
Finding Compiler Bugs through Cross-Language Code Generator and Differential Testing
Zhongkui Ma
Ma, Zhongkui
The University of Queensland
Australia
Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Convex Hull Approximation for Activation Functions
Aravind Machiry
Machiry, Aravind
Purdue University
United States
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Julian Mackay
Mackay, Julian
Kry10 Ltd
Reasoning about External Calls
Stefan Mada
Mada, Stefan
University of Utah
Translation Validation for LLVM's AArch64 Backend
Anil Madhavapeddy
Madhavapeddy, Anil
University of Cambridge, UK
United Kingdom
A guided tour through Oxidized OCaml
Functional Networking for Millions of Docker Desktops (Experience Report)
P. Madhusudan
Madhusudan, P.
University of Illinois at Urbana-Champaign
United States
FO-Complete Program Verification for Heap Logics
Synthesizing DSLs for Few-Shot Learning
Jean-Marie Madiot
Madiot, Jean-Marie
Inria
France
Formal Semantics and Program Logics for a Fragment of OCaml
Magnus Madsen
Madsen, Magnus
Aarhus University
Denmark
Flix: A Design for Language-Integrated Datalog
Qualified Types with Boolean Algebras
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Committee Member in Program Committee within the SPLASH Onward! Papers-track
Ole Lehrmann Madsen
Madsen, Ole Lehrmann
Aarhus University
Denmark
Committee Member in Program Committee within the SPLASH Onward! Papers-track
Enrico Magnago
Magnago, Enrico
Amazon Web Services
Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Romina Mahinpei
Mahinpei, Romina
Princeton University
Interactive Theorem Provers for Proof Education
Daryl Maier
Maier, Daryl
IBM Canada
Canada
CoSSJIT: Combining Static Analysis and Speculation in JIT Compilers
Kenji Maillard
Maillard, Kenji
Inria – LS2N, Université de Nantes
France
Incremental Certified Programming
Rupak Majumdar
Majumdar, Rupak
MPI-SWS
Germany
Model-guided Fuzzing of Distributed Systems
Caleb Malchik
Malchik, Caleb
Yale University
On Collective Control over User Interfaces in the Face of Network Effects
Konstantinos Mamouras
Mamouras, Konstantinos
Rice University
United States
Efficient Algorithms for the Uniform Tokenization Problem
Wensen Mao
Mao, Wensen
Rutgers University
Abstraction Refinement-guided Program Synthesis for Robot Learning from Demonstrations
Michaël Marcozzi
Marcozzi, Michaël
Université Paris-Saclay, CEA, List
France
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Dylan Marinho
Marinho, Dylan
Sorbonne Université, CNRS UMR 7606, LIP6, Paris, France
France
Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Oliver Markgraf
Markgraf, Oliver
RPTU Kaiserslautern-Landau
The Power of Regular Constraint Propagation
Petros Markopoulos
Markopoulos, Petros
Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Stefan Marr
Marr, Stefan
Johannes Kepler University Linz
Austria
Session Chair of Debugging and Validation (part of SPLASH OOPSLA)
Session Chair of Runtime (part of SPLASH OOPSLA)
Divining Profiler Accuracy: An Approach to Approximate Profiler Accuracy Through Machine Code-Level Slowdown
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Jason Mars
Mars, Jason
University of Michigan
MTP: A Meaning-Typed Language Abstraction for AI-Integrated Programming
Brianna Marshall
Marshall, Brianna
Northeastern University
United States
From Linearity to Borrowing
Chris Martens
Martens, Chris
Northeastern University
United States
PC Member in Program Committee within the SPLASH Onward! Essays-track
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Ruben Martins
Martins, Ruben
Carnegie Mellon University
United States
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Guido Martínez
Martínez, Guido
Microsoft Research
United States
SecRef*: Securely Sharing Mutable References between Verified and Unverified Code in F*
Kristóf Marussy
Marussy, Kristóf
Budapest University of Technology and Economics
Hungary
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Isabella Mastroeni
Mastroeni, Isabella
University of Verona
Italy
Relating Distances and Abstractions: An Abstract Interpretation Perspective
Hidehiko Masuhara
Masuhara, Hidehiko
Institute of Science Tokyo
Japan
Steering Committee Member in Onward! Steering Committee within the SPLASH Onward! Essays-track
Session Chair of Compilation 3 (part of SPLASH OOPSLA)
Session Chair of Compilation 1 (part of SPLASH OOPSLA)
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Session Chair of Concurrency (part of SPLASH Onward! Papers)
Committee Member in Program Committee within the SPLASH Onward! Papers-track
Steering Committee Member in Steering Committee within the SPLASH Onward! Papers-track
An Interactive Learning Environment for Program Design
Daisy: An Exercise Environment for Learning Information Modeling
Sebastian Mateos Nicolajsen
Mateos Nicolajsen, Sebastian
IT University of Copenhagen
Denmark
Committee Member in Program Commitee within the SPLASH -E-track
Umang Mathur
Mathur, Umang
National University of Singapore
Singapore
Efficient Decrease-And-Conquer Linearizability Monitoring
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
View Types in Rust
Damiano Mazza
Mazza, Damiano
CNRS, LIPN, Université Sorbonne Paris Nord
France
Committee Member in ICFP Programme Committee within the ICFP Papers-track
Riccardo Mazza
Mazza, Riccardo
APM Saluzzo
Italy
Sonic Earth - An Algorithmic Performance Approach to Real-Time Environmental Sonification
Concert: Sonic Earth
Conor McBride
McBride, Conor
University of Strathclyde
Fulls Seldom Differ
James McCann
McCann, James
Carnegie Mellon University
United States
Committee Member in Program Committee within the SPLASH FARM-track
Polynomial-Time Program Equivalence for Machine Knitting
Kathryn S McKinley
McKinley, Kathryn S
Google
Advancing Performance via a Systematic Application of Research and Industrial Best Practice
Work Packets: A New Abstraction for GC Software Engineering, Optimization, and Innovation
Michael McLoughlin
McLoughlin, Michael
Carnegie Mellon University
United States
Scaling Instruction-Selection Verification against Authoritative ISA Semantics
S Hessam M Mehr
Mehr, S Hessam M
University of Glasgow
TideScript: A Domain Specific Language for Peptide Chemistry
Vaibhav Mehta
Mehta, Vaibhav
Cornell University
United States
A Hoare Logic For Symmetry Properties
Antero Mejr
Mejr, Antero
Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Olivier Melançon
Melançon, Olivier
Université de Montréal
Canada
Float Self-Tagging
Stephen Mell
Mell, Stephen
University of Pennsylvania
Opportunistically Parallel Lambda Calculus
Guillaume Melquiond
Melquiond, Guillaume
Université Paris-Saclay - CNRS - ENS Paris-Saclay - Inria
France
Committee Member in ICFP Programme Committee within the ICFP Papers-track
Charith Mendis
Mendis, Charith
University of Illinois at Urbana-Champaign
United States
Automated Verification of Soundness of DNN Certifiers
GALA: A High Performance Graph Neural Network Acceleration LAnguage and Compiler
SPLAT: A framework for optimised GPU code-generation for SParse reguLar ATtention
End-to-End Compiler Infrastructure for Emerging Tensor Accelerators
Eagon Meng
Meng, Eagon
MIT
What You See Is What It Does: A Structural Pattern for Legible Software
Ruijie Meng
Meng, Ruijie
National University of Singapore, Singapore
Singapore
Large Language Model powered Symbolic Execution
Mira Mezini
Mezini, Mira
TU Darmstadt; hessian.AI; National Research Center for Applied Cybersecurity ATHENE
Germany
Steering Committee Member in Steering Committee for SPLASH 2025
Benjamin Mikek
Mikek, Benjamin
Georgia Institute of Technology
Towards Compiler-Guided Static Analysis
Mae Milano
Milano, Mae
Princeton University
United States
Interactive Theorem Provers for Proof Education
Session Chair of Performance Evening (part of SPLASH FARM)
Session Chair of Math and Music (part of SPLASH FARM)
Session Chair of Functional Programming (part of SPLASH FARM)
Session Chair of Language Design (part of SPLASH FARM)
General Chair in Organizing Committee within the SPLASH FARM-track
Session Chair of LGBTQ Lunch (part of ICFP Diversity, Equity, and Inclusion)
Stefan Milius
Milius, Stefan
Friedrich-Alexander University Erlangen-Nürnberg
Germany
Bialgebraic Reasoning on Stateful Languages
Heather Miller
Miller, Heather
Carnegie Mellon University and Two Sigma
Debugging WebAssembly? Put some Whamm on it!
Todd Millstein
Millstein, Todd
University of California at Los Angeles
United States
Tuning Random Generators: Property-Based Testing as Probabilistic Programming
Synthesizing Implication Lemmas for Interactive Theorem Proving
Tijana Minić
Minić, Tijana
Derivation Visualization for Context-Free Grammar Design: Helping Students Understand Context-Free Grammars
Mikhail Mints
Mints, Mikhail
California Institute of Technology
United States
Compositional Quantum Control Flow with Efficient Compilation in Qunity
Antoine Miné
Miné, Antoine
Sorbonne Université
France
Committee Member in Program Committee within the SAS -track
Sasa Misailovic
Misailovic, Sasa
University of Illinois at Urbana-Champaign
United States
Workshop Co-Chair in Organizing Committee for SPLASH 2025
Workshops Co-Chair in Workshop Selection Committee within the ICFP/SPLASH Workshops-track
Precise Abstract Interpretation of Probabilistic Programs with Interval Data Uncertainty
Ashish Mishra
Mishra, Ashish
IIT Hyderabad
India
Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
We’ve Got You Covered: Type-Guided Repair of Incomplete Input Generators
Committee Member in Program Committee within the SAS -track
Md Rakib Hossain Misu
Misu, Md Rakib Hossain
University of California Irvine
United States
AutoVerus: Automated Proof Generation for Rust Code
Sidi Mohamed Beillahi
Mohamed Beillahi, Sidi
University of Toronto
Canada
HEMVM: a Heterogeneous Blockchain Framework for Interoperable Virtual Machines
Committee Member in Program Committee within the SAS -track
Abdalrhman Mohamed
Mohamed, Abdalrhman
Stanford University
Interactive Bit Vector Reasoning using Verified Bitblasting
Isidore Mohr
Mohr, Isidore
Concert: Girard’s Paradox
Girard's Paradox as Structure Music
Alexandre Moine
Moine, Alexandre
New York University
United States
Committee Member in ICFP Programme Committee within the ICFP Papers-track
Evgenii Moiseenko
Moiseenko, Evgenii
JetBrains Research
Testing concurrent code on JVM with Lincheck
Abtin Molavi
Molavi, Abtin
University of Wisconsin-Madison
Dependency-Aware Compilation for Surface Code Quantum Architectures
Compiling Quantum Circuits
Raphaël Monat
Monat, Raphaël
Inria and University of Lille
France
Committee Member in Program Committee within the SAS -track
Fabrizio Montesi
Montesi, Fabrizio
University of Southern Denmark
Denmark
Relax! The Semilenient Core of Choreographic Programming (Functional Pearl)
Arjan J. Mooij
Mooij, Arjan J.
Zürich University of Applied Sciences
Language-Parametric Reference Synthesis
David Moon
Moon, David
University of Michigan
United States
Syntactic Completions with Material Obligations
José Morales
Morales, José
IMDEA Software Institute
Spain
Committee Member in Steering Committee within the SAS -track
Angelica Moreira
Moreira, Angelica
Microsoft Research
Canada
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Gabriel A. Moreno
Moreno, Gabriel A.
Carnegie Mellon University Software Engineering Institute
United States
Quantified Underapproximation via Labeled Bunches
Nicholas Morris
Morris, Nicholas
University of Glasgow
TideScript: A Domain Specific Language for Peptide Chemistry
Cameron Moy
Moy, Cameron
Northeastern University
United States
Teaching Software Specification (Experience Report)
Fabian Muehlboeck
Muehlboeck, Fabian
Australian National University
Australia
View Types in Rust
Eric Mugnier
Mugnier, Eric
University of California San Diego
On the Impact of Formal Verification on Software Development
Laurel: Unblocking Automated Verification with Large Language Models
Serkan Muhcu
Muhcu, Serkan
Technische Universität Berlin
Multiple Resumptions and Local Mutable State, Directly
Prasita Mukherjee
Mukherjee, Prasita
Purdue University
KestRel: Relational Verification Using E-Graphs for Program Alignment
Adithya Murali
Murali, Adithya
University of Illinois at Urbana-Champaign
United States
FO-Complete Program Verification for Heap Logics
Charlie Murphy
Murphy, Charlie
Amazon Web Services, USA
United States
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Gail Murphy
Murphy, Gail
University of British Columbia
Canada
An Exploration of How Generative AI Affects Workflow and Collaboration in a Software Engineering Course
Andrew Myers
Myers, Andrew
Cornell University
SIGPLAN Chair in Steering Committee for SPLASH 2025
Anders Møller
Møller, Anders
Aarhus University
Denmark
SIGPLAN Vice Chair in Steering Committee for SPLASH 2025
Marius Müller
Müller, Marius
University of Tübingen
Germany
Compiling Classical Sequent Calculus to Stock Hardware: The Duality of Compilation
Peter Müller
Müller, Peter
ETH Zurich
Switzerland
Place Capability Graphs: A General-Purpose Model of Rust’s Ownership and Borrowing Guarantees
Modular Reasoning about Global Variables and Their Initialization
A Refinement Methodology for Distributed Programs in Rust
Ritam Nag
Nag, Ritam
MIT
Pyrosome: Verified Compilation for Modular Metatheory
Kartik Nagar
Nagar, Kartik
IIT Madras
India
Automatically Verifying Replication-aware Linearizability
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Santosh Nagarakatte
Nagarakatte, Santosh
Rutgers University
United States
Comparing the Precision of Abstract Operators in the eBPF Verifier using Differential Synthesis
Srinidhi Nagendra
Nagendra, Srinidhi
IRIF, Chennai Mathematical Institute
France
Model-guided Fuzzing of Distributed Systems
Shaan Nagy
Nagy, Shaan
University of Wisconsin-Madison
Semantics of Sets of Programs
Tomoki Nakamaru
Nakamaru, Tomoki
The University of Tokyo
Japan
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Kedar Namjoshi
Namjoshi, Kedar
Nokia Bell Labs
United States
Committee Member in Steering Committee within the SAS -track
Chandrakana Nandi
Nandi, Chandrakana
Certora
United States
Formalizing Linear Motion G-code for Invariant Checking and Differential Testing of Fabrication Tools
Workshops Co-Chair in Workshop Selection Committee within the ICFP/SPLASH Workshops-track
Aleksandar Nanevski
Nanevski, Aleksandar
IMDEA Software Institute
Spain
Verifying Graph Algorithms in Separation Logic: A Case for an Algebraic Approach
Daniele Nantes-Sobrinho
Nantes-Sobrinho, Daniele
Imperial College London
United Kingdom
Compositional Symbolic Execution for the Next 700 Memory Models
Srinivas Narayana
Narayana, Srinivas
Rutgers University
Comparing the Precision of Abstract Operators in the eBPF Verifier using Differential Synthesis
Nuntipat Narkthong
Narkthong, Nuntipat
Northeastern University
United States
Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Jorge A. Navas
Navas, Jorge A.
Certora
United States
A Flow-Sensitive Refinement Type System for Verifying eBPF Programs
Committee Member in Program Committee within the SAS -track
Amirmohammad Nazari
Nazari, Amirmohammad
University of Southern California
United States
Committee Member in SAS Artifact Evaluation Committee within the SAS Artifact-track
Ian Neal
Neal, Ian
University of Michigan and Veridise
Scalable and Accurate Application-level Crash-Consistency Testing via Representative Testing
Luca Negrini
Negrini, Luca
Ca’ Foscari University of Venice
Italy
Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Vladyslav Nekriach
Nekriach, Vladyslav
University Of Toronto
Canada
HEMVM: a Heterogeneous Blockchain Framework for Interoperable Virtual Machines
Tim Nelson
Nelson, Tim
Brown University
United States
Committee Member in Program Commitee within the SPLASH -E-track
Max S. New
New, Max S.
University of Michigan
United States
Notions of Stack-manipulating Computation and Relative Monads
Hoan Nguyen
Nguyen, Hoan
Amazon Web Services
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Yunbo Ni
Ni, Yunbo
The Chinese University of Hong Kong
Hong Kong SAR China
An Empirical Study of Bugs in the rustc Compiler
Interleaving Large Language Models for Compiler Testing
LegoFuzz: Interleaving Large Language Models for Compiler Testing
Mihai Nicola
Nicola, Mihai
Stevens Institute of Technology
Abstract Interpretation of Temporal Safety Effects of Higher Order Programs
Oscar Nierstrasz
Nierstrasz, Oscar
feenk.com
Switzerland
PC Member in Program Committee within the SPLASH Onward! Essays-track
Yue Niu
Niu, Yue
National Institute of Informatics
Integrating Resource Analyses via Resource Decomposition
James Noble
Noble, James
Independent. Wellington, NZ
New Zealand
Session Chair of Onward! Essays 2 (part of SPLASH Onward! Essays)
Reasoning about External Calls
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Session Chair of Onward! Essays 2 (part of SPLASH Onward! Papers)
Exploring The Design Space For Runtime Enforcement of Dynamic Capabilities
Michael Norrish
Norrish, Michael
Australian National University
Australia
Reproducibility Debt in Scientific Software
Aman Nougrahiya
Nougrahiya, Aman
IIT Madras
India
IncIDFA: An Efficient and Generic Algorithm for Incremental Iterative Dataflow Analysis
Clemens Nylandsted Klokmose
Nylandsted Klokmose, Clemens
Aarhus University
Denmark
Steering Committee Member in Steering Committee for SPLASH 2025
Onward! Papers Co-chair in Organizing Committee for SPLASH 2025
Steering Committee Member in Onward! Steering Committee within the SPLASH Onward! Essays-track
Co-chair in Program Committee within the SPLASH Onward! Papers-track
Steering Committee Member in Steering Committee within the SPLASH Onward! Papers-track
Liam O'Connor
O'Connor, Liam
Australian National University
Australia
ICFP Contest Report
Committee Member in ICFP Programme Committee within the ICFP Papers-track
Lina Ochoa
Ochoa, Lina
Eindhoven University of Technology
Personalization of Programming Education: An NLP-based Bi-dimensional Classification of Programming Exercises
Martin Odersky
Odersky, Martin
EPFL
Switzerland
What's in the Box: Ergonomic and Expressive Capture Tracking over Generic Data Structures
Hakjoo Oh
Oh, Hakjoo
Korea University
South Korea
Session Chair of Semantics (part of SPLASH OOPSLA)
Enhancing APR with PRISM: A Semantic-Based Approach to Overfitting Patch Detection
PAFL: Enhancing Fault Localizers by Leveraging Project-Specific Fault Patterns
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Lemma Discovery for Inductive Equational Proofs via Recursive Function Synthesis
Committee Member in ICFP Programme Committee within the ICFP Papers-track
Session Chair of Compiler (part of SAS )
Co-chair in Program Committee within the SAS -track
Wonseok Oh
Oh, Wonseok
Korea University
South Korea
Committee Member in SAS Artifact Evaluation Committee within the SAS Artifact-track
Bruno C. d. S. Oliveira
Oliveira, Bruno C. d. S.
University of Hong Kong
China
Session Chair of Languages (part of SPLASH OOPSLA)
Flexible and Expressive Typed Path Patterns for GQL
(TOPLAS) Type-Safe Compilation of Dynamic Inheritance via Merging
Liberating Merges via Apartness and Guarded Subtyping
Normalization by Evaluation for Non-cumulativity
Luca Olivieri
Olivieri, Luca
Ca’ Foscari University of Venice
Italy
Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Cyrus Omar
Omar, Cyrus
University of Michigan
United States
Incremental Bidirectional Typing via Order Maintenance
Syntactic Completions with Material Obligations
Steve Oney
Oney, Steve
University of Michigan
Committee Member in Program Committee within the SPLASH Onward! Papers-track
Emily Ong
Ong, Emily
National University of Singapore
Singapore
Siloso: Finding Logic Bugs in RDBMS via Dialect-Adaptable Reference Engine Construction
Dominic Orchard
Orchard, Dominic
University of Cambridge; University of Kent
United Kingdom
Session Chair of Types and Specifications (part of ICFP Papers)
Klaus Ostermann
Ostermann, Klaus
University of Tübingen
Germany
Compiling Classical Sequent Calculus to Stock Hardware: The Duality of Compilation
Committee Member in ICFP Programme Committee within the ICFP Papers-track
Rodrigo Otoni
Otoni, Rodrigo
USI Lugano
Switzerland
A Language for Quantifying Quantum Network Behavior
Rohan Padhye
Padhye, Rohan
Carnegie Mellon University
United States
Fray: An Efficient General-Purpose Concurrency Testing Platform for the JVM
Oded Padon
Padon, Oded
Weizmann Institute of Science
Israel
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Sreepathi Pai
Pai, Sreepathi
University of Rochester
United States
Formalizing Linear Motion G-code for Invariant Checking and Differential Testing of Fabrication Tools
Sasha Pak
Pak, Sasha
Australian National University
Australia
Verifying Extract Method Refactoring in Rust
View Types in Rust
Jens Palsberg
Palsberg, Jens
University of California, Los Angeles (UCLA)
United States
Session Chair of Quantum (part of SPLASH OOPSLA)
Soundness of Predictive Concurrency Analyses
Minxue Pan
Pan, Minxue
Nanjing University
China
Towards a Theoretically-Backed and Practical Framework for Selective Object-Sensitive Pointer Analysis
Pavel Panchekha
Panchekha, Pavel
University of Utah
United States
Incremental Bidirectional Typing via Order Maintenance
Naomi Panda
Panda, Naomi
Waddle: A Serious Game to Teach Writing, Reading, and Debugging Programs
Awanish Pandey
Pandey, Awanish
IIT Roorkee
India
Committee Member in Review Committee within the SPLASH Student Research Competition-track
Akash Pardeshi
Pardeshi, Akash
University of Illinois at Urbana-Champaign
United States
End-to-End Compiler Infrastructure for Emerging Tensor Accelerators
Pavel Parizek
Parizek, Pavel
Charles University
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Jihee Park
Park, Jihee
KAIST
South Korea
Bridging the Gap between Real-World and Formal Binary Lifting through Filtered-Simulation
Jihyeok Park
Park, Jihyeok
Korea University
South Korea
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Committee Member in Program Committee within the SAS -track
Kanghee Park
Park, Kanghee
University of Wisconsin-Madison
United States
LOUD: Synthesizing Strongest and Weakest Specifications
Seung Hoon Park
Park, Seung Hoon
Imperial College London
Compositional Symbolic Execution for the Next 700 Memory Models
Tae Hong Park
Park, Tae Hong
Purdue University
United States
Computers & Music AND Computer Music— An Unlikely [Ongoing] Journey
Program Chair in Organizing Committee within the SPLASH FARM-track
Bryan Parno
Parno, Bryan
Carnegie Mellon University
United States
Scaling Instruction-Selection Verification against Authoritative ISA Semantics
Lionel Parreaux
Parreaux, Lionel
HKUST (The Hong Kong University of Science and Technology)
Hong Kong SAR China
Session Chair of Theory (part of SPLASH OOPSLA)
Session Chair of Type 1 (part of SPLASH OOPSLA)
A Lightweight Type-and-Effect System for Invalidation Safety: Tracking Permanent and Temporary Invalidation With Constraint-Based Subtype Inference
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Committee Member in Competition Judges within the SPLASH Student Research Competition-track
Pouya Partow
Partow, Pouya
Birmingham University
Big Steps in Higher-Order Mathematical Operational Semantics
Radha Patel
Patel, Radha
MIT CSAIL
Finch: Sparse and Structured Tensor Programming with Control Flow
Daniel Patterson
Patterson, Daniel
Northeastern University
United States
SPLASH-E Co-Chair in Organizing Committee for SPLASH 2025
SPLASH-E Co-Chair in Program Commitee within the SPLASH -E-track
Teaching Software Specification (Experience Report)
William Payne
Payne, William
UNC School of Information and Library Science
Weft—Enabling Tidal on the Web
Luke Pearson
Pearson, Luke
Polychain Capital
Tabby: A Synthesis-Aided Compiler for High-Performance Zero-Knowledge Proof Circuits
Anurudh Peduri
Peduri, Anurudh
Ruhr University Bochum
QbC: Quantum Correctness by Construction
Yu Pei
Pei, Yu
Hong Kong Polytechnic University
China
PReMM: LLM-Based Program Repair for Multi-Method Bugs via Divide and Conquer
Hila Peleg
Peleg, Hila
Technion
Israel
ScooPy: Enhancing Program Synthesis with Nested Example Specifications
Daniel A. A. Pelsmaeker
Pelsmaeker, Daniel A. A.
Delft University of Technology, Netherlands
Netherlands
Language-Parametric Reference Synthesis
Mai Jacob Peng
Peng, Mai Jacob
McGill University
Canada
Sound and Modular Activity Analysis for Automatic Differentiation in MLIR
Wei Peng
Peng, Wei
Fudan University
JavART: a Lightweight Rule-Based JIT Compiler Using Translation Rules Extracted from a Learning Approach
Xuanyu Peng
Peng, Xuanyu
University of California, San Diego
United States
LOUD: Synthesizing Strongest and Weakest Specifications
Yiteng Peng
Peng, Yiteng
Hong Kong University of Science and Technology
China
Extraction and Mutation at a High Level: Template-Based Fuzzing for JavaScript Engines
João Pereira
Pereira, João
ETH Zurich
Modular Reasoning about Global Variables and Their Initialization
A Refinement Methodology for Distributed Programs in Rust
Mário Pereira
Pereira, Mário
NOVA LINCS & DI -- Nova School of Science and Technology
Portugal
Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Daniel Perelman
Perelman, Daniel
Microsoft
United States
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Roly Perera
Perera, Roly
University of Cambridge/University of Bristol
United Kingdom
Committee Member in Program Committee within the SPLASH Onward! Papers-track
Basile Pesin
Pesin, Basile
Ecole Nationale de l'Aviation Civile (ENAC)
Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Edward Peters
Peters, Edward
Pushing the Information-Theoretic Limits of Random Access Lists
Anja Petković Komel
Petković Komel, Anja
Argot Collective
Divide and Conquer: A Compositional Approach to Game-Theoretic Security
Tomas Petricek
Petricek, Tomas
Charles University
Czechia
Steering Committee Member in Onward! Steering Committee within the SPLASH Onward! Essays-track
Steering Committee Member in Steering Committee within the SPLASH Onward! Papers-track
Daniela Petrisan
Petrisan, Daniela
IRIF, Université Paris Diderot
France
Committee Member in ICFP Programme Committee within the ICFP Papers-track
Loïc Peyrot
Peyrot, Loïc
IMDEA Software Institute
Polymorphic Records for Dynamic Languages
Simon Peyton Jones
Peyton Jones, Simon
Epic Games
United Kingdom
Committee Member in ICFP Programme Committee within the ICFP Papers-track
Frank Pfenning
Pfenning, Frank
Carnegie Mellon University, USA
Structural Information Flow: A Fresh Look at Types for Non-Interference
Long Pham
Pham, Long
Carnegie Mellon University
United States
Integrating Resource Analyses via Resource Decomposition
Nguyen Pham
Pham, Nguyen
EPFL, LAMP
Switzerland
What's in the Box: Ergonomic and Expressive Capture Tracking over Generic Data Structures
Phitchaya Mangpo Phothilimthana
Phothilimthana, Phitchaya Mangpo
OpenAI
Mind the Abstraction Gap: Bringing Equality Saturation to Real-World ML Compilers
David Pichardie
Pichardie, David
Meta
France
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Contextual Equality Saturation
Committee Member in Steering Committee within the SAS -track
Jean Pichon-Pharabod
Pichon-Pharabod, Jean
Aarhus University
Denmark
Synchronous Programming for Kids: A Manifesto
Lauren Pick
Pick, Lauren
The Chinese University of Hong Kong
Checking Observational Correctness of Database Systems
Brigitte Pientka
Pientka, Brigitte
McGill University
Canada
McTT: A Verified Kernel for a Proof Assistant
Fusing Session-Typed Concurrent Programming into Functional Programming
Benjamin C. Pierce
Pierce, Benjamin C.
University of Pennsylvania
United States
Tuning Random Generators: Property-Based Testing as Probabilistic Programming
QED in Context: An Observation Study of Proof Assistant Users
Bennet: Randomized Specification Testing for Heap-Manipulating Programs
Frank Piessens
Piessens, Frank
KU Leuven
Belgium
Software Stacks for Confidential Computing Hardware
Ruzica Piskac
Piskac, Ruzica
Yale University
United States
Counterexample-Guided Inference of Modular Specifications
Coinductive Proofs of Regular Expression Equivalence in Zero Knowledge
Goran Piskachev
Piskachev, Goran
Amazon Web Services
Germany
Committee Member in Program Committee within the SAS -track
Clément Pit-Claudel
Pit-Claudel, Clément
EPFL
Switzerland
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
André Platzer
Platzer, André
Karlsruhe Institute of Technology (KIT)
Germany
Adaptive Shielding via Parametric Safety Proofs
Dan Plyukhin
Plyukhin, Dan
University of Southern Denmark
Denmark
Relax! The Semilenient Core of Choreographic Programming (Functional Pearl)
Gabriel Poesia
Poesia, Gabriel
Stanford University
Automated Discovery of Tactic Libraries for Interactive Theorem Proving
Nadia Polikarpova
Polikarpova, Nadia
University of California at San Diego
United States
Peepco: Batch-Based Consistency Optimization
Laurel: Unblocking Automated Verification with Large Language Models
Guillermo Polito
Polito, Guillermo
Univ. Lille, Inria, CNRS, Centrale Lille, UMR 9189 CRIStAL
France
Committee Member in Program Committee within the SPLASH Onward! Papers-track
Thomas J. Porter
Porter, Thomas J.
University of Michigan
United States
Incremental Bidirectional Typing via Order Maintenance
Syntactic Completions with Material Obligations
Alex Potanin
Potanin, Alex
Australian National University
Australia
Steering Committee Chair in Steering Committee for SPLASH 2025
[Closed Session] Adjudication meeting for SIGPLAN's John Vlissides award
SIGPLAN Awards
SPLASH Awards
Embedding Quantum Program Verification into Dafny
SPLASH Organisers Discussion and AMA
Verifying Extract Method Refactoring in Rust
Reproducibility Debt in Scientific Software
View Types in Rust
X-by-Construction: Towards Ensuring Non-Functional Properties in by-Construction Engineering
François Pottier
Pottier, François
Inria
France
Formal Semantics and Program Logics for a Fragment of OCaml
Jyoti Prakash
Prakash, Jyoti
University of Passau
Germany
Committee Member in SAS Artifact Evaluation Committee within the SAS Artifact-track
Pontakorn Prasertsuk
Prasertsuk, Pontakorn
Singapore
Evolving How We Teach Memory Models
Thomas S. Price
Price, Thomas S.
Carnegie Mellon University
United States
Polynomial-Time Program Equivalence for Machine Knitting
Aleksandar Prokopec
Prokopec, Aleksandar
Oracle Labs
Switzerland
Heap-Snapshot Matching and Ordering using CAHPs: A Context-Augmented Heap-Path Representation for Exact and Partial Path Matching using Prefix Trees
Loïc Pujet
Pujet, Loïc
Stockholm University
Type Theory in Type Theory using a Strictified Syntax
Yong Qi Foo
Qi Foo, Yong
National University of Singapore
Singapore
Pushing the Information-Theoretic Limits of Random Access Lists
Xueying Qin
Qin, Xueying
University of Southern Denmark
Denmark
Relax! The Semilenient Core of Choreographic Programming (Functional Pearl)
Xiaokang Qiu
Qiu, Xiaokang
Purdue University
United States
Committee Member in Program Committee within the SAS -track
Weihao Qu
Qu, Weihao
University at Buffalo, SUNY
Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Andrew Quinn
Quinn, Andrew
University of California at Santa Cruz
United States
Scalable and Accurate Application-level Crash-Consistency Testing via Representative Testing
Benjamin Quiring
Quiring, Benjamin
University of Maryland at College Park
United States
Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Environment-Sharing Analysis and Caller-Provided Environments for Higher-Order Languages
Azalea Raad
Raad, Azalea
Imperial College London
United Kingdom
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Dimi Racordon
Racordon, Dimi
EPFL, LAMP
Switzerland
PC Member in Program Committee within the SPLASH Onward! Essays-track
Dimi Racordon
Racordon, Dimi
EPFL
Switzerland
Existentialize your Generics
Arjun Radhakrishna
Radhakrishna, Arjun
Microsoft
United States
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Jonathan Ragan-Kelley
Ragan-Kelley, Jonathan
Massachusetts Institute of Technology
United States
Gauguin, Descartes, Bayes: A Diurnal Golem's Brain
A Domain-Specific Probabilistic Programming Language for Reasoning about Reasoning (or: a memo on memo)
Shanto Rahman
Rahman, Shanto
The University of Texas at Austin
United States
UTFix: Change Aware Unit Test Repairing using LLM
Understanding and Improving Flaky Test Classification
Sophie Rain
Rain, Sophie
Argot Collective
Divide and Conquer: A Compositional Approach to Game-Theoretic Security
Ramya Ramalingam
Ramalingam, Ramya
University of Pennsylvania
Active Learning for Neurosymbolic Program Synthesis
Arjun Ramesh
Ramesh, Arjun
Carnegie Mellon University
Unveiling Heisenbugs with Diversified Execution
Robert Rand
Rand, Robert
University of Chicago
United States
Compositional Quantum Control Flow with Efficient Compilation in Qunity
A Language for Quantifying Quantum Network Behavior
Francesca Randone
Randone, Francesca
Department of Mathematics, Informatics and Geosciences, University of Trieste, Italy
Foundations for Deductive Verification of Continuous Probabilistic Programs: From Lebesgue to Riemann and Back
Marianna Rapoport
Rapoport, Marianna
Amazon Web Services
Canada
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Joseph Raskind
Raskind, Joseph
SUNY Binghamton
Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Aseem Rastogi
Rastogi, Aseem
Microsoft Research
India
Automatically Verifying Replication-aware Linearizability
Savitha Ravi
Ravi, Savitha
UC San Diego
An Empirical Evaluation of Property-Based Testing in Python
Michael Rawson
Rawson, Michael
University of Southampton
United Kingdom
Divide and Conquer: A Compositional Approach to Game-Theoretic Security
Baishakhi Ray
Ray, Baishakhi
Columbia University
United States
UTFix: Change Aware Unit Test Repairing using LLM
Patrick Redmond
Redmond, Patrick
University of California, Santa Cruz
Exploring the Theory and Practice of Concurrency in the Entity-Component-System Pattern
John Regehr
Regehr, John
University of Utah
United States
PC Member in Program Committee within the SPLASH Onward! Essays-track
Translation Validation for LLVM's AArch64 Backend
Baber Rehman
Rehman, Baber
University of Hong Kong
Hong Kong SAR China
Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Hamza Remmal
Remmal, Hamza
EPFL, LAMP
Switzerland
Existentialize your Generics
Alexander Repenning
Repenning, Alexander
University of Colorado, Boulder
United States
Committee Member in Program Committee within the SPLASH Onward! Papers-track
John Reppy
Reppy, John
University of Chicago
United States
Session Chair of Clever Compilation (part of ICFP Papers)
Environment-Sharing Analysis and Caller-Provided Environments for Higher-Order Languages
Committee Member in ICFP Programme Committee within the ICFP Papers-track
Thomas Reps
Reps, Thomas
University of Wisconsin-Madison
United States
Software Model Checking via Summary-Guided Search
(TOPLAS) Polynomial Bounds of CFLOBDDs against BDDs
Semantics of Sets of Programs
Scalable Equivalence Checking and Verification of Shallow Quantum Circuits
Mohammad Rezaalipour
Rezaalipour, Mohammad
University of Passau
Germany
Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Jaspreet Riar
Riar, Jaspreet
Carnegie Mellon University
Unveiling Heisenbugs with Diversified Execution
Jay Richards
Richards, Jay
University of Kent
Symbolic MRD: Dynamic Memory, Undefined Behaviour, and Extrinsic Choice
Bryan Richlinski
Richlinski, Bryan
Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Manuel Rigger
Rigger, Manuel
National University of Singapore
Singapore
Flexible and Expressive Typed Path Patterns for GQL
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Talia Lily Ringer
Ringer, Talia Lily
University of Illinois Urbana-Champaign
United States
Proof Repair across Quotient Type Equivalences
Xavier Rival
Rival, Xavier
Inria - CNRS - Ecole Normale Superieure de Paris - PSL University
France
Session Chair of Abstraction and Proofs (part of SAS )
Towards static analyses and abstract domains for hyperproperties
Committee Member in Program Committee within the SAS -track
Exequiel Rivas
Rivas, Exequiel
Tallinn University of Technology; Ahrefs
SecRef*: Securely Sharing Mutable References between Verified and Unverified Code in F*
Cody Rivera
Rivera, Cody
University of Illinois, Urbana-Champaign
Checking $\delta$-Satisfiability of Reals with Integrals
Alice Rixte
Rixte, Alice
Generalizing Turtle Geometry: An Extensible Language for Vector Graphics Drawing
Neil Rolnick
Rolnick, Neil
Concert: Mirages
Tiark Rompf
Rompf, Tiark
Purdue University
United States
Modeling Reachability Types with Logical Relations -- Semantic Type Soundness, Termination, Effect Safety, and Equational Theory
Complete the Cycle: Reachability Types with Expressive Cyclic References
Committee Member in ICFP Programme Committee within the ICFP Papers-track
Julian Rosemann
Rosemann, Julian
Saarland University, Saarland Informatics Campus
Germany
Non-interference Preserving Optimising Compilation
Andrea Rosà
Rosà, Andrea
USI Lugano
Switzerland
Heap-Snapshot Matching and Ordering using CAHPs: A Context-Augmented Heap-Path Representation for Exact and Partial Path Matching using Prefix Trees
Committee Member in Program Committee within the SPLASH Onward! Papers-track
Jurriaan Rot
Rot, Jurriaan
Radboud University Nijmegen
A Unifying Approach to Product Constructions for Quantitative Temporal Inference
Anthony Rowe
Rowe, Anthony
Carnegie Mellon University
Unveiling Heisenbugs with Diversified Execution
Radosław Jan Rowicki
Rowicki, Radosław Jan
Technical University of Denmark
Denmark
Correct Black-Box Monitors for Distributed Deadlock Detection: Formalisation and Implementation
Craig Roy
Roy, Craig
Quantinuum
Fulls Seldom Differ
Subhajit Roy
Roy, Subhajit
IIT Kanpur
India
Student Research Competition Chair in Organizing Committee for SPLASH 2025
Memory-Safety Verification of Open Programs With Angelic Assumptions
SPLASH SRC Awards
Co-chair in Review Committee within the SPLASH Student Research Competition-track
Philipp Ruemmer
Ruemmer, Philipp
University of Regensburg and Uppsala University
Germany
The Power of Regular Constraint Propagation
Neea Rusch
Rusch, Neea
Augusta University
United States
Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Yeonhee Ryou
Ryou, Yeonhee
KAIST
South Korea
Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Sukyoung Ryu
Ryu, Sukyoung
KAIST
South Korea
Steering Committee Member in Steering Committee for SPLASH 2025
OOPSLA Review Committee Co-Chair in Organizing Committee for SPLASH 2025
Session Chair of Thursday SPLASH Keynote (part of SPLASH Keynotes)
Session Chair of Verification 2 (part of SPLASH OOPSLA)
Bridging the Gap between Real-World and Formal Binary Lifting through Filtered-Simulation
RC Chair Report
OOPSLA Awards
Co-chair in OOPSLA Review Committee within the SPLASH OOPSLA-track
William S. Moses
S. Moses, William
University of Illinois Urbana-Champaign
United States
Sound and Modular Activity Analysis for Automatic Differentiation in MLIR
Mind the Abstraction Gap: Bringing Equality Saturation to Real-World ML Compilers
Feras A. Saad
Saad, Feras A.
Carnegie Mellon University
United States
Integrating Resource Analyses via Resource Decomposition
Amr Sabry
Sabry, Amr
Indiana University
United States
A Haskell Adiabatic DSL: Solving Classical Optimization Problems on Quantum Hardware
Hannes Saffrich
Saffrich, Hannes
University of Freiburg
Borrowing From Session Types
Sunita Saha
Saha, Sunita
German Research Center for Artificial Intelligence (DFKI), Saarbrücken, Germany
im2im: Automatically Converting In-Memory Image Representations using A Knowledge Graph Approach
Ayman Said
Said, Ayman
University of Michigan
Scalable and Accurate Application-level Crash-Consistency Testing via Representative Testing
Kazuhiko Sakaguchi
Sakaguchi, Kazuhiko
CNRS - ENS Lyon - Université Claude Bernard Lyon 1 - LIP - UMR 5668
France
A Bargain for Mergesorts: How to Prove Your Mergesort Correct and Stable, Almost for Free
Ken Sakayori
Sakayori, Ken
University of Tokyo
Japan
Automated Catamorphism Synthesis for Solving Constrained Horn Clauses over Algebraic Data Types
Marie Salomon
Salomon, Marie
University of British Columbia
Canada
An Exploration of How Generative AI Affects Workflow and Collaboration in a Software Engineering Course
Michael Sammler
Sammler, Michael
Institute of Science and Technology Austria
Austria
Committee Member in ICFP Programme Committee within the ICFP Papers-track
Adrian Sampson
Sampson, Adrian
Cornell University
PC Member in Program Committee within the SPLASH Onward! Essays-track
Ashley Samuelson
Samuelson, Ashley
University of Wisconsin-Madison
United States
Choreographic Quick Changes: First-Class Location (Set) Polymorphism
David Sanan
Sanan, David
Singapore Institute of Technology
Singapore
A complete formal semantics of eBPF instruction set architecture for Solana
Chuta Sano
Sano, Chuta
McGill University
Canada
Fusing Session-Typed Concurrent Programming into Functional Programming
André L. Santos
Santos, André L.
University Institute of Lisbon, Portugal
Committee Member in Program Commitee within the SPLASH -E-track
Yasmin Chandini Sarita
Sarita, Yasmin Chandini
UIUC
Automated Verification of Soundness of DNN Certifiers
Kartik Sathyanarayanan
Sathyanarayanan, Kartik
Netflix, Inc.
Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Ryosuke Sato
Sato, Ryosuke
Tokyo University of Agriculture and Technology
Japan
Automated Catamorphism Synthesis for Solving Constrained Horn Clauses over Algebraic Data Types
Alceste Scalas
Scalas, Alceste
Technical University of Denmark
Denmark
Correct Black-Box Monitors for Distributed Deadlock Detection: Formalisation and Implementation
Ina Schaefer
Schaefer, Ina
KIT
Germany
QbC: Quantum Correctness by Construction
X-by-Construction: Towards Ensuring Non-Functional Properties in by-Construction Engineering
Daniel Schemmel
Schemmel, Daniel
Imperial College London
P³: Reasoning about Patches via Product Programs
Gabriel Scherer
Scherer, Gabriel
Université Paris Cité - Inria - CNRS
France
Committee Member in ICFP Programme Committee within the ICFP Papers-track
Marko Schmellenkamp
Schmellenkamp, Marko
Ruhr University Bochum
Germany
Detecting and explaining (in-)equivalence of context-free grammars
Bradley Schmerl
Schmerl, Bradley
School of Computer Science, Carnegie Mellon University
ROSpec: A Domain-Specific Language for ROS-based Robot Software
Valentin Schneeberger
Schneeberger, Valentin
EPFL
Logically Qualified Types for Scala
Matthew Schneider
Schneider, Matthew
Carnegie Mellon University
United States
Debugging WebAssembly? Put some Whamm on it!
Christophe Scholliers
Scholliers, Christophe
Universiteit Gent, Belgium
MIO: Multiverse Debugging in the face of Input/Output
Tom Schrijvers
Schrijvers, Tom
KU Leuven
Belgium
Effectful Lenses: There and Back with Different Monads
Lutz Schröder
Schröder, Lutz
Friedrich-Alexander University Erlangen-Nürnberg
Germany
Bialgebraic Reasoning on Stateful Languages
Michael Schröder
Schröder, Michael
TU Wien
Austria
Static Inference of Regular Grammars for Ad Hoc Parsers
Manuela Schuler
Schuler, Manuela
German Research Center for Artificial Intelligence (DFKI), Saarbrücken, Germany; Saarland University, Saarbrücken, Germany
im2im: Automatically Converting In-Memory Image Representations using A Knowledge Graph Approach
Adriana Schulz
Schulz, Adriana
University of Washington
United States
Polynomial-Time Program Equivalence for Machine Knitting
Philipp Schuster
Schuster, Philipp
University of Tübingen
Germany
Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Dynamic Wind for Effect Handlers
Compiling Classical Sequent Calculus to Stock Hardware: The Duality of Compilation
The Simple Essence of Monomorphization
Multiple Resumptions and Local Mutable State, Directly
David J. Scott
Scott, David J.
Docker, Inc.
Functional Networking for Millions of Docker Desktops (Experience Report)
Remy Seassau
Seassau, Remy
Inria
France
Formal Semantics and Program Logics for a Fragment of OCaml
Taro Sekiyama
Sekiyama, Taro
National Institute of Informatics
Japan
On Higher-Order Model Checking of Effectful Answer-Type-Polymorphic Programs
Mazyar Seraj
Seraj, Mazyar
Eindhoven University of Technology
Netherlands
Personalization of Programming Education: An NLP-based Bi-dimensional Classification of Programming Exercises
Committee Member in Program Commitee within the SPLASH -E-track
Ilya Sergey
Sergey, Ilya
National University of Singapore
Singapore
ICFP General Chair and Local Chair in Organizing Committee for SPLASH 2025
Inductive Synthesis of Inductive Heap Predicates
General Chair Report
Opening
Award Ceremony
Session Chair of Monday ICFP Keynote (part of ICFP Keynotes)
Multi-Modal Verification of Distributed Systems in Lean
Manuel Serrano
Serrano, Manuel
Inria; Université Côte d’Azur
France
Session Chair of Memory (part of SPLASH OOPSLA)
Float Self-Tagging
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Associate Chair in ICFP Programme Committee within the ICFP Papers-track
Sanjit A. Seshia
Seshia, Sanjit A.
University of California, Berkeley
United States
Checking Observational Correctness of Database Systems
Matan Shachnai
Shachnai, Matan
Comparing the Precision of Abstract Operators in the eBPF Verifier using Differential Synthesis
Amir Shaikhha
Shaikhha, Amir
University of Edinburgh
United Kingdom
Compressed and Parallelized Structured Tensor Algebra
Arindam Sharma
Sharma, Arindam
Imperial College London
P³: Reasoning about Patches via Product Programs
Dongdong She
She, Dongdong
HKUST (The Hong Kong University of Science and Technology)
Hong Kong SAR China
Publications Chair in Organizing Committee for SPLASH 2025
Jiasi Shen
Shen, Jiasi
The Hong Kong University of Science and Technology
Session Chair of Neural Network (part of SPLASH OOPSLA)
Session Chair of Code (part of SPLASH OOPSLA)
A Sound Static Analysis Approach to I/O API Migration
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Qingchao Shen
Shen, Qingchao
Tianjin University
China
DESIL: Detecting Silent Bugs in MLIR Compiler Infrastructure
Ashley Sheng
Sheng, Ashley
Wellesley College
United States
Scaling Instruction-Selection Verification against Authoritative ISA Semantics
Stephen Sherratt
Sherratt, Stephen
Tarides
Software-defined declarative synthesizer live-coding in a jupyter notebook
August Shi
Shi, August
The University of Texas at Austin
United States
Understanding and Improving Flaky Test Classification
Chenghang Shi
Shi, Chenghang
SKLP, Institute of Computing Technology, CAS
China
Fast Client-Driven CFL-Reachability via Regularization-Based Graph Simplification
Chuanqi Shi
Shi, Chuanqi
School of Computer Science and Engineering, College of Software Engineering, School of Artifical Intelligence, Southeast University
ABC: Towards a Universal Code Styler through Model Merging
Jessica Shi
Shi, Jessica
University of Pennsylvania
QED in Context: An Observation Study of Proof Assistant Users
Qingkai Shi
Shi, Qingkai
Nanjing University
China
An Empirical Study of Bugs in the rustc Compiler
Yuanfeng Shi
Shi, Yuanfeng
Peking University
China
On Abstraction Refinement for Bayesian Program Analysis
Olin Shivers
Shivers, Olin
Northeastern University
United States
Environment-Sharing Analysis and Caller-Provided Environments for Higher-Order Languages
Xujie Si
Si, Xujie
University of Toronto
Committee Member in Program Committee within the SAS -track
Jeremy G. Siek
Siek, Jeremy G.
Indiana University
United States
Session Chair of Gradual Typing and Security (part of ICFP Papers)
Committee Member in ICFP Programme Committee within the ICFP Papers-track
Cedric Siems
Siems, Cedric
Ruhr University Bochum
Detecting and explaining (in-)equivalence of context-free grammars
Ho Siew Foong
Siew Foong, Ho
National University of Singapore
Singapore
Local Arrangements Chair in Organizing Committee for SPLASH 2025
Mihaela Sighireanu
Sighireanu, Mihaela
University Paris-Saclay, ENS Paris-Saclay, CNRS, LMF
France
Steering Committee Member in Steering Committee for SPLASH 2025
Committee Member in Steering Committee within the SAS -track
Florian Sihler
Sihler, Florian
Ulm University
Germany
Statically Analyzing the Dataflow of R Programs
Waddle: A Serious Game to Teach Writing, Reading, and Debugging Programs
Alexandra Silva
Silva, Alexandra
Cornell University
United States
Associate Chair in OOPSLA Review Committee within the SPLASH OOPSLA-track
Robert Simmons
Simmons, Robert
Independent
United States
Committee Member in Program Commitee within the SPLASH -E-track
Jeremy Singer
Singer, Jeremy
University of Glasgow
United Kingdom
Let's Take Esoteric Programming Languages Seriously
Abhishek Kr Singh
Singh, Abhishek Kr
IIIT Hyderabad
India
Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Avaljot Singh
Singh, Avaljot
UIUC
United States
Automated Verification of Soundness of DNN Certifiers
Gagandeep Singh
Singh, Gagandeep
University of Illinois at Urbana-Champaign; VMware Research
United States
Automated Verification of Soundness of DNN Certifiers
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Committee Member in Program Committee within the SAS -track
Committee Member in Steering Committee within the SAS -track
Satnam Singh
Singh, Satnam
Independent
United States
Functional Programming for Hardware Design
Somesh Singh
Singh, Somesh
Siemens EDA
France
Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
A. Prasad Sistla
Sistla, A. Prasad
University of Illinois at Chicago
Checking $\delta$-Satisfiability of Reals with Integrals
KC Sivaramakrishnan
Sivaramakrishnan, KC
IIT Madras and Tarides
India
Session Chair of Verification 3 (part of SPLASH OOPSLA)
Automatically Verifying Replication-aware Linearizability
Associate Chair in OOPSLA Review Committee within the SPLASH OOPSLA-track
A guided tour through Oxidized OCaml
Session Chair of Implementation (part of ICFP Papers)
Committee Member in ICFP Programme Committee within the ICFP Papers-track
Aishwarya Sivaraman
Sivaraman, Aishwarya
Meta
Synthesizing Implication Lemmas for Interactive Theorem Proving
Kugesan Sivasothynathan
Sivasothynathan, Kugesan
Jaseci Labs
MTP: A Meaning-Typed Language Abstraction for AI-Integrated Programming
Dang Sixuan
Sixuan, Dang
Duke University
Agora: Trust Less and Open More in Verification for Confidential Computing
Opale Sjöstedt
Sjöstedt, Opale
Imperial College London
Compositional Symbolic Execution for the Next 700 Memory Models
Philipp Slusallek
Slusallek, Philipp
DFKI, Germany
Germany
im2im: Automatically Converting In-Memory Image Representations using A Knowledge Graph Approach
Yannis Smaragdakis
Smaragdakis, Yannis
University of Athens
Greece
Universal Scalability in Declarative Program Analysis (with Choice-Based Combination Pruning)
Calvin Smith
Smith, Calvin
University of Texas Austin
United States
Committee Member in Review Committee within the SPLASH Student Research Competition-track
Sunbeom So
So, Sunbeom
GIST (Gwangju Institute of Science and Technology)
Committee Member in Program Committee within the SAS -track
Armando Solar-Lezama
Solar-Lezama, Armando
Massachusetts Institute of Technology
United States
Peepco: Batch-Based Consistency Optimization
Dowon Song
Song, Dowon
Korea University
South Korea
Enhancing APR with PRISM: A Semantic-Based Approach to Overfitting Patch Detection
Fu Song
Song, Fu
Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences; Nanjing Institute of Software Technology
China
Verification of Bit-Flip Attacks against Quantized Neural Networks
Committee Member in Program Committee within the SAS -track
Jiaxin Song
Song, Jiaxin
University of Illinois at Urbana-Champaign
United States
Tabby: A Synthesis-Aided Compiler for High-Performance Zero-Knowledge Proof Circuits
Wei Song
Song, Wei
Nanjing University of Science and Technology
China
DepFuzz: Efficient Smart Contract Fuzzing with Function Dependence Guidance
Finding Compiler Bugs through Cross-Language Code Generator and Differential Testing
Yahui Song
Song, Yahui
Standard Chartered Bank
Singapore
SRC Judge & Co-Organizer in Review Committee within the SPLASH Student Research Competition-track
SRC Judge & Co-Organizer in Competition Judges within the SPLASH Student Research Competition-track
Committee Member in ICFP Programme Committee within the ICFP Papers-track
Session Chair of Testing and Constraint Solving (part of SAS )
Specifying and Verifying Future Conditions
Tyler Sorensen
Sorensen, Tyler
Microsoft Research and University of California at Santa Cruz
United States
SafeRace: Assessing and Addressing WebGPU Memory Safety in the Presence of Data Races
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Skye Soss
Soss, Skye
University of Chicago
United States
Environment-Sharing Analysis and Caller-Provided Environments for Higher-Order Languages
Thodoris Sotiropoulos
Sotiropoulos, Thodoris
ETH Zurich
Switzerland
Validating Soundness and Completeness in Pattern-Match Coverage Analyzers
Matthew Sotoudeh
Sotoudeh, Matthew
Stanford University
Pathological Cases for a Class of Reachability-Based Garbage Collectors
Literate Tracing
Robert Soulé
Soulé, Robert
Yale University
A Language for Quantifying Quantum Network Behavior
Vimala Soundarapandian
Soundarapandian, Vimala
IIT Madras
India
Automatically Verifying Replication-aware Linearizability
Janek Spaderna
Spaderna, Janek
University of Freiburg, Germany
Borrowing From Session Types
Michael Sperber
Sperber, Michael
Active Group GmbH
Germany
PC Member in Program Committee within the SPLASH Onward! Essays-track
Arnaud Spiwack
Spiwack, Arnaud
Tweag
France
Destination calculus: A linear λ-calculus for purely functional memory writes
Manu Sridharan
Sridharan, Manu
University of California at Riverside
United States
Steering Committee Member in Steering Committee for SPLASH 2025
Steering Committee Member in Onward! Steering Committee within the SPLASH Onward! Essays-track
Steering Committee Member in Steering Committee within the SPLASH Onward! Papers-track
Caleb Stanford
Stanford, Caleb
University of California, Davis
United States
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Jonathan Lindegaard Starup
Starup, Jonathan Lindegaard
Denmark
Qualified Types with Boolean Algebras
Fynn Stebel
Stebel, Fynn
Ruhr University Bochum
Detecting and explaining (in-)equivalence of context-free grammars
Maarten Steevens
Steevens, Maarten
Ghent University, Belgium
Belgium
MIO: Multiverse Debugging in the face of Input/Output
Leo Stefanesco
Stefanesco, Leo
University of Cambridge
United Kingdom
Certified Decision Procedures for Width-Independent Bitvector Predicates
Interactive Bit Vector Reasoning using Verified Bitblasting
Session Chair of Separation Logic (part of ICFP Papers)
Friedrich Steimann
Steimann, Friedrich
Fernuniversität in Hagen
Germany
PC Member in Program Committee within the SPLASH Onward! Essays-track
Jonathan Sterling
Sterling, Jonathan
University of Cambridge
United Kingdom
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Michel Steuwer
Steuwer, Michel
Technische Universität Berlin
Germany
Multiple Resumptions and Local Mutable State, Directly
Sam Stites
Stites, Sam
Northeastern University
United States
Multi-Language Probabilistic Programming
Quentin Stiévenart
Stiévenart, Quentin
Université du Québec à Montréal
Canada
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Abstracting Concolic Execution for Soft Contract Verification
Filip Strömbäck
Strömbäck, Filip
Linköping University
Sweden
Continuations for All: Language Design Considerations for Accessible Continuations
Felix Stutz
Stutz, Felix
University of Luxembourg, Luxembourg
Characterizing Implementability of Global Protocols with Infinite States and Data
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Zhendong Su
Su, Zhendong
ETH Zurich
Switzerland
The Quest Toward that Perfect Compiler
Validating Soundness and Completeness in Pattern-Match Coverage Analyzers
An Empirical Study of Bugs in the rustc Compiler
API-guided Dataset Synthesis to Finetune Large Code Models
Giancarlo Succi
Succi, Giancarlo
Committee Member in Program Committee within the SPLASH Onward! Papers-track
Chamika Sudusinghe
Sudusinghe, Chamika
University of Illinois at Urbana-Champaign
GALA: A High Performance Graph Neural Network Acceleration LAnguage and Compiler
Tianxiang Sui
Sui, Tianxiang
Ant Group
MetaKernel: Enabling Efficient Encrypted Neural Network Inference Through Unified MVM and Convolution
Yulei Sui
Sui, Yulei
University of New South Wales
Australia
Student Research Competition Chair in Organizing Committee for SPLASH 2025
Efficient Abstract Interpretation via Selective Widening
SPLASH SRC Awards
Co-chair in Review Committee within the SPLASH Student Research Competition-track
Co-chair in Program Committee within the SAS -track
Alexander J. Summers
Summers, Alexander J.
University of British Columbia
Canada
Session Chair of Rust (part of SPLASH OOPSLA)
Place Capability Graphs: A General-Purpose Model of Rust’s Ownership and Borrowing Guarantees
Chengnian Sun
Sun, Chengnian
University of Waterloo
Canada
Boosting Program Reduction with the Missing Piece of Syntax-Guided Transformations
Jun Sun
Sun, Jun
Singapore Management University
Singapore
Correct-By-Construction: Certified Individual Fairness through Neural Network Training
Verification of Bit-Flip Attacks against Quantized Neural Networks
Fuzzing C++ Compilers via Type-Driven Mutation
Maolin Sun
Sun, Maolin
Nanjing University
China
Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Validating SMT Rewriters via Rewrite Space Exploration Supported by Generative Equality Saturation
Yaozhu Sun
Sun, Yaozhu
National Institute of Informatics
Japan
Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
(TOPLAS) Type-Safe Compilation of Dynamic Inheritance via Merging
Vaishnavi Sundararajan
Sundararajan, Vaishnavi
IIT Delhi
India
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Vijay Sundaresan
Sundaresan, Vijay
IBM Canada
Canada
CoSSJIT: Combining Static Analysis and Speculation in JIT Compilers
Shiv Sundram
Sundram, Shiv
Stanford University
REPTILE: Performant Tiling of Recurrences
Chenyao Suo
Suo, Chenyao
Tianjin University
China
DESIL: Detecting Silent Bugs in MLIR Compiler Infrastructure
Milijana Surbatovich
Surbatovich, Milijana
University of Maryland
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Session Chair of Women in PL Dinner (part of ICFP Diversity, Equity, and Inclusion)
Nikhil Swamy
Swamy, Nikhil
Microsoft Research
United States
Committee Member in ICFP Programme Committee within the ICFP Papers-track
Wouter Swierstra
Swierstra, Wouter
Utrecht University, Netherlands
Netherlands
First-Order Laziness
Emma Söderberg
Söderberg, Emma
Lund University
Sweden
Committee Member in Program Committee within the SPLASH Onward! Papers-track
Marco T Morazan
T Morazan, Marco
Seton Hall University
United States
Derivation Visualization for Context-Free Grammar Design: Helping Students Understand Context-Free Grammars
Nicolas Tabareau
Tabareau, Nicolas
Inria
France
Incremental Certified Programming
Robust Dynamic Embedding for Gradual Typing
Marcel Taeumel
Taeumel, Marcel
University of Potsdam; Hasso Plattner Institute
Germany
Steering Committee Member in Steering Committee for SPLASH 2025
Steering Committee Member in Onward! Steering Committee within the SPLASH Onward! Essays-track
Steering Committee Member in Steering Committee within the SPLASH Onward! Papers-track
Gourav Takhar
Takhar, Gourav
Indian Institute of Technology - Kanpur
India
Memory-Safety Verification of Open Programs With Angelic Assumptions
SRC Judge & Co-Organizer in Competition Judges within the SPLASH Student Research Competition-track
Jean-Pierre Talpin
Talpin, Jean-Pierre
INRIA, France
HpC: A Calculus for Hybrid and Mobile Systems
Gang (Gary) Tan
Tan, Gang (Gary)
Pennsylvania State University
United States
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Grace Tan
Tan, Grace
National University of Singapore
Evolving How We Teach Memory Models
Guangming Tan
Tan, Guangming
Chinese Academy of Sciences(CAS)
Stencil-Lifting: Hierarchical Recursive Lifting System for Extracting Summary of Stencil Kernel in Legacy Codes
Lin Tan
Tan, Lin
Purdue University
United States
Show Me Why It's Correct: Saving 1/3 of Debugging Time in Program Repair with Interactive Runtime Comparison
Shangyin Tan
Tan, Shangyin
University of California, Berkeley
United States
Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Tian Tan
Tan, Tian
Nanjing University
China
Two Approaches to Fast Bytecode Frontend for Static Analysis
Committee Member in Program Committee within the SAS -track
Yudai Tanabe
Tanabe, Yudai
Institute of Science Tokyo
Japan
Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Dixin Tang
Tang, Dixin
University of Texas Austin
Homomorphism Calculus for User-Defined Aggregations
Lingjia Tang
Tang, Lingjia
University of Michigan
MTP: A Meaning-Typed Language Abstraction for AI-Integrated Programming
Wenhao Tang
Tang, Wenhao
The University of Edinburgh
United Kingdom
Modal Effect Types
Yutian Tang
Tang, Yutian
University of Glasgow, United Kingdom
United Kingdom
Artemis: Toward Accurate Detection of Server-Side Request Forgeries through LLM-Assisted Inter-Procedural Path-Sensitive Taint Analysis
Swamit Tannu
Tannu, Swamit
University of Wisconsin-Madison
Dependency-Aware Compilation for Surface Code Quantum Architectures
Compiling Quantum Circuits
Éric Tanter
Tanter, Éric
University of Chile
Chile
Incremental Certified Programming
Robust Dynamic Embedding for Gradual Typing
Muhammad Usman Tariq
Tariq, Muhammad Usman
Stanford University
REPTILE: Performant Tiling of Recurrences
Joseph Tassarotti
Tassarotti, Joseph
New York University
United States
Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs
Christine Tasson
Tasson, Christine
Sorbonne Université — LIP6
France
Committee Member in ICFP Programme Committee within the ICFP Papers-track
Ross Tate
Tate, Ross
Independent Researcher and Consultant
United States
Type-Outference with Label-Listeners: Foundations for Decidable Type-Consistency for Nominal Object-Oriented Generics
Mohit Tekriwal
Tekriwal, Mohit
Lawrence Livermore National Laboratory
United States
Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Mohit Tekriwal
Tekriwal, Mohit
Lawrence Livermore National Laboratory
United States
Committee Member in Program Committee within the SAS -track
Joshua B. Tenenbaum
Tenenbaum, Joshua B.
Massachusetts Institute of Technology
United States
Gauguin, Descartes, Bayes: A Diurnal Golem's Brain
A Domain-Specific Probabilistic Programming Language for Reasoning about Reasoning (or: a memo on memo)
Tachio Terauchi
Terauchi, Tachio
Waseda University
Japan
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Manas Thakur
Thakur, Manas
IIT Bombay
India
CoSSJIT: Combining Static Analysis and Speculation in JIT Compilers
SRC Judge & Co-Organizer in Competition Judges within the SPLASH Student Research Competition-track
Committee Member in Program Committee within the SAS -track
Michelle Thalakottur
Thalakottur, Michelle
Northeastern University
United States
Student Volunteer Co-Chair in Organizing Committee for SPLASH 2025
Suhas Thalanki
Thalanki, Suhas
Carnegie Mellon University
Debugging WebAssembly? Put some Whamm on it!
Peter Thiemann
Thiemann, Peter
University of Freiburg
Germany
Session Chair of Proofs (part of SPLASH OOPSLA)
Borrowing From Session Types
Associate Chair in ICFP Programme Committee within the ICFP Papers-track
Session Chair of Tuesday ICFP Keynote (part of ICFP Keynotes)
Thore Thießen
Thießen, Thore
University of Münster
Porpoise: An LLM-Based Sandbox for Novices to Practice Writing Purpose Statements
Will Thomas
Thomas, Will
University of Kansas
Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Yongqiang Tian
Tian, Yongqiang
Monash University
Hong Kong SAR China
Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Boosting Program Reduction with the Missing Piece of Syntax-Guided Transformations
Matthias Tichy
Tichy, Matthias
Ulm University
Germany
Statically Analyzing the Dataflow of R Programs
Waddle: A Serious Game to Teach Writing, Reading, and Debugging Programs
Eli Tilevich
Tilevich, Eli
Virginia Tech
United States
Committee Member in Program Commitee within the SPLASH -E-track
Amin Timany
Timany, Amin
Aarhus University
Denmark
Reasoning about Weak Isolation Levels in Separation Logic
Christopher Steven Timperley
Timperley, Christopher Steven
Carnegie Mellon University
United States
ROSpec: A Domain-Specific Language for ROS-based Robot Software
Frank Tip
Tip, Frank
Northeastern University
United States
Steering Committee Member in Steering Committee for SPLASH 2025
Tanmay Tirpankar
Tirpankar, Tanmay
University of Utah
Translation Validation for LLVM's AArch64 Backend
Ben L. Titzer
Titzer, Ben L.
Carnegie Mellon University
United States
Rebase Co-chair in Organizing Committee for SPLASH 2025
Unveiling Heisenbugs with Diversified Execution
Debugging WebAssembly? Put some Whamm on it!
WebAssembly Research Tools Tutorial
Shrey Tiwari
Tiwari, Shrey
Carnegie Mellon University
United States
Fray: An Efficient General-Purpose Concurrency Testing Platform for the JVM
Ryan Tjoa
Tjoa, Ryan
University of Washington; Jane Street
United States
Tuning Random Generators: Property-Based Testing as Probabilistic Programming
Sam Tobin-Hochstadt
Tobin-Hochstadt, Sam
Indiana University
United States
ICFP 2026 Announcement
Bernardo Toninho
Toninho, Bernardo
NOVA-LINCS; Nova University of Lisbon
Portugal
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Bernardo Toninho
Toninho, Bernardo
Instituto Superior Técnico - University of Lisbon
Portugal
Fusing Session-Typed Concurrent Programming into Functional Programming
Cassia Torczon
Torczon, Cassia
University of Pennsylvania
QED in Context: An Observation Study of Proof Assistant Users
Matías Toro
Toro, Matías
University of Chile
Chile
Flexible and Expressive Typed Path Patterns for GQL
Robust Dynamic Embedding for Gradual Typing
Committee Member in ICFP Programme Committee within the ICFP Papers-track
Laurence Tratt
Tratt, Laurence
King's College London
United Kingdom
Garbage Collection for Rust: The Finalizer Frontier
Christoph Treude
Treude, Christoph
Singapore Management University
Singapore
Reproducibility Debt in Scientific Software
Conan Truong
Truong, Conan
University of California, Irvine
Towards Verifying Crash Consistency
Yi-Zhen Tsai
Tsai, Yi-Zhen
University of California, Riverside
Hambazi: Spatial Coordination Synthesis for Augmented Reality
Stelios Tsampas
Tsampas, Stelios
University of Southern Denmark
Denmark
Bialgebraic Reasoning on Stateful Languages
CRDT Emulation, Simulation, and Representation Independence
Big Steps in Higher-Order Mathematical Operational Semantics
Ilias Tsatiris
Tsatiris, Ilias
Dedaub
Greece
Universal Scalability in Declarative Program Analysis (with Choice-Based Combination Pruning)
Saar Tzour-Shaday
Tzour-Shaday, Saar
Technion – Israel Institute of Technology
Israel
Mini-Batch Robustness Verification of Deep Neural Networks
Thien Udomsrirungruang
Udomsrirungruang, Thien
University of Oxford
qblaze: An Efficient and Scalable Sparse Quantum Simulator
Tomoharu Ugawa
Ugawa, Tomoharu
University of Tokyo
Japan
Session Chair of Languages (part of SPLASH Onward! Papers)
Hiroshi Unno
Unno, Hiroshi
Tohoku University
Japan
On Higher-Order Model Checking of Effectful Answer-Type-Polymorphic Programs
Committee Member in ICFP Programme Committee within the ICFP Papers-track
Caterina Urban
Urban, Caterina
Inria & ENS | PSL
France
Relating Distances and Abstractions: An Abstract Interpretation Perspective
Committee Member in Program Committee within the SAS -track
Committee Member in Steering Committee within the SAS -track
Henning Urbat
Urbat, Henning
Friedrich-Alexander University Erlangen-Nürnberg
Germany
Session Chair of Semantics (part of ICFP Papers)
Bialgebraic Reasoning on Stateful Languages
Jan Vahrenhold
Vahrenhold, Jan
University of Münster
Germany
Porpoise: An LLM-Based Sandbox for Novices to Practice Writing Purpose Statements
Nachiappan Valliappan
Valliappan, Nachiappan
University of Edinburgh
United Kingdom
Committee Member in ICFP Programme Committee within the ICFP Papers-track
Milla Valnet
Valnet, Milla
Sorbonne Université
France
Committee Member in SAS Artifact Evaluation Committee within the SAS Artifact-track
Isaac van Bakel
van Bakel, Isaac
ETH Zurich
Switzerland
Modular Reasoning about Global Variables and Their Initialization
Mark van den Brand
van den Brand, Mark
Eindhoven University of Technology
Netherlands
Personalization of Programming Education: An NLP-based Bi-dimensional Classification of Programming Exercises
Guy Van den Broeck
Van den Broeck, Guy
University of California at Los Angeles
Tuning Random Generators: Property-Based Testing as Probabilistic Programming
Andre van der Hoek
van der Hoek, Andre
University of California, Irvine
United States
PC Member in Program Committee within the SPLASH Onward! Essays-track
Tijs van der Storm
van der Storm, Tijs
CWI & University of Groningen
Netherlands
Steering Committee Member in Onward! Steering Committee within the SPLASH Onward! Essays-track
Committee Member in Program Committee within the SPLASH Onward! Papers-track
Steering Committee Member in Steering Committee within the SPLASH Onward! Papers-track
Noah Van Es
Van Es, Noah
Sofware Languages Lab, Vrije Universiteit Brussel
Belgium
Delta Store Semantics: Abstract Garbage Collection for Abstract Definitional Interpreters
Monarch: A Modular Framework for Abstract Definitional Interpreters in Haskell
Jacob Van Geffen
Van Geffen, Jacob
Veridise Inc.
Scalable and Accurate Application-level Crash-Consistency Testing via Representative Testing
Eric Van Wyk
Van Wyk, Eric
University of Minnesota, Twin Cities
United States
Steering Committee Member in Steering Committee for SPLASH 2025
Bram Vandenbogaerde
Vandenbogaerde, Bram
Software Languages Lab, Vrije Universiteit Brussel
Belgium
Abstracting Concolic Execution for Soft Contract Verification
Delta Store Semantics: Abstract Garbage Collection for Abstract Definitional Interpreters
Monarch: A Modular Framework for Abstract Definitional Interpreters in Haskell
Frederik Vandeputte
Vandeputte, Frederik
Nokia Bell Labs
Foundational Design Principles and Patterns for Building Robust & Adaptive GenAI-Native Systems
Sushen Vangeepuram
Vangeepuram, Sushen
Iowa State University
Embedding Quantum Program Verification into Dafny
Alexa VanHattum
VanHattum, Alexa
Wellesley College
United States
Scaling Instruction-Selection Verification against Authoritative ISA Semantics
Vasco T. Vasconcelos
Vasconcelos, Vasco T.
LASIGE, University of Lisbon
Portugal
Steering Committee Member in Steering Committee for SPLASH 2025
Steering Committee Member in Onward! Steering Committee within the SPLASH Onward! Essays-track
Borrowing From Session Types
Session Chair of Tools (part of SPLASH Onward! Papers)
Steering Committee Member in Steering Committee within the SPLASH Onward! Papers-track
Martin Vechev
Vechev, Martin
ETH Zurich
Switzerland
qblaze: An Efficient and Scalable Sparse Quantum Simulator
Jyothi Vedurada
Vedurada, Jyothi
IIT Hyderabad
India
Committee Member in Review Committee within the SPLASH Student Research Competition-track
Andreas Veneris
Veneris, Andreas
University of Toronto
Canada
HEMVM: a Heterogeneous Blockchain Framework for Interoperable Virtual Machines
Hristo Venev
Venev, Hristo
INSAIT, Sofia University "St. Kliment Ohridski"
Bulgaria
qblaze: An Efficient and Scalable Sparse Quantum Simulator
Sarah Verbelen
Verbelen, Sarah
Vrije Universiteit Brussel, Belgium
Monarch: A Modular Framework for Abstract Definitional Interpreters in Haskell
Vasudev Vikram
Vikram, Vasudev
Carnegie Mellon University
United States
Fray: An Efficient General-Purpose Concurrency Testing Platform for the JVM
Cosmo Viola
Viola, Cosmo
University of Illinois Urbana-Champaign
Proof Repair across Quotient Type Equivalences
Harishankar Vishwanathan
Vishwanathan, Harishankar
Comparing the Precision of Abstract Operators in the eBPF Verifier using Differential Synthesis
Mahesh Viswanathan
Viswanathan, Mahesh
University of Illinois at Urbana-Champaign
United States
Checking $\delta$-Satisfiability of Reals with Integrals
Jan Vitek
Vitek, Jan
Northeastern University
United States
Steering Committee Chair in Steering Committee for SPLASH 2025
Yakir Vizel
Vizel, Yakir
Technion—Israel Institute of Technology
Israel
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Arya Vohra
Vohra, Arya
University of Chicago
Mind the Abstraction Gap: Bringing Equality Saturation to Real-World ML Compilers
Finn Voichick
Voichick, Finn
University of Maryland
United States
Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Compositional Quantum Control Flow with Efficient Compilation in Qunity
David Voigt
Voigt, David
University of Tübingen
Dynamic Wind for Effect Handlers
Domagoj Vrgoč
Vrgoč, Domagoj
Pontificia Universidad Católica de Chile & IMFD Chile
Flexible and Expressive Typed Path Patterns for GQL
Philip Wadler
Wadler, Philip
IOG; University of Edinburgh
United Kingdom
[Closed Session] Adjudication meeting for SIGPLAN's John Vlissides award
Committee Member in Program Committee and Panel within the SPLASH Doctoral Symposium-track
Session Chair of Parametricity (part of ICFP Papers)
Andrew Wagner
Wagner, Andrew
Northeastern University
United States
From Linearity to Borrowing
Gijs Walravens
Walravens, Gijs
Eindhoven University of Technology
Personalization of Programming Education: An NLP-based Bi-dimensional Classification of Programming Exercises
Michael Walter
Walter, Michael
Ruhr-Universität Bochum
QbC: Quantum Correctness by Construction
Bo Wang
Wang, Bo
Beijing Jiaotong University
China
Fuzzing C++ Compilers via Type-Driven Mutation
Chao Wang
Wang, Chao
University of Southern California
United States
Probabilistic Inference for Datalog with Correlated Inputs
Claire Wang
Wang, Claire
University of Pennsylvania
Rocq N'Roll
Concert: RocqNRoll
Di Wang
Wang, Di
Peking University
China
Automatic Linear Resource Bound Analysis for Rust via Prophecy Potentials
Hanzhang Wang
Wang, Hanzhang
Fudan University, China
China
JavART: a Lightweight Rule-Based JIT Compiler Using Translation Rules Extracted from a Learning Approach
Jianrong Wang
Wang, Jianrong
Tianjin University
China
DESIL: Detecting Silent Bugs in MLIR Compiler Infrastructure
Jiawei Wang
Wang, Jiawei
UNSW
Efficient Abstract Interpretation via Selective Widening
Jingbo Wang
Wang, Jingbo
Purdue University
Probabilistic Inference for Datalog with Correlated Inputs
Ke Wang
Wang, Ke
Peking University
Synchronized Behavior Checking: A Method for Finding Missed Compiler Optimizations
Linzhang Wang
Wang, Linzhang
Nanjing University
Synchronized Behavior Checking: A Method for Finding Missed Compiler Optimizations
Peixin Wang
Wang, Peixin
East China Normal University
Structural Abstraction and Refinement for Probabilistic Programs
Ruixin Wang
Wang, Ruixin
Purdue University
United States
Show Me Why It's Correct: Saving 1/3 of Debugging Time in Program Repair with Interactive Runtime Comparison
Shengyi Wang
Wang, Shengyi
Princeton University
United States
Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Shiqi Wang
Wang, Shiqi
AWS AI Labs
United States
UTFix: Change Aware Unit Test Repairing using LLM
Shuai Wang
Wang, Shuai
Hong Kong University of Science and Technology
China
Extraction and Mutation at a High Level: Template-Based Fuzzing for JavaScript Engines
API-guided Dataset Synthesis to Finetune Large Code Models
Binary Cryptographic Function Identification via Similarity Analysis with Path-insensitive Emulation
Shuling Wang
Wang, Shuling
Institute of Software, Chinese Academy of Sciences
HpC: A Calculus for Hybrid and Mobile Systems
Wenwen Wang
Wang, Wenwen
University of Georgia
United States
JavART: a Lightweight Rule-Based JIT Compiler Using Translation Rules Extracted from a Learning Approach
Wenxi Wang
Wang, Wenxi
University of Virgina
United States
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
XiaoFeng Wang
Wang, XiaoFeng
Nanyang Technological University
Agora: Trust Less and Open More in Verification for Confidential Computing
Xinyu Wang
Wang, Xinyu
University of Michigan
United States
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Yongjia Wang
Wang, Yongjia
College of Intelligence and Computing, Tianjin University
DESIL: Detecting Silent Bugs in MLIR Compiler Infrastructure
Yongzhi Wang
Wang, Yongzhi
Xidian University
HybridPersist: A Compiler Support for User-Friendly and Efficient PM Programming
Yu Wang
Wang, Yu
Nanjing University
China
Synchronized Behavior Checking: A Method for Finding Missed Compiler Optimizations
Yuepeng Wang
Wang, Yuepeng
Simon Fraser University
Canada
Committee Member in Program Committee within the SAS -track
Yuning Wang
Wang, Yuning
Rutgers University
Abstraction Refinement-guided Program Synthesis for Robot Learning from Demonstrations
Zhuangda Wang
Wang, Zhuangda
Xiamen University
China
TailTracer: Continuous Tail Tracing for Production Use
Zihan Wang
Wang, Zihan
The University of Queensland and CSIRO's Data61
Australia
Convex Hull Approximation for Activation Functions
Ziteng Wang
Wang, Ziteng
University of Texas at Austin
United States
Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Homomorphism Calculus for User-Defined Aggregations
Kazuki Watanabe
Watanabe, Kazuki
National Institute of Informatics; SOKENDAI
Japan
A Unifying Approach to Product Constructions for Quantitative Temporal Inference
Conrad Watt
Watt, Conrad
Nanyang Technological University
Singapore
Doctoral Symposium Chair in Organizing Committee for SPLASH 2025
Session Chair of Session 2 (part of SPLASH Doctoral Symposium)
Session Chair of Session 1 (part of SPLASH Doctoral Symposium)
Introductions
[Closed Session] Adjudication meeting for SIGPLAN's John Vlissides award
Organizing Chair in Program Committee and Panel within the SPLASH Doctoral Symposium-track
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
WebAssembly Research Tools Tutorial
Joe Watt
Watt, Joe
Institute for Infocomm Research, A*STAR
Singapore
Student Volunteer Co-Chair in Organizing Committee for SPLASH 2025
Tan Wei Han
Wei Han, Tan
Local Arrangements Chair in Organizing Committee for SPLASH 2025
Anjiang Wei
Wei, Anjiang
Stanford University
United States
Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Guannan Wei
Wei, Guannan
Tufts University
United States
Modeling Reachability Types with Logical Relations -- Semantic Type Soundness, Termination, Effect Safety, and Equational Theory
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Committee Member in ICFP Programme Committee within the ICFP Papers-track
Ivan Wei
Wei, Ivan
University of Michigan
Incremental Bidirectional Typing via Order Maintenance
Stephanie Weirich
Weirich, Stephanie
University of Pennsylvania
United States
Committee Member in ICFP Programme Committee within the ICFP Papers-track
Hongbo Wen
Wen, Hongbo
University of California, Santa Barbara & Riema Labs
Tabby: A Synthesis-Aided Compiler for High-Performance Zero-Knowledge Proof Circuits
Zhongzhen Wen
Wen, Zhongzhen
Nanjing University
China
PReMM: LLM-Based Program Repair for Multi-Method Bugs via Divide and Conquer
Sam Westrick
Westrick, Sam
New York University
United States
Committee Member in Program Committee within the SPLASH FARM-track
Leo White
White, Leo
Jane Street
United Kingdom
Modal Effect Types
Committee Member in ICFP Programme Committee within the ICFP Papers-track
John Wickerson
Wickerson, John
Imperial College London
United Kingdom
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Thomas Wies
Wies, Thomas
New York University
United States
Abstract Interpretation of Temporal Safety Effects of Higher Order Programs
Characterizing Implementability of Global Protocols with Infinite States and Data
Graham Williams
Williams, Graham
Australian National University
Reproducibility Debt in Scientific Software
Richard Willie
Willie, Richard
National University of Singapore
View Types in Rust
Christian Wimmer
Wimmer, Christian
Amazon Web Services
United States
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Tobias Winkler
Winkler, Tobias
RWTH Aachen University
Germany
Foundations for Deductive Verification of Continuous Probabilistic Programs: From Lebesgue to Riemann and Back
Daniel Winograd-Cort
Winograd-Cort, Daniel
Nectry Inc.
United States
Sponsorship Co-Chair in Organizing Committee for SPLASH 2025
Théo Winterhalter
Winterhalter, Théo
INRIA
France
SecRef*: Securely Sharing Mutable References between Verified and Unverified Code in F*
Committee Member in ICFP Programme Committee within the ICFP Papers-track
Jaeyeon Won
Won, Jaeyeon
MIT
The Continuous Tensor Abstraction: Where Indices are Real
Jotham Wong
Wong, Jotham
National University of Singapore, Singapore
Singapore
Evolving How We Teach Memory Models
Wai Kin Wong
Wong, Wai Kin
Hong Kong University of Science and Technology
Extraction and Mutation at a High Level: Template-Based Fuzzing for JavaScript Engines
Daniel Wright
Wright, Daniel
University of Surrey
Symbolic MRD: Dynamic Memory, Undefined Behaviour, and Extrinsic Choice
Tobias Wrigstad
Wrigstad, Tobias
Uppsala University
Sweden
Associate Chair in OOPSLA Review Committee within the SPLASH OOPSLA-track
Daoyuan Wu
Wu, Daoyuan
Lingnan University
Hong Kong SAR China
Extraction and Mutation at a High Level: Template-Based Fuzzing for JavaScript Engines
API-guided Dataset Synthesis to Finetune Large Code Models
Jiangchang Wu
Wu, Jiangchang
Nanjing University
China
Validating SMT Rewriters via Rewrite Space Exploration Supported by Generative Equality Saturation
Ming Wu
Wu, Ming
Shanghai Tree-Graph Blockchain Research Institute
HEMVM: a Heterogeneous Blockchain Framework for Interoperable Virtual Machines
Rongxin Wu
Wu, Rongxin
Xiamen University
China
TailTracer: Continuous Tail Tracing for Production Use
Shushu Wu
Wu, Shushu
Shanghai Jiao Tong University
Encode the $\forall\exists$ Relational Hoare Logic into Standard Hoare Logic
Xiwei Wu
Wu, Xiwei
Shanghai Jiao Tong University
China
Encode the $\forall\exists$ Relational Hoare Logic into Standard Hoare Logic
Dongwei Xiao
Xiao, Dongwei
Hong Kong University of Science and Technology
Hong Kong SAR China
Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Extraction and Mutation at a High Level: Template-Based Fuzzing for JavaScript Engines
Junmin Xiao
Xiao, Junmin
Stencil-Lifting: Hierarchical Recursive Lifting System for Extracting Summary of Stencil Kernel in Legacy Codes
Linjie Xiao
Xiao, Linjie
Ant Group
MetaKernel: Enabling Efficient Encrypted Neural Network Inference Through Unified MVM and Convolution
Linna Xie
Xie, Linna
Nanjing University
China
PReMM: LLM-Based Program Repair for Multi-Method Bugs via Divide and Conquer
Ningning Xie
Xie, Ningning
University of Toronto
Canada
Multi-stage Programming with Splice Variables
Committee Member in ICFP Programme Committee within the ICFP Papers-track
Ruifeng Xie
Xie, Ruifeng
Peking University
Effectful Lenses: There and Back with Different Monads
Zifan Xie
Xie, Zifan
Huazhong University of Science and Technology
China
Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Jimmy Xin
Xin, Jimmy
The University of Texas at Austin
Automated Discovery of Tactic Libraries for Interactive Theorem Proving
Yutong Xin
Xin, Yutong
The University of Texas at Austin
Automated Discovery of Tactic Libraries for Interactive Theorem Proving
Chris Xiong
Xiong, Chris
Ohio State University
Carapace: Static–Dynamic Information Flow Control in Rust
Yingfei Xiong
Xiong, Yingfei
Peking University
China
Session Chair of Synthesis 1 (part of SPLASH OOPSLA)
Tunneling Through the Hill: Multi-Way Intersection for Version-Space Algebras in Program Synthesis
Amanda Xu
Xu, Amanda
University of Wisconsin-Madison
How to Synthesize Quantum-Circuit Optimizers
Dependency-Aware Compilation for Surface Code Quantum Architectures
Checking Observational Correctness of Database Systems
Compiling Quantum Circuits
Baowen Xu
Xu, Baowen
Nanjing University
An Empirical Study of Bugs in the rustc Compiler
Han Xu
Xu, Han
Princeton University
United States
Liberating Merges via Apartness and Guarded Subtyping
Jiexiao Xu
Xu, Jiexiao
University of Washington
Scalable and Accurate Application-level Crash-Consistency Testing via Representative Testing
Xiangzhe Xu
Xu, Xiangzhe
Purdue University
United States
Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Committee Member in SAS Artifact Evaluation Committee within the SAS Artifact-track
Xiong Xu
Xu, Xiong
Institute of Software, Chinese Academy of Sciences
HpC: A Calculus for Hybrid and Mobile Systems
Yichen Xu
Xu, Yichen
EPFL
What's in the Box: Ergonomic and Expressive Capture Tracking over Generic Data Structures
Zhenyang Xu
Xu, Zhenyang
University of Waterloo
Canada
Boosting Program Reduction with the Missing Piece of Syntax-Guided Transformations
Jingling Xue
Xue, Jingling
University of New South Wales
Australia
Fast Client-Driven CFL-Reachability via Regularization-Based Graph Simplification
MetaKernel: Enabling Efficient Encrypted Neural Network Inference Through Unified MVM and Convolution
Runze Xue
Xue, Runze
University of Michigan; University of Cambridge; Indiana University
United States
Notions of Stack-manipulating Computation and Relative Monads
Xu Xue
Xue, Xu
The University of Hong Kong
Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Berk Yagli
Yagli, Berk
Concert: False Awakening on a Mediterranean Island
Jeremy Yallop
Yallop, Jeremy
University of Cambridge
United Kingdom
Frex: Dependently Typed Algebraic Simplification
Zhenyu Yan
Yan, Zhenyu
Peking University
China
Committee Member in SAS Artifact Evaluation Committee within the SAS Artifact-track
Chenyuan Yang
Yang, Chenyuan
University of Illinois Urbana-Champaign
United States
AutoVerus: Automated Proof Generation for Rust Code
Fan Yang
Yang, Fan
Microsoft Research Asia
AutoVerus: Automated Proof Generation for Rust Code
Min Yang
Yang, Min
Fudan University
China
ApkDiffer: Accurate and Scalable Cross-Version Diffing Analysis for Android Applications
Minghui Yang
Yang, Minghui
OPPO
ApkDiffer: Accurate and Scalable Cross-Version Diffing Analysis for Android Applications
Sen Yang
Yang, Sen
Yale University
Agora: Trust Less and Open More in Verification for Confidential Computing
Shengyuan Yang
Yang, Shengyuan
University of Wisconsin-Madison
Committee Member in SAS Artifact Evaluation Committee within the SAS Artifact-track
Yibiao Yang
Yang, Yibiao
Nanjing University
China
Validating SMT Rewriters via Rewrite Space Exploration Supported by Generative Equality Saturation
Yixin Yang
Yang, Yixin
Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Ziyi Yang
Yang, Ziyi
National University of Singapore
Singapore
Inductive Synthesis of Inductive Heap Predicates
Jianan Yao
Yao, Jianan
University of Toronto
AutoVerus: Automated Proof Generation for Rust Code
Peisen Yao
Yao, Peisen
Zhejiang University
China
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Bounded-Exhaustive Subspace Diversification for SMT Solver Testing
Committee Member in Program Committee within the SAS -track
Wenjia Ye
Ye, Wenjia
National University of Singapore
Singapore
Flexible and Expressive Typed Path Patterns for GQL
Pen-Chung Yew
Yew, Pen-Chung
University of Minnesota at Twin Cities
United States
JavART: a Lightweight Rule-Based JIT Compiler Using Translation Rules Extracted from a Learning Approach
Jooyong Yi
Yi, Jooyong
UNIST
South Korea
Committee Member in Program Committee within the SAS -track
Kwangkeun Yi
Yi, Kwangkeun
Seoul National University
React-tRace: A Semantics for Understanding React Hooks
Xizhe Yin
Yin, Xizhe
Nanjing University
China
An Empirical Study of Bugs in the rustc Compiler
Irene Yoon
Yoon, Irene
Inria
France
Formal Semantics and Program Logics for a Fragment of OCaml
Committee Member in ICFP Programme Committee within the ICFP Papers-track
Taeyoung Yoon
Yoon, Taeyoung
Seoul National University
Lilo: A Higher-Order, Relational Concurrent Separation Logic for Liveness
Nobuko Yoshida
Yoshida, Nobuko
University of Oxford
United Kingdom
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Shu-Hung You
You, Shu-Hung
Institute of Information Science, Academia Sinica, Taiwan
Taiwan
Contract System Metatheories à la Carte: A Transition-System View of Contracts
David Young
Young, David
University of Kansas, USA
A Haskell Adiabatic DSL: Solving Classical Optimization Problems on Quantum Hardware
Neringa Young
Young, Neringa
Lithuania
SIGPLAN Conference Manager in Organizing Committee for SPLASH 2025
Nengkun Yu
Yu, Nengkun
Stony Brook University, USA
United States
Scalable Equivalence Checking and Verification of Shallow Quantum Circuits
Liang Yuan
Yuan, Liang
Chinese Academy of Sciences
Stencil-Lifting: Hierarchical Recursive Lifting System for Extracting Summary of Stencil Kernel in Legacy Codes
Peng Yuan
Yuan, Peng
Ant Group
MetaKernel: Enabling Efficient Encrypted Neural Network Inference Through Unified MVM and Convolution
Shenghao Yuan
Yuan, Shenghao
Zhejiang University
A complete formal semantics of eBPF instruction set architecture for Solana
Yongwei Yuan
Yuan, Yongwei
Purdue University
United States
Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Yueming Yuan
Yuan, Yueming
University of Illinois Urbana-Champaign
SPLAT: A framework for optimised GPU code-generation for SParse reguLar ATtention
Zhou Yuanyuan
Yuanyuan, Zhou
UCSD
On the Impact of Formal Verification on Software Development
Laurel: Unblocking Automated Verification with Large Language Models
Insu Yun
Yun, Insu
KAIST
Bridging the Gap between Real-World and Formal Binary Lifting through Filtered-Simulation
Tom Yuviler
Yuviler, Tom
Technion
Enhancing Neural Network Robustness via Synthesis of Repair Programs
Enea Zaffanella
Zaffanella, Enea
University of Parma
Italy
Committee Member in Program Committee within the SAS -track
Yannick Zakowski
Zakowski, Yannick
Inria
France
Structural temporal logic for mechanized program verification
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Giacomo Zanatta
Zanatta, Giacomo
Ca’ Foscari University of Venice
Italy
Committee Member in SAS Artifact Evaluation Committee within the SAS Artifact-track
Lucas Zavalia
Zavalia, Lucas
Florida State University Tallahassee
United States
A Flow-Sensitive Refinement Type System for Verifying eBPF Programs
Steve Zdancewic
Zdancewic, Steve
University of Pennsylvania
United States
Opportunistically Parallel Lambda Calculus
Structural temporal logic for mechanized program verification
Stefan Zetzsche
Zetzsche, Stefan
Amazon
United Kingdom
Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Thomas Zeume
Zeume, Thomas
Ruhr University Bochum
Germany
Detecting and explaining (in-)equivalence of context-free grammars
Bohua Zhan
Zhan, Bohua
Huawei Technologies Co., Ltd.
HpC: A Calculus for Hybrid and Mobile Systems
Naijun Zhan
Zhan, Naijun
Peking University
HpC: A Calculus for Hybrid and Mobile Systems
Chaoyue Zhang
Zhang, Chaoyue
Nanjing University
China
Towards a Theoretically-Backed and Practical Framework for Selective Object-Sensitive Pointer Analysis
Charles Zhang
Zhang, Charles
The Hong Kong University of Science and Technology
China
Steering Committee Member in Steering Committee for SPLASH 2025
General Chair in Organizing Committee for SPLASH 2025
Session Chair of Friday SPLASH Keynote (part of SPLASH Keynotes)
Session Chair of TOPLAS and Remote (part of SPLASH OOPSLA)
SPLASH Awards
General Chair Report
Cheng Zhang
Zhang, Cheng
Worcester Polytechnic Institute
United States
Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Chengyu Zhang
Zhang, Chengyu
ETH Zurich
Validating Soundness and Completeness in Pattern-Match Coverage Analyzers
Danfeng Zhang
Zhang, Danfeng
Duke University
United States
Agora: Trust Less and Open More in Verification for Confidential Computing
Fan Zhang
Zhang, Fan
Yale University
Agora: Trust Less and Open More in Verification for Confidential Computing
Jialu Zhang
Zhang, Jialu
University of Waterloo
Canada
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Mengxiao Zhang
Zhang, Mengxiao
Boosting Program Reduction with the Missing Piece of Syntax-Guided Transformations
Nuda Zhang
Zhang, Nuda
University of Michigan
Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Qirun Zhang
Zhang, Qirun
Georgia Institute of Technology
United States
Poster Co-Chair in Organizing Committee for SPLASH 2025
Fast Constraint Synthesis for C++ Function Templates
Chair in Organizing Committee within the SPLASH Posters-track
From Within: Compiler Testing and Validation via Compilers
Committee Member in Program Committee within the SAS -track
Ruihan Zhang
Zhang, Ruihan
Singapore Management University (SMU)
Correct-By-Construction: Certified Individual Fairness through Neural Network Training
Shuhao Zhang
Zhang, Shuhao
Peking University
China
Tunneling Through the Hill: Multi-Way Intersection for Version-Space Algebras in Program Synthesis
Teng Zhang
Zhang, Teng
Nanjing University
China
Committee Member in SAS Artifact Evaluation Committee within the SAS Artifact-track
Tian Zhang
Zhang, Tian
Nanjing University
China
PReMM: LLM-Based Program Repair for Multi-Method Bugs via Divide and Conquer
Tianyi Zhang
Zhang, Tianyi
Purdue University
United States
Show Me Why It's Correct: Saving 1/3 of Debugging Time in Program Repair with Interactive Runtime Comparison
Weihua Zhang
Zhang, Weihua
Fudan University
China
JavART: a Lightweight Rule-Based JIT Compiler Using Translation Rules Extracted from a Learning Approach
Wenmeng Zhang
Zhang, Wenmeng
College of Computer Science and Technology, National University of Defense Technology, Changsha, China
Multi-Modal Sketch-based Behavior Tree Synthesis
Xiangyu Zhang
Zhang, Xiangyu
Purdue University
United States
Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Xiaojing Zhang
Zhang, Xiaojing
Ant Group
MetaKernel: Enabling Efficient Encrypted Neural Network Inference Through Unified MVM and Convolution
Xin Zhang
Zhang, Xin
Peking University
China
Combining Formal and Informal Information in Bayesian Program Analysis via Soft Evidences
On Abstraction Refinement for Bayesian Program Analysis
Committee Member in Program Committee within the SAS -track
Xing Zhang
Zhang, Xing
Peking University
China
Fuzzing C++ Compilers via Type-Driven Mutation
Yedi Zhang
Zhang, Yedi
National University of Singapore
Verification of Bit-Flip Attacks against Quantized Neural Networks
Yi Zhang
Zhang, Yi
Nanjing University
China
Synchronized Behavior Checking: A Method for Finding Missed Compiler Optimizations
Yifan Zhang
Zhang, Yifan
Peking University
China
On Abstraction Refinement for Bayesian Program Analysis
Ying Zhang
Zhang, Ying
Wake Forest University
United States
Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Yiyu Zhang
Zhang, Yiyu
Nanjing University
China
HybridPersist: A Compiler Support for User-Friendly and Efficient PM Programming
TailTracer: Continuous Tail Tracing for Production Use
Yizhou Zhang
Zhang, Yizhou
University of Waterloo
Canada
Zero-Overhead Lexical Effect Handlers
Compiling with Generating Functions
Yuan Zhang
Zhang, Yuan
Fudan University
China
ApkDiffer: Accurate and Scalable Cross-Version Diffing Analysis for Android Applications
Zhaoyang Zhang
Zhang, Zhaoyang
The Hong Kong University of Science and Technology
Hong Kong SAR China
A Sound Static Analysis Approach to I/O API Migration
Zhuoruo Zhang
Zhang, Zhuoruo
Zhejiang University
A complete formal semantics of eBPF instruction set architecture for Solana
Ziqi Zhang
Zhang, Ziqi
University of Illinois Urbana-Champaign
China
Orax: A Feedback-Driven Framework for Efficiently Solving Satisfiability Modulo Theories and Oracles
Pinhan Zhao
Zhao, Pinhan
University of Michigan
United States
Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Wenyu Zhao
Zhao, Wenyu
Australian National University
Australia
Advancing Performance via a Systematic Application of Research and Industrial Best Practice
Work Packets: A New Abstraction for GC Software Engineering, Optimization, and Innovation
Yongwang Zhao
Zhao, Yongwang
Zhejiang University
A complete formal semantics of eBPF instruction set architecture for Solana
Yubo Zhao
Zhao, Yubo
Shanghai Jiao Tong University
Binary Cryptographic Function Identification via Similarity Analysis with Path-insensitive Emulation
Zhongkai Zhao
Zhao, Zhongkai
National University of Singapore
Show Me Why It's Correct: Saving 1/3 of Debugging Time in Program Repair with Interactive Runtime Comparison
Junda Zheng
Zheng, Junda
Bounded-Exhaustive Subspace Diversification for SMT Solver Testing
Linus Zheng
Zheng, Linus
University of Texas at Austin
Homomorphism Calculus for User-Defined Aggregations
Xusheng Zhi
Zhi, Xusheng
University of Wisconsin-Madison
United States
(TOPLAS) Polynomial Bounds of CFLOBDDs against BDDs
Byron Zhong
Zhong, Byron
University of Chicago
United States
Environment-Sharing Analysis and Caller-Provided Environments for Higher-Order Languages
Sizhe Zhong
Zhong, Sizhe
The Hong Kong University of Science and Technology
A Sound Static Analysis Approach to I/O API Migration
Zhineng Zhong
Zhong, Zhineng
Key Laboratory of High-Confidence Software Technologies (MOE), School of Computer Science, Peking University
Orax: A Feedback-Driven Framework for Efficiently Solving Satisfiability Modulo Theories and Oracles
Diyu Zhou
Zhou, Diyu
Peking University
A Sound Static Analysis Approach to I/O API Migration
Litao Zhou
Zhou, Litao
University of Hong Kong
China
Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Quan Zhou
Zhou, Quan
Penn State University
Agora: Trust Less and Open More in Verification for Confidential Computing
Xiangyu Zhou
Zhou, Xiangyu
University of Michigan
Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Yanqi Zhou
Zhou, Yanqi
Google
SPLAT: A framework for optimised GPU code-generation for SParse reguLar ATtention
Yuming Zhou
Zhou, Yuming
Nanjing University
China
Validating SMT Rewriters via Rewrite Space Exploration Supported by Generative Equality Saturation
Zhe Zhou
Zhou, Zhe
Purdue University
We’ve Got You Covered: Type-Guided Repair of Incomplete Input Generators
Zhichao Zhou
Zhou, Zhichao
School of Information Science and Technology, ShanghaiTech University
China
Artemis: Toward Accurate Detection of Server-Side Request Forgeries through LLM-Assisted Inter-Procedural Path-Sensitive Taint Analysis
Ziqiao Zhou
Zhou, Ziqiao
Microsoft Research
United States
AutoVerus: Automated Proof Generation for Rust Code
He Zhu
Zhu, He
Rutgers University, USA
Abstraction Refinement-guided Program Synthesis for Robot Learning from Demonstrations
Jun Zhu
Zhu, Jun
Nankai University
Adaptive Shielding via Parametric Safety Proofs
Qing Zhu
Zhu, Qing
Ant Group
MetaKernel: Enabling Efficient Encrypted Neural Network Inference Through Unified MVM and Convolution
Siyuan Zhu
Zhu, Siyuan
Peking University, China
Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Oleksandr Zinenko
Zinenko, Oleksandr
Brium
Sound and Modular Activity Analysis for Automatic Differentiation in MLIR
Mind the Abstraction Gap: Bringing Equality Saturation to Real-World ML Compilers
Li Zongjie
Zongjie, Li
Hong Kong University of Science and Technology
China
API-guided Dataset Synthesis to Finetune Large Code Models
Damien Zufferey
Zufferey, Damien
SonarSource
Switzerland
Characterizing Implementability of Global Protocols with Infinite States and Data
Zhiqiang Zuo
Zuo, Zhiqiang
Nanjing University
China
HybridPersist: A Compiler Support for User-Friendly and Efficient PM Programming
TailTracer: Continuous Tail Tracing for Production Use
Aron Zwaan
Zwaan, Aron
Delft University of Technology
Netherlands
Language-Parametric Reference Synthesis
Artjoms Šinkarovs
Šinkarovs, Artjoms
University of Southampton
Correctness Meets Performance: From Agda to Futhark
Fri 24 Apr 20:36