SPLASH 2025 Contributors

Filter

Role Type

Contributing to

Number of Roles

Country

Results (1384)

A Zain K AamerAamer, Zain K University of PennsylvaniaUnited States Bennet: Randomized Specification Testing for Heap-Manipulating Programs
Neha AbbasAbbas, Neha University of California, Santa Cruz SafeRace: Assessing and Addressing WebGPU Memory Safety in the Presence of Data Races
Andreas AbelAbel, Andreas Gothenburg UniversitySweden Committee Member in ICFP Programme Committee within the ICFP Papers-track
Coşku AcayAcay, Coşku Observe, Inc.United States Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Michael D. AdamsAdams, Michael D. National University of SingaporeUnited States Pushing the Information-Theoretic Limits of Random Access Lists
Nicholas AdamsAdams, Nicholas None How to secure a distributed database such as OpenRiak with open-source tools
Eddie AftandilianAftandilian, Eddie GitHub NextUnited States Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Chaitanya AgarwalAgarwal, Chaitanya New York University Abstract Interpretation of Temporal Safety Effects of Higher Order Programs
Alejandro AguirreAguirre, Alejandro Aarhus UniversityDenmark Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs
Danel AhmanAhman, Danel University of LjubljanaSlovenia SecRef: Securely Sharing Mutable References between Verified and Unverified Code in F
Amal AhmedAhmed, Amal Northeastern University, USAUnited 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 AhnAhn, Joongwon Seoul National University React-tRace: A Semantics for Understanding React Hooks
Benedikt AhrensAhrens, Benedikt Delft University of TechnologyNetherlands 2-Functoriality of Initial Semantics, and Applications
Willow AhrensAhrens, Willow Massachusetts Institute of TechnologyUnited States Finch: Sparse and Structured Tensor Programming with Control Flow The Continuous Tensor Abstraction: Where Indices are Real
Marat AkhinAkhin, Marat JetBrainsNetherlands Finding Compiler Bugs through Cross-Language Code Generator and Differential Testing
Aws AlbarghouthiAlbarghouthi, Aws University of Wisconsin-MadisonUnited States Dependency-Aware Compilation for Surface Code Quantum Architectures Checking Observational Correctness of Database Systems Compiling Quantum Circuits
Jonathan AldrichAldrich, Jonathan Carnegie Mellon UniversityUnited States Structural Information Flow: A Fresh Look at Types for Non-Interference
Mark W. AldrichAldrich, Mark W. Tufts UniversityUnited States RestPi: Path-Sensitive Type Inference for REST APIs
Karim AliAli, Karim NYU Abu DhabiUnited Arab Emirates Committee Member in Program Committee within the SAS -track
Shan AliAli, Shan Yale University Coinductive Proofs of Regular Expression Equivalence in Zero Knowledge
Guillaume AllaisAllais, Guillaume University of StrathclydeUnited Kingdom Frex: Dependently Typed Algebraic Simplification Committee Member in ICFP Programme Committee within the ICFP Papers-track
Henry AllardAllard, Henry Iowa State UniversityUnited States Embedding Quantum Program Verification into Dafny
Anders Alnor MathiasenAlnor Mathiasen, Anders Aarhus UniversityDenmark Reasoning about Weak Isolation Levels in Separation Logic
Dalal AlrajehAlrajeh, Dalal Imperial College LondonUnited Kingdom Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Saman AmarasingheAmarasinghe, Saman Massachusetts Institute of TechnologyUnited States Finch: Sparse and Structured Tensor Programming with Control Flow The Continuous Tensor Abstraction: Where Indices are Real
Nada AminAmin, Nada Harvard UniversityUnited States Committee Member in ICFP Programme Committee within the ICFP Papers-track
Junwen AnAn, Junwen Singapore LLM-assisted Dialect-Agnostic SQL Query Parsing
Yujin AnAn, Yujin Chungnam National University Simplifying Lifter-generated Emulation Style LLVM IR for Analysis Suitability
Zixi AnAn, Zixi Debugging WebAssembly? Put some Whamm on it!
Aditya AnandAnand, Aditya Indian Institute of Technology BombayIndia CoSSJIT: Combining Static Analysis and Speculation in JIT Compilers
Emmanuel Anaya GonzalezAnaya Gonzalez, Emmanuel UCSD Laurel: Unblocking Automated Verification with Large Language Models
Carolyn Jane AndersonAnderson, Carolyn Jane Wellesley CollegeUnited States PC Member in Program Committee within the SPLASH Onward! Essays-track
Cezar-Constantin AndriciAndrici, Cezar-Constantin MPI-SPGermany SecRef: Securely Sharing Mutable References between Verified and Unverified Code in F
Sebastian AngelAngel, Sebastian University of PennsylvaniaUnited States Structural temporal logic for mechanized program verification
Anastasios AntoniadisAntoniadis, Anastasios University of Athens, GreeceGreece Universal Scalability in Declarative Program Analysis (with Choice-Based Combination Pruning)
Timos AntonopoulosAntonopoulos, Timos Yale UniversityUnited States Coinductive Proofs of Regular Expression Equivalence in Zero Knowledge
Meghana Aparna SistlaAparna Sistla, Meghana The University of Texas at AustinUnited States Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
David AponteAponte, David Microsoft SPLAT: A framework for optimised GPU code-generation for SParse reguLar ATtention
Vincenzo ArceriArceri, Vincenzo University of Parma, ItalyItaly Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Blair ArchibaldArchibald, Blair University of GlasgowUnited Kingdom TideScript: A Domain Specific Language for Peptide Chemistry
Sven ArgoArgo, Sven Ruhr University Bochum Detecting and explaining (in-)equivalence of context-free grammars
Kenichi AsaiAsai, Kenichi Ochanomizu UniversityJapan Committee Member in Program Commitee within the SPLASH -E-track
Flavio AscariAscari, Flavio University of Pisa Revealing Sources of (Memory) Errors via Backward Analysis
Eric AtkinsonAtkinson, 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 AustenAusten, Skyler Brown University Sharing is Scaring: Linking Cloud File-Sharing to Programming Language Semantics
Charles AverillAverill, Charles University of Texas at DallasUnited States The Proof Must Go On: Formal Methods in the Theater of Secure Software Development of the Future
Jessy AyalaAyala, Jessy University of California, IrvineUnited States Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Sacha-Élie AyounAyoun, Sacha-Élie Imperial College LondonUnited Kingdom Compositional Symbolic Execution for the Next 700 Memory Models
Pedro Henrique Azevedo de AmorimAzevedo de Amorim, Pedro Henrique Cornell University Denotational Foundations for Expected Cost Analysis
B Timur BabakolBabakol, Timur SUNY Binghamton, USA Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Casper BachBach, Casper University of Southern DenmarkDenmark Language-Parametric Reference Synthesis
Jakub BachurskiBachurski, Jakub University of CambridgeUnited Kingdom Mind the Abstraction Gap: Bringing Equality Saturation to Real-World ML Compilers
Kyungmin BaeBae, Kyungmin POSTECHSouth Korea Formal Analysis of Networked PLC Controllers Interacting with Physical Environments Committee Member in Program Committee within the SAS -track
Thomas BAGRELBAGREL, Thomas Tweag, LORIA/INRIA Destination calculus: A linear λ-calculus for purely functional memory writes
Alexander BaiBai, Alexander New York UniversityUnited 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 BaiBai, Guangdong University of QueenslandAustralia Convex Hull Approximation for Activation Functions
Hrishikesh BalakrishnanBalakrishnan, Hrishikesh University of Illinois Urbana-Champaign FO-Complete Program Verification for Heap Logics
Lucas BangBang, Lucas Harvey Mudd College PLMW Co-Chair in Organizing Committee for SPLASH 2025
Elisa BaniassadBaniassad, Elisa University of British ColumbiaCanada Committee Member in Program Commitee within the SPLASH -E-track
Peihua BaoBao, Peihua University of Chinese Academy of Sciences Stencil-Lifting: Hierarchical Recursive Lifting System for Extracting Summary of Stencil Kernel in Legacy Codes
Yuyan BaoBao, Yuyan Augusta UniversityUnited 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 BarashBarash, Mikhail University of BergenNorway Involving Students in Design and Implementation of ECMAScript (JavaScript) Proposals
Sébastien BardinBardin, Sébastien CEA LIST, University Paris-SaclayFrance Committee Member in Program Committee within the SAS -track
Shraddha BarkeBarke, Shraddha Microsoft Research, RedmondUnited States PC Member in Program Committee within the SPLASH Onward! Essays-track
Celeste BarnabyBarnaby, Celeste University of Texas at AustinUnited States Active Learning for Neurosymbolic Program Synthesis
Dan BarowyBarowy, Dan Williams CollegeUnited States Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Clark BarrettBarrett, Clark Stanford UniversityUnited States Interactive Bit Vector Reasoning using Verified Bitblasting
Aurèle BarrièreBarrière, Aurèle EPFLSwitzerland Committee Member in ICFP Programme Committee within the ICFP Papers-track
Antranig BasmanBasman, Antranig Raising the Floor - InternationalUnited Kingdom Committee Member in Program Committee within the SPLASH Onward! Papers-track
Matteo BassoBasso, 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 BastaniBastani, Osbert University of PennsylvaniaUnited States Opportunistically Parallel Lambda Calculus Active Learning for Neurosymbolic Program Synthesis
Mark BattyBatty, Mark University of KentUnited Kingdom Symbolic MRD: Dynamic Memory, Undefined Behaviour, and Extrinsic Choice
Kevin BatzBatz, Kevin RWTH Aachen UniversityGermany Foundations for Deductive Verification of Continuous Probabilistic Programs: From Lebesgue to Riemann and Back
Guillaume BaudartBaudart, Guillaume InriaFrance Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Emilien BauerBauer, Emilien Compressed and Parallelized Structured Tensor Algebra
Rohan BavishiBavishi, Rohan AmazonUnited 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 BelyakovaBelyakova, Julia Purdue UniversityUnited States Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Aaron BembenekBembenek, Aaron The University of MelbourneAustralia Current Practices for Building LLM-Powered Reasoning Tools Are Ad Hoc—and We Can do Better
Dorra Ben KhalifaBen Khalifa, Dorra ENAC - University of ToulouseFrance 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 BensoussanBensoussan, Avner King's College LondonUnited Kingdom Shaking Up Quantum Simulators with Fuzzing and Rigour AccelerQ: Accelerating Quantum Eigensolvers With Machine Learning on Quantum Simulators
Nick BentonBenton, Nick MetaUnited Kingdom Committee Member in ICFP Programme Committee within the ICFP Papers-track
Ryan BergerBerger, Ryan Nvidia Translation Validation for LLVM's AArch64 Backend
Simon BerlingerBerlinger, Simon Ulm University, Germany Waddle: A Serious Game to Teach Writing, Reading, and Debugging Programs
Jean-Philippe BernardyBernardy, Jean-Philippe University of Gothenburg, Sweden Committee Member in ICFP Programme Committee within the ICFP Papers-track
Quentin BernetBernet, Quentin EPFL Logically Qualified Types for Scala
Gilbert BernsteinBernstein, Gilbert University of WashingtonUnited States Committee Member in Program Committee within the SPLASH FARM-track Polynomial-Time Program Equivalence for Machine Knitting
Ivan BeschastnikhBeschastnikh, Ivan The University of British ColumbiaCanada TraceLinking Implementations with their Verified Designs
Raven BeutnerBeutner, Raven CISPA Helmholtz Center for Information Security, Germany Verifying Asynchronous Hyperproperties in Reactive Systems
Siddharth BhatBhat, Siddharth University of Cambridge Certified Decision Procedures for Width-Independent Bitvector Predicates Interactive Bit Vector Reasoning using Verified Bitblasting
Bishnu BhusalBhusal, Bishnu University of MissouriUnited States Checking $\delta$-Satisfiability of Reals with Integrals
Annette BieniusaBieniusa, Annette University of Kaiserslautern-LandauGermany PC Member in Program Committee within the SPLASH Onward! Essays-track
Baldip BijlaniBijlani, Baldip Indian Institute of Technology Kanpur Memory-Safety Verification of Open Programs With Angelic Assumptions
Vladyslav BilykBilyk, Vladyslav Semantics-preserving Transformation of Context-free Grammars into LL(1) Form
Walter BinderBinder, Walter USI LuganoSwitzerland 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 BirkedalBirkedal, Lars Aarhus UniversityDenmark Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs Reasoning about Weak Isolation Levels in Separation Logic
Stephen M. BlackburnBlackburn, Stephen M. Google; Australian National UniversityAustralia 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 BlackburnBlackburn, Steve Google and Australian National UniversityAustralia Session Chair of Abstraction (part of SPLASH OOPSLA)
Jasmin BlanchetteBlanchette, Jasmin Ludwig-Maximilians-Universität MünchenGermany Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Sandrine BlazyBlazy, Sandrine University of RennesFrance A Mechanized Semantics for Dataflow Circuits Committee Member in ICFP Programme Committee within the ICFP Papers-track
Kelly BlincoeBlincoe, Kelly University of AucklandNew Zealand PC Member in Program Committee within the SPLASH Onward! Essays-track
Andrew BlinnBlinn, Andrew University of MichiganUnited States Syntactic Completions with Material Obligations
Ivana BocevskaBocevska, Ivana TU Wien Divide and Conquer: A Compositional Approach to Game-Theoretic Security
Sean BocirneaBocirnea, Sean University of British Columbia Type-Preserving Flat Closure Optimization
Rastislav BodíkBodík, Rastislav Google Research, Brain TeamUnited States HieraSynth: A Parallel Framework for Complete Super-Optimization with Hierarchical Space Decomposition
Rose BohrerBohrer, Rose National Institute of Advanced Industrial Science and Technology (AIST), JapanJapan Committee Member in Program Committee within the SPLASH FARM-track
Giacomo BoldiniBoldini, Giacomo Ca' Foscari University of VeniceItaly Committee Member in SAS Artifact Evaluation Committee within the SAS Artifact-track
CF Bolz-TereickBolz-Tereick, CF Heinrich-Heine-Universität DüsseldorfGermany Tracing Just-in-time Compilation for Effects and Handlers
Michael D. BondBond, Michael D. Ohio State University Carapace: Static–Dynamic Information Flow Control in Rust
Daniele BonettaBonetta, Daniele VU AmsterdamNetherlands HeapBuffers: Why not just using a binary serialization format for your managed memory?
Tabea BordisBordis, Tabea Karlsruhe Institute of Technology X-by-Construction: Towards Ensuring Non-Functional Properties in by-Construction Engineering
Cândida BorgesBorges, Cândida Concert: The River Oycus
Nader Boushehrinejad MoradiBoushehrinejad Moradi, Nader University of UtahUnited States Translation Validation for LLVM's AArch64 Backend
Matt BovelBovel, Matt EPFLSwitzerland Existentialize your Generics
Matthieu BovelBovel, Matthieu EPFL Logically Qualified Types for Scala
Wavid BowmanBowman, Wavid University of FloridaUnited States Debugging WebAssembly? Put some Whamm on it!
William J. BowmanBowman, William J. University of British ColumbiaCanada 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äuserBrachthäuser, Jonathan Immanuel University of TübingenGermany 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 BradyBrady, Edwin University of St. AndrewsUnited Kingdom Frex: Dependently Typed Algebraic Simplification
Oliver BračevacBračevac, Oliver EPFL, LAMPSwitzerland 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 BreitnerBreitner, Joachim Lean FRO, LLCGermany Committee Member in ICFP Programme Committee within the ICFP Papers-track
Ana BrendelBrendel, Ana University of California Los AngelesUnited States Synthesizing Implication Lemmas for Interactive Theorem Proving
Mitch BrilesBriles, Mitch University of Utah Translation Validation for LLVM's AArch64 Backend
Matthew BrittonBritton, Matthew The Australian National University Verifying Extract Method Refactoring in Rust
Rutger BroekhoffBroekhoff, Rutger Radboud University NijmegenNetherlands Verified Interpreters for Dynamic Languages with Applications to the Nix Expression Language
Fraser BrownBrown, Fraser CMU Scaling Instruction-Selection Verification against Authoritative ISA Semantics
Roberto BruniBruni, Roberto University of PisaItaly Revealing Sources of (Memory) Errors via Backward Analysis Committee Member in Program Committee within the SAS -track
Anita BuckleyBuckley, Anita USI Lugano A Language for Quantifying Quantum Network Behavior
Humphrey BurchellBurchell, Humphrey University of KentUnited Kingdom Divining Profiler Accuracy: An Approach to Approximate Profiler Accuracy Through Machine Code-Level Slowdown
Roger BurtonpatelBurtonpatel, Roger University of PennsylvaniaUnited States Rocq N'Roll Concert: RocqNRoll
William E. ByrdByrd, William E. University of Alabama at BirminghamUnited States Committee Member in ICFP Programme Committee within the ICFP Papers-track
Aurea BíláBílá, Aurea ETH ZurichSwitzerland Place Capability Graphs: A General-Purpose Model of Rust’s Ownership and Borrowing Guarantees A Refinement Methodology for Distributed Programs in Rust
Henrik BövingBöving, Henrik Lean FRO Interactive Bit Vector Reasoning using Verified Bitblasting
C Joanna C. S. SantosC. S. Santos, Joanna University of Notre DameUnited States Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Cristian CadarCadar, Cristian Imperial College LondonUnited Kingdom P³: Reasoning about Patches via Product Programs
Jessica Belicia CahyonoCahyono, Jessica Belicia Institute of Science TokyoJapan Daisy: An Exercise Environment for Learning Information Modeling
Jose CalderonCalderon, Jose Galois, Inc.United States Exploring the Theory and Practice of Concurrency in the Entity-Component-System Pattern
José Pablo CambroneroCambronero, José Pablo Google, USAUnited States Committee Member in Review Committee within the SPLASH Student Research Competition-track
Marco CampionCampion, Marco INRIA & ENS Paris \| Université PSLFrance Relating Distances and Abstractions: An Abstract Interpretation Perspective
Paulo CanelasCanelas, Paulo Carnegie Mellon UniversityUnited States ROSpec: A Domain-Specific Language for ROS-based Robot Software
Man CaoCao, Man Google Advancing Performance via a Systematic Application of Research and Industrial Best Practice
Qinxiang CaoCao, Qinxiang Shanghai Jiao Tong UniversityChina Encode the $\forall\exists$ Relational Hoare Logic into Standard Hoare Logic
Cristina CarbunaruCarbunaru, Cristina National University of Singapore, SingaporeSingapore Evolving How We Teach Memory Models
Jacques CaretteCarette, Jacques McMaster UniversityCanada Committee Member in Program Committee within the SPLASH Onward! Papers-track
J. CarrCarr, J. University of ChicagoUnited States Environment-Sharing Analysis and Caller-Provided Environments for Higher-Order Languages
Chris CasinghinoCasinghino, Chris Jane Street A guided tour through Oxidized OCaml
Giuseppe CastagnaCastagna, Giuseppe CNRS; Université Paris CitéFrance Polymorphic Records for Dynamic Languages
Jonathan CastelloCastello, Jonathan University of California, Santa CruzUnited States Exploring the Theory and Practice of Concurrency in the Entity-Component-System Pattern CRDT Emulation, Simulation, and Representation Independence
Ethan CecchettiCecchetti, Ethan University of Wisconsin-MadisonUnited States Choreographic Quick Changes: First-Class Location (Set) Polymorphism
Sooyoung ChaCha, Sooyoung Sungkyunkwan University Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Elena ChachkarovaChachkarova, Elena Kings College London Shaking Up Quantum Simulators with Fuzzing and Rigour AccelerQ: Accelerating Quantum Eigensolvers With Machine Learning on Quantum Simulators
Rohit ChadhaChadha, Rohit University of Missouri Checking $\delta$-Satisfiability of Reals with Integrals
Kartik ChandraChandra, Kartik MITUnited 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 ChangChang, Bor-Yuh Evan University of Colorado Boulder & AmazonUnited 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 ChangChang, Rui Zhejiang University A complete formal semantics of eBPF instruction set architecture for Solana
Prantik ChatterjeeChatterjee, Prantik MathWorksIndia Memory-Safety Verification of Open Programs With Angelic Assumptions
Chong ChenChen, Chong Beijing Jiaotong University Fuzzing C++ Compilers via Type-Driven Mutation
Dong ChenChen, Dong Huawei Technologies Co., Ltd Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Fei ChenChen, Fei German Research Center for Artificial Intelligence (DFKI), Saarland UniversityGermany im2im: Automatically Converting In-Memory Image Representations using A Knowledge Graph Approach
Guanlin ChenChen, Guanlin Peking University Tunneling Through the Hill: Multi-Way Intersection for Version-Space Algebras in Program Synthesis
Hongbo ChenChen, Hongbo Indiana University Bloomington Agora: Trust Less and Open More in Verification for Confidential Computing
Hongzheng ChenChen, Hongzheng Cornell UniversityUnited States Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Jiasi ChenChen, Jiasi University of Michigan Hambazi: Spatial Coordination Synthesis for Augmented Reality
Jocelyn Qiaochu ChenChen, Jocelyn Qiaochu New York University, University of AlbertaUnited States Automated Discovery of Tactic Libraries for Interactive Theorem Proving Active Learning for Neurosymbolic Program Synthesis
Junjie ChenChen, Junjie Tianjin UniversityChina DESIL: Detecting Silent Bugs in MLIR Compiler Infrastructure Fuzzing C++ Compilers via Type-Driven Mutation
Liqian ChenChen, Liqian NUDTChina Committee Member in Program Committee within the SAS -track
Menglong ChenChen, Menglong Nanjing UniversityChina Committee Member in SAS Artifact Evaluation Committee within the SAS Artifact-track
Mingyi ChenChen, Mingyi University of California, Irvine Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Sen ChenChen, Sen Nankai UniversityChina Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Siyan ChenChen, 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 ChenChen, Tony MIT A Domain-Specific Probabilistic Programming Language for Reasoning about Reasoning (or: a memo on memo)
Weijun ChenChen, Weijun Shanghai Jiao Tong University, China A Programming Language for Feasible Solutions
Weiyi ChenChen, Weiyi Purdue University Probabilistic Inference for Datalog with Correlated Inputs
Xi ChenChen, 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 ChenChen, Yanju University of California, San DiegoUnited 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 ChenChen, Yanning University of Toronto Tabby: A Synthesis-Aided Compiler for High-Performance Zero-Knowledge Proof Circuits
Yitong ChenChen, 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 ChenChen, Zhenbang College of Computer, National University of Defense TechnologyChina Multi-Modal Sketch-based Behavior Tree Synthesis
Zhiyang ChenChen, Zhiyang University of TorontoCanada A Multi-Layer Dynamic Security Framework for DeFi Smart Contracts
Ellie Y. ChengCheng, Ellie Y. MITUnited States Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Feifei ChengCheng, Feifei Iowa State University Embedding Quantum Program Verification into Dafny
Luyu ChengCheng, Luyu Hong Kong University of Science and TechnologyHong Kong SAR China Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Ruotong ChengCheng, Ruotong University of TorontoCanada Products of Recursive Programs for Hypersafety Verification
Xiao ChengCheng, Xiao Macquarie UniversityAustralia Efficient Abstract Interpretation via Selective Widening SRC Judge & Co-Organizer in Competition Judges within the SPLASH Student Research Competition-track
Alvin CheungCheung, Alvin University of California at BerkeleyUnited States Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Tsung-Ju ChiangChiang, Tsung-Ju University of TorontoCanada Multi-stage Programming with Splice Variables
Michele ChiariChiari, Michele TU WienAustria Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Shigeru ChibaChiba, Shigeru The University of TokyoJapan 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
Zakaria ChihaniChihani, Zakaria CEA, LIST, France Verifying Neural Networks with PyRAT
Wei-Ngan ChinChin, Wei-Ngan National University of SingaporeSingapore Specifying and Verifying Future Conditions
Shardul ChiplunkarChiplunkar, Shardul EPFLSwitzerland Practical compositional diagramming
Adam ChlipalaChlipala, Adam Massachusetts Institute of TechnologyUnited States Session Chair of Reasoning (part of SPLASH OOPSLA)
Adam ChlipalaChlipala, Adam MIT CSAIL Pyrosome: Verified Compilation for Modular Metatheory
Minki ChoCho, Minki Seoul National UniversitySouth Korea Lilo: A Higher-Order, Relational Concurrent Separation Logic for Liveness
Minsung ChoCho, Minsung United States Scaling Optimization Over Uncertainty via Compilation
Joonwon ChoiChoi, Joonwon Amazon Web ServicesUnited States Revamping Verilog Semantics for Foundational Verification
Eloise ChristianChristian, Eloise Rochester Institute of TechnologyUnited States SIGPLAN AV Report
Ravi ChughChugh, Ravi University of Chicago Code Style Sheets: CSS for Code
Benjamin ChungChung, Benjamin JuliaHub Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Pavel ChuprikovChuprikov, Pavel Télécom Paris, Institut Polytechnique de Paris A Language for Quantifying Quantum Network Behavior
Luke ChurchChurch, Luke University of Cambridge \| Candela IncUnited Kingdom Committee Member in Program Committee within the SPLASH Onward! Papers-track
Luisa CicoliniCicolini, Luisa University of CambridgeUnited Kingdom Interactive Bit Vector Reasoning using Verified Bitblasting
Cristina CifuentesCifuentes, Cristina Oracle Software AssuranceAustralia PC Member in Program Committee within the SPLASH Onward! Essays-track
Berk CirisciCirisci, Berk Amazon Web Services UTFix: Change Aware Unit Test Repairing using LLM
Jürgen CitoCito, Jürgen TU WienAustria Static Inference of Regular Grammars for Ad Hoc Parsers
Peter ClarkClark, Peter None How to secure a distributed database such as OpenRiak with open-source tools
Christopher ClarkeClarke, Christopher University of Michigan MTP: A Meaning-Typed Language Abstraction for AI-Integrated Programming
Siobhán ClarkeClarke, Siobhán Trinity College Dublin, IrelandIreland Committee Member in Program Committee within the SPLASH Onward! Papers-track
Josh CluneClune, Josh Carnegie Mellon University Interactive Bit Vector Reasoning using Verified Bitblasting
Michael CoblenzCoblenz, Michael University of California, San DiegoUnited 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 CogumbreiroCogumbreiro, Tiago University of Massachusetts BostonUnited States Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Albert CohenCohen, Albert Google DeepMindFrance Mind the Abstraction Gap: Bringing Equality Saturation to Real-World ML Compilers
Cyril CohenCohen, Cyril Inria - CNRS - ENS Lyon - Université Claude Bernard Lyon 1 - LIP - UMR 5668France A Bargain for Mergesorts: How to Prove Your Mergesort Correct and Stable, Almost for Free
Sam CohenCohen, Sam University of Chicago Code Style Sheets: CSS for Code
Youyou CongCong, Youyou Institute of Science TokyoJapan 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 CookseyCooksey, Simon Symbolic MRD: Dynamic Memory, Undefined Behaviour, and Extrinsic Choice
Nathan CorbynCorbyn, Nathan University of OxfordUnited Kingdom Frex: Dependently Typed Algebraic Simplification
Lucas C. CordeiroCordeiro, Lucas C. University of Manchester, UKUnited Kingdom Committee Member in Program Committee within the SAS -track
Arthur CorrensonCorrenson, Arthur CISPA Helmholtz Center for Information SecurityGermany Almost Fair Simulations
Nicholas CoughlinCoughlin, Nicholas Defence Science and Technology Group, Australia Translation Validation for LLVM's AArch64 Backend
Aaron CouncilmanCouncilman, Aaron Univ of Illinois Urbana-Champaign FO-Complete Program Verification for Heap Logics
Patrick CousotCousot, Patrick Committee Member in Steering Committee within the SAS -track
Douglas A. CreagerCreager, Douglas A. AstralUnited States Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Will CrichtonCrichton, Will Brown UniversityUnited States A guided tour through Oxidized OCaml
Guofeng CuiCui, Guofeng Rutgers University Abstraction Refinement-guided Program Synthesis for Robot Learning from Demonstrations
Weidong CuiCui, Weidong Microsoft Research AutoVerus: Automated Proof Generation for Rust Code
D Marcelo d'Amorimd'Amorim, Marcelo North Carolina State UniversityUnited States Faster Explicit-Trace Monitoring-Oriented Programming for Runtime Verification of Software Tests
Loris D'AntoniD'Antoni, Loris University of California at San DiegoUnited 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. ChinD. Chin, Kyle An Exploration of How Generative AI Affects Workflow and Collaboration in a Software Engineering Course
Francesco DagninoDagnino, Francesco Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Joshua DahlDahl, 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 DahmenDahmen, 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 DaiDai, Jiarun Fudan UniversityChina ApkDiffer: Accurate and Scalable Cross-Version Diffing Analysis for Android Applications
Ting DaiDai, Ting IBM Research Artemis: Toward Accurate Detection of Server-Side Request Forgeries through LLM-Assisted Inter-Procedural Path-Sensitive Taint Analysis
Ugo Dal LagoDal Lago, Ugo University of Bologna & INRIA Sophia AntipolisItaly On Higher-Order Model Checking of Effectful Answer-Type-Polymorphic Programs Committee Member in ICFP Programme Committee within the ICFP Papers-track
Mila Dalla PredaDalla Preda, Mila University of VeronaItaly Committee Member in Program Committee within the SAS -track
Jayanaka DantanarayanaDantanarayana, Jayanaka University of Michigan MTP: A Meaning-Typed Language Abstraction for AI-Integrated Programming
Olivier DanvyDanvy, Olivier National University of SingaporeSingapore How Computer Science Was Introduced at Yale-NUS College
Olivier DanvyDanvy, Olivier Yale-NUS College and School of Computing, SingaporeSingapore Session Chair of Verification (part of SAS ) On a simple problem due to Yves Bertot
David DaraisDarais, David GaloisUnited States Committee Member in ICFP Programme Committee within the ICFP Papers-track
Anupam DasDas, Anupam University of Birmingham, UKUnited Kingdom Committee Member in ICFP Programme Committee within the ICFP Papers-track
Dylan DavisDavis, Dylan Swinburne University I Am Your Co-Pilot
Charles de Harode Haro, Charles École Normale Supérieure \| Université PSLFrance Committee Member in SAS Artifact Evaluation Committee within the SAS Artifact-track
Markus de Medeirosde Medeiros, Markus New York UniversityUnited States Place Capability Graphs: A General-Purpose Model of Rust’s Ownership and Borrowing Guarantees
Wolfgang De MeuterDe Meuter, Wolfgang Vrije Universiteit BrusselBelgium 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 RooverDe Roover, Coen Vrije Universiteit BrusselBelgium 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 DeedsDeeds, Kyle University of Washington Finch: Sparse and Structured Tensor Programming with Control Flow
Maryam Mehri DehnaviDehnavi, Maryam Mehri University of TorontoCanada Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Benjamin DelawareDelaware, Benjamin Purdue UniversityUnited States We’ve Got You Covered: Type-Guided Repair of Incomplete Input Generators KestRel: Relational Verification Using E-Graphs for Program Alignment
Delphine DemangeDemange, Delphine Univ Rennes, Inria, CNRS, IRISAFrance A Mechanized Semantics for Dataflow Circuits
Brian DemskyDemsky, Brian University of California at Irvine Towards Verifying Crash Consistency
Haotian DengDeng, Haotian Purdue University Complete the Cycle: Reachability Types with Expressive Cyclic References
Ming DengDeng, Ming Beijing Jiaotong University Fuzzing C++ Compilers via Type-Driven Mutation
Anoop DeorasDeoras, Anoop AWS AI Labs UTFix: Change Aware Unit Test Repairing using LLM
Farzaneh DerakhshanDerakhshan, Farzaneh Illinois Institute of TechnologyUnited States Quantified Underapproximation via Labeled Bunches Committee Member in ICFP Programme Committee within the ICFP Papers-track
Ankush DesaiDesai, Ankush Amazon Web ServicesUnited States Checking Observational Correctness of Database Systems
Dominique DevrieseDevriese, Dominique KU LeuvenBelgium 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 DharanikotaDharanikota, Samvid Efficient ComputerUnited States Fray: An Efficient General-Purpose Concurrency Testing Platform for the JVM
Tomás DiazDiaz, Tomás University of ChileChile Flexible and Expressive Typed Path Patterns for GQL Incremental Certified Programming
Robert DickersonDickerson, Robert Purdue UniversityUnited States KestRel: Relational Verification Using E-Graphs for Program Alignment
Işıl DilligDillig, Işıl University of Texas at AustinUnited 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 DimitrovDimitrov, Dimitar INSAIT, Sofia University "St. Kliment Ohridski"Bulgaria qblaze: An Efficient and Scalable Sparse Quantum Simulator
Christos DimoulasDimoulas, Christos Northwestern UniversityUnited States Contract System Metatheories à 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 DingDing, Shuo Georgia Institute of TechnologyChina Fast Constraint Synthesis for C++ Function Templates
Alexander DingesDinges, Alexander RPTU Kaiserslautern-LandauGermany Truly Functional Solutions to the Longest Uptrend Problem (Functional Pearl)
Chandeepa DissanayakeDissanayake, Chandeepa Iowa State UniversityUnited States A Haskell Adiabatic DSL: Solving Classical Optimization Problems on Quantum Hardware
Stephen DolanDolan, Stephen Jane StreetUnited Kingdom Modal Effect Types
Jin Song DongDong, Jin Song National University of SingaporeSingapore Verification of Bit-Flip Attacks against Quantized Neural Networks
Rui DongDong, Rui University of MichiganUnited 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 CohenDrachsler Cohen, Dana TechnionIsrael 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 DraperDraper, Steve University of Glasgow Let's Take Esoteric Programming Languages Seriously
Alexandre DreweryDrewery, Alexandre INRIA Contextual Equality Saturation
Derek DreyerDreyer, Derek MPI-SWSGermany JFP Announcement
Sophia DrossopoulouDrossopoulou, Sophia Imperial College LondonUnited Kingdom Reasoning about External Calls
Cezara DrăgoiDrăgoi, Cezara AWS / ENS Committee Member in Steering Committee within the SAS -track
Xuan Du TrinhDu Trinh, Xuan Stony Brook UniversityUnited States Scalable Equivalence Checking and Verification of Shallow Quantum Circuits
Xiaoning DuDu, Xiaoning Monash UniversityAustralia Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Yuanlin DuanDuan, Yuanlin Rutgers University Abstraction Refinement-guided Program Synthesis for Robot Learning from Demonstrations
Christophe DubachDubach, Christophe McGill UniversityCanada Sound and Modular Activity Analysis for Automatic Differentiation in MLIR
Stéphane DucasseDucasse, Stéphane Inria; University of Lille; CNRS; Centrale Lille; CRIStALFrance Committee Member in Program Committee within the SPLASH Onward! Papers-track
Gregory J. DuckDuck, Gregory J. National University of SingaporeSingapore Large Language Model powered Symbolic Execution
Léon DucruetDucruet, Léon Aarhus UniversityDenmark Reasoning about Weak Isolation Levels in Separation Logic
Arpita DuttaDutta, Arpita National University of SingaporeSingapore Incremental and Unbounded Loop Analysis
Saikat DuttaDutta, Saikat Cornell UniversityUnited States Understanding and Improving Flaky Test Classification
Saikat DuttaDutta, Saikat University of Illinois at Urbana-ChampaignUnited States Precise Abstract Interpretation of Probabilistic Programs with Interval Data Uncertainty
E Harley D. Eades IIIEades III, Harley D. Augusta UniversityUnited States Committee Member in ICFP Programme Committee within the ICFP Papers-track
Jonathan EdwardsEdwards, Jonathan IndependentUnited 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 EilersEilers, Marco ETH ZurichSwitzerland Modular Reasoning about Global Variables and Their Initialization
Susan EisenbachEisenbach, Susan Imperial College LondonUnited Kingdom Reasoning about External Calls
Richard A. EisenbergEisenberg, Richard A. Jane StreetUnited 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 ElsmanElsman, Martin University of CopenhagenDenmark Session Chair of Applications and SRC Talks (part of ICFP Papers)
Joel S EmerEmer, Joel S MIT/NVIDIAUnited States The Continuous Tensor Abstraction: Where Indices are Real
Madeline EndresEndres, Madeline University of Massachusetts AmherstUnited States PC Member in Program Committee within the SPLASH Onward! Essays-track
Constantin EneaEnea, Constantin LIX, CNRS, Ecole Polytechnique Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Sebastian ErdwegErdweg, Sebastian JGU MainzGermany Associate Chair in OOPSLA Review Committee within the SPLASH OOPSLA-track
Guilherme EspadaEspada, Guilherme LASIGE, University of LisbonPortugal SIGPLAN AV Report
Patrick EugsterEugster, Patrick USI Lugano, SwitzerlandSwitzerland A Language for Quantifying Quantum Network Behavior
Tae Eun KimEun Kim, Tae KAISTSouth Korea Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Karine Even-MendozaEven-Mendoza, Karine King’s College LondonUnited 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
F Teodoro F. CollinF. Collin, Teodoro MIT CSAIL Finch: Sparse and Structured Tensor Programming with Control Flow The Continuous Tensor Abstraction: Where Indices are Real
Luis F. GomesF. Gomes, Luis Carnegie Mellon UniversityPortugal Student Volunteer Co-Chair in Organizing Committee for SPLASH 2025
Chris FallinFallin, Chris F5United States Scaling Instruction-Selection Verification against Authoritative ISA Semantics
Max FanFan, Max Cornell University Proof Repair across Quotient Type Equivalences
Le FangFang, Le Purdue University Show Me Why It's Correct: Saving 1/3 of Debugging Time in Program Repair with Interactive Runtime Comparison
Ruijie FangFang, Ruijie University of Texas at AustinUnited States Software Model Checking via Summary-Guided Search Homomorphism Calculus for User-Defined Aggregations
Umar FarooqFarooq, Umar Louisiana State UniversityUnited States Publicity Co-Chair, Web Co-Chair in Organizing Committee for SPLASH 2025
Azadeh FarzanFarzan, Azadeh University of TorontoCanada Products of Recursive Programs for Hypersafety Verification
Andrew FawcettFawcett, Andrew Victoria University of WellingtonNew Zealand Exploring The Design Space For Runtime Enforcement of Dynamic Capabilities
Aleksandr FedchinFedchin, Aleksandr Tufts UniversityUnited States Metamorph: Synthesizing Large Objects from Dafny Specifications
Grigory FedyukovichFedyukovich, Grigory Florida State UniversityUnited States A Flow-Sensitive Refinement Type System for Verifying eBPF Programs
Marc FeeleyFeeley, Marc Université de MontréalCanada Float Self-Tagging
Joan FeigenbaumFeigenbaum, Joan Yale On Collective Control over User Interfaces in the Face of Network Eﬀects
Qiong FengFeng, Qiong Nanjing University of Science and TechnologyChina Finding Compiler Bugs through Cross-Language Code Generator and Differential Testing
Yang FengFeng, Yang Nanjing UniversityChina An Empirical Study of Bugs in the rustc Compiler
Yao FengFeng, Yao Tsinghua University Adaptive Shielding via Parametric Safety Proofs
Yu FengFeng, Yu University of California at Santa BarbaraUnited States Tabby: A Synthesis-Aided Compiler for High-Performance Zero-Knowledge Proof Circuits
Ziyuan FengFeng, Ziyuan Nanjing University of Science and Technology Finding Compiler Bugs through Cross-Language Code Generator and Differential Testing
Pietro FerraraFerrara, Pietro Ca’ Foscari University of VeniceItaly Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Patrick FerrisFerris, Patrick University of Cambridge, UKUnited Kingdom Functional Networking for Millions of Docker Desktops (Experience Report)
Jack FeserFeser, Jack BasisUnited States Peepco: Batch-Based Consistency Optimization
Jonas FialaFiala, Jonas ETH Zürich Place Capability Graphs: A General-Purpose Model of Rust’s Ownership and Borrowing Guarantees
David Anthony K. FieldsFields, David Anthony K. Seton Hall University Automata Visualization for Validation and Verification: Helping Develop Correctness Arguments for Nondeterministic Machines
Andrzej FilinskiFilinski, Andrzej DIKU, University of Copenhagen Committee Member in ICFP Programme Committee within the ICFP Papers-track
Robert Bruce FindlerFindler, Robert Bruce Northwestern UniversityUnited States Contract System Metatheories à la Carte: A Transition-System View of Contracts Metaprogramming in Rhombus Committee Member in ICFP Programme Committee within the ICFP Papers-track
Bernd FinkbeinerFinkbeiner, Bernd CISPA Helmholtz Center for Information SecurityGermany Verifying Asynchronous Hyperproperties in Reactive Systems Almost Fair Simulations
Patricia FirlejczykFirlejczyk, Patricia ETH ZurichSwitzerland Modular Reasoning about Global Variables and Their Initialization
Emily FirstFirst, Emily University of California, San DiegoUnited States Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Kathi FislerFisler, Kathi Brown UniversityUnited States Sharing is Scaring: Linking Cloud File-Sharing to Programming Language Semantics
Matthew FlattFlatt, Matthew University of UtahUnited States Session Chair of Systems (part of SPLASH OOPSLA) Metaprogramming in Rhombus
Krisztian FlautnerFlautner, Krisztian University of Michigan MTP: A Meaning-Typed Language Abstraction for AI-Integrated Programming
Cyril Flurin MoserFlurin Moser, Cyril ETH Zurich Validating Soundness and Completeness in Pattern-Match Coverage Analyzers
Alcides FonsecaFonseca, Alcides LASIGE; University of LisbonPortugal ROSpec: A Domain-Specific Language for ROS-based Robot Software
Darius FooFoo, Darius National University of Singapore Specifying and Verifying Future Conditions
Sophie FortzFortz, Sophie King's College LondonUnited Kingdom Shaking Up Quantum Simulators with Fuzzing and Rigour AccelerQ: Accelerating Quantum Eigensolvers With Machine Learning on Quantum Simulators
Jeffrey S. FosterFoster, Jeffrey S. Tufts UniversityUnited 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 FosterFoster, Nate Cornell University; Jane StreetUnited States Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Adrian FrancalanzaFrancalanza, Adrian University of MaltaMalta Correct Black-Box Monitors for Distributed Deadlock Detection: Formalisation and Implementation
Michael FranzFranz, Michael University of California, IrvineUnited States Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Leon FrenotFrenot, Leon ENS Lyon Interactive Bit Vector Reasoning using Verified Bitblasting
Marco FrigoFrigo, Marco University of Illinois at Urbana-Champaign End-to-End Compiler Infrastructure for Emerging Tensor Accelerators
Thomas FritzFritz, Thomas University of ZurichSwitzerland An Exploration of How Generative AI Affects Workflow and Collaboration in a Software Engineering Course
Daniel FruminFrumin, Daniel University of GroningenNetherlands Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Hongfei FuFu, Hongfei Shanghai Jiao Tong UniversityChina Structural Abstraction and Refinement for Probabilistic Programs
Yuxi FuFu, Yuxi Shanghai Jiao Tong University, China A Programming Language for Feasible Solutions
G Marcial GaißertGaißert, Marcial University of TübingenGermany Tracing Just-in-time Compilation for Effects and Handlers
Pierre GantyGanty, Pierre IMDEA Software Institute, Spain Committee Member in Program Committee within the SAS -track
Cunyuan GaoGao, Cunyuan HKUST A Lightweight Type-and-Effect System for Invalidation Safety: Tracking Permanent and Temporary Invalidation With Constraint-Based Subtype Inference
Miao GaoGao, 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 GaoGao, Pengfei ByteDance Verification of Bit-Flip Attacks against Quantized Neural Networks
Yanfeng GaoGao, Yanfeng Nanjing University HybridPersist: A Compiler Support for User-Friendly and Efficient PM Programming
Zhiqiang GaoGao, 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. GarcedGarced, Andrés M. Seton Hall University Derivation Visualization for Context-Free Grammar Design: Helping Students Understand Context-Free Grammars
Ronald GarciaGarcia, Ronald University of British ColumbiaCanada Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Philippa GardnerGardner, Philippa Imperial College LondonUnited Kingdom Compositional Symbolic Execution for the Next 700 Memory Models
Deepak GargGarg, Deepak MPI-SWSGermany 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 GargGarg, Harshit Northeastern University - Khoury College of Computer SciencesUnited States Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Poorva GargGarg, Poorva University of California, Los AngelesIndia Tuning Random Generators: Property-Based Testing as Probabilistic Programming
Pranav GargGarg, Pranav AWSUnited States UTFix: Change Aware Unit Test Repairing using LLM
Antoine GaulinGaulin, Antoine McGill UniversityCanada McTT: A Verified Kernel for a Proof Assistant
François GauthierGauthier, François Oracle LabsAustralia Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Thomas GazagnaireGazagnaire, Thomas TaridesFrance Functional Networking for Millions of Docker Desktops (Experience Report)
Yuhao GeGe, Yuhao University of Illinois at Urbana-Champaign SPLAT: A framework for optimised GPU code-generation for SParse reguLar ATtention
Zhaoyi GeGe, Zhaoyi University of WaterlooCanada Zero-Overhead Lexical Effect Handlers
Jasper GeerGeer, Jasper University of British ColumbiaCanada Place Capability Graphs: A General-Purpose Model of Rust’s Ownership and Borrowing Guarantees
Timon GehrGehr, Timon ETH ZurichSwitzerland qblaze: An Efficient and Scalable Sparse Quantum Simulator
Adam GellerGeller, Adam Computer Science, University of British ColumbiaCanada Type-Preserving Flat Closure Optimization
Samir GenaimGenaim, Samir Universidad Complutense de MadridSpain Committee Member in Program Committee within the SAS -track
Jared GentnerGentner, Jared None How to Score in the Art Racket
Aina Linn GeorgesGeorges, Aina Linn Max Planck Institute for Software Systems (MPI-SWS) Committee Member in ICFP Programme Committee within the ICFP Papers-track
Kimball GermaneGermane, Kimball Brigham Young UniversityUnited States Session Chair of Algorithms (part of ICFP Papers) Call-Guarded Abstract Definitional Interpreters
Dan GhicaGhica, Dan Huawei Research and University of BirminghamUnited Kingdom Committee Member in ICFP Programme Committee within the ICFP Papers-track
Mahdi GhorbaniGhorbani, Mahdi University of EdinburghUnited Kingdom Compressed and Parallelized Structured Tensor Algebra
Roberto GiacobazziGiacobazzi, Roberto University of ArizonaUnited States Committee Member in Steering Committee within the SAS -track
Ryan GibbGibb, Ryan University of Cambridge Functional Networking for Millions of Docker Desktops (Experience Report)
Olek GierczakGierczak, Olek Northeastern University From Linearity to Borrowing
Elizabeth GilbertGilbert, Elizabeth Carnegie Mellon University Debugging WebAssembly? Put some Whamm on it!
Elena GlassmanGlassman, Elena Harvard UniversityUnited States PC Member in Program Committee within the SPLASH Onward! Essays-track
Nathan GloverGlover, Nathan Carnegie Mellon University Integrating Resource Analyses via Resource Decomposition
Brighten GodfreyGodfrey, Brighten UIUC and Broadcom SafeTree: Expressive Tree Policies for Microservices
Harrison GoldsteinGoldstein, Harrison University at Buffalo, the State University of New York at BuffaloUnited States Tuning Random Generators: Property-Based Testing as Probabilistic Programming QED in Context: An Observation Study of Proof Assistant Users
Sergey GoncharovGoncharov, Sergey University of BirminghamUnited Kingdom Bialgebraic Reasoning on Stateful Languages Big Steps in Higher-Order Mathematical Operational Semantics
Léon GondelmanGondelman, Léon Aalborg UniversityDenmark Reasoning about Weak Isolation Levels in Separation Logic
Yeyun GongGong, Yeyun Microsoft Research AutoVerus: Automated Proof Generation for Rust Code
Elisa Gonzalez BoixGonzalez Boix, Elisa Vrije Universiteit BrusselBelgium Committee Member in Program Committee within the SPLASH Onward! Papers-track
Noah D. GoodmanGoodman, Noah D. Stanford University Automated Discovery of Tactic Libraries for Interactive Theorem Proving
Kiran GopinathanGopinathan, Kiran University of Illinois Urbana ChampaignUnited States Committee Member in ICFP Programme Committee within the ICFP Papers-track
Colin GordonGordon, Colin Drexel UniversityUnited 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 GoriGori, Roberta Diaprtimento di Informatica, Universita' di Pisa, Italy Revealing Sources of (Memory) Errors via Backward Analysis
Alessandra GorlaGorla, Alessandra IMDEA Software InstituteSpain Committee Member in Steering Committee within the SAS -track
Chester GouldGould, Chester University of British Columbia Type-Preserving Flat Closure Optimization
Hemant GouniGouni, Hemant Carnegie Mellon UniversityUnited States Structural Information Flow: A Fresh Look at Types for Non-Interference
Pierre GoutagnyGoutagny, Pierre Inria and University of LilleFrance Committee Member in SAS Artifact Evaluation Committee within the SAS Artifact-track
John GouwarGouwar, John Northeastern UniversityUnited States Scaling Optimization Over Uncertainty via Compilation
Kevin GraafGraaf, Kevin Independent Researcher Carving Text at Its Joints: A New Perspective on Writing and Computers
Marcos GranduryGrandury, Marcos IMDEA Software Institute; Universidad Politécnica de MadridSpain Verifying Graph Algorithms in Separation Logic: A Case for an Algebraic Approach
Zachary GrannanGrannan, Zachary University of British ColumbiaCanada Place Capability Graphs: A General-Purpose Model of Rust’s Ownership and Borrowing Guarantees
Daniel GratzerGratzer, Daniel Aarhus UniversityDenmark Committee Member in ICFP Programme Committee within the ICFP Papers-track
Eva GraversenGraversen, Eva University of Southern Denmark Committee Member in ICFP Programme Committee within the ICFP Papers-track
James Bryan GravesGraves, James Bryan Indiana University A Haskell Adiabatic DSL: Solving Classical Optimization Problems on Quantum Hardware
Gavin GrayGray, Gavin Brown UniversityUnited States A guided tour through Oxidized OCaml
Neville GrechGrech, Neville Dedaub LimitedMalta Universal Scalability in Declarative Program Analysis (with Choice-Based Combination Pruning)
Michael GreenbergGreenberg, Michael Stevens Institute of TechnologyUnited States Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Ben GreenmanGreenman, Ben University of UtahUnited States Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Ben GreenmanGreenman, Ben University of Utah, USA Workshops Co-Chair in Workshop Selection Committee within the ICFP/SPLASH Workshops-track
Simon Oddershede GregersenGregersen, Simon Oddershede New York UniversityUnited States Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs
Karuna GrewalGrewal, Karuna Cornell University SafeTree: Expressive Tree Policies for Microservices
Tobias GrosserGrosser, Tobias University of CambridgeUnited Kingdom Certified Decision Procedures for Width-Independent Bitvector Predicates Interactive Bit Vector Reasoning using Verified Bitblasting Compressed and Parallelized Structured Tensor Algebra
Alexander GryzlovGryzlov, Alexander IMDEA Software InstituteSpain Verifying Graph Algorithms in Separation Logic: A Case for an Algebraic Approach
Dawu GuGu, Dawu Shanghai Jiao Tong University Binary Cryptographic Function Identification via Similarity Analysis with Path-insensitive Emulation
Yile GuGu, Yile University of Washington Scalable and Accurate Application-level Crash-Consistency Testing via Representative Testing
Hanqin GuanGuan, Hanqin Peking University Orax: A Feedback-Driven Framework for Efficiently Solving Satisfiability Modulo Theories and Oracles
Kevin GuanGuan, Kevin Cornell UniversityUnited States Faster Explicit-Trace Monitoring-Oriented Programming for Runtime Verification of Software Tests
Ege Berkay GulcanGulcan, Ege Berkay Delft University of TechnologyNetherlands Model-guided Fuzzing of Distributed Systems
Ahan GuptaGupta, Ahan University of Illinois at Urbana-Champaign SPLAT: A framework for optimised GPU code-generation for SParse reguLar ATtention
Arie GurfinkelGurfinkel, Arie University of WaterlooCanada A Flow-Sensitive Refinement Type System for Verifying eBPF Programs
Sankha Narayan GuriaGuria, Sankha Narayan University of KansasUnited 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 GutierrezGutierrez, Claudio DCC, Universidad de Chile & IMFD Flexible and Expressive Typed Path Patterns for GQL
H Huong HaHa, Huong RMIT UniversityAustralia Committee Member in Review Committee within the SPLASH Student Research Competition-track
Andrew HabibHabib, Andrew ABB Corporate Research, GermanyGermany Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Sebastian HackHack, Sebastian Saarland University, Saarland Informatics CampusGermany Non-interference Preserving Optimising Compilation
Finn HackettHackett, Finn University of British ColumbiaCanada TraceLinking Implementations with their Verified Designs
Kerry HaganHagan, Kerry University of Illinois, Urbana-ChampaignUnited States Cellular Automata as a Model For 1-bit Synthesis in Mitosis Concert: Mitosis
Matthew HagueHague, Matthew Royal Holloway University of LondonUnited Kingdom The Power of Regular Constraint Propagation
Shashin HalalingaiahHalalingaiah, Shashin UT Austin, IIT MadrasUnited States Probabilistic Inference for Datalog with Correlated Inputs
William HallahanHallahan, William Binghamton Counterexample-Guided Inference of Modular Specifications
Philipp HallerHaller, Philipp KTH Royal Institute of TechnologySweden Committee Member in Program Committee within the SPLASH Onward! Papers-track
Sara S. HamoudaHamouda, Sara S. Canva Advancing Performance via a Systematic Application of Research and Industrial Best Practice
Ameer HamzaHamza, Ameer Florida State UniversityUnited States A Flow-Sensitive Refinement Type System for Verifying eBPF Programs
Xing HanHan, Xing The Hong Kong University of Science and Technology Agora: Trust Less and Open More in Verification for Confidential Computing
Zhilei HanHan, Zhilei Tsinghua University Structural Abstraction and Refinement for Probabilistic Programs
Dan HaoHao, Dan Peking UniversityChina Fuzzing C++ Compilers via Type-Driven Mutation
Ben HardekopfHardekopf, Ben University of California at Santa BarbaraUnited States Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Adi HarifHarif, 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, RenoUnited States An Argument for the Practicality of Entity Component Systems as the Primary Data Structure for an Interpreter or Compiler
Philipp G. HaselwarterHaselwarter, Philipp G. Aarhus UniversityDenmark Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs
Zara HassanHassan, Zara Australian National UniversityAustralia Reproducibility Debt in Scientific Software
Ichiro HasuoHasuo, Ichiro National Institute of Informatics, JapanJapan A Unifying Approach to Product Constructions for Quantitative Temporal Inference
Matthias HauswirthHauswirth, Matthias USI LuganoSwitzerland Associate Chair in OOPSLA Review Committee within the SPLASH OOPSLA-track
Chris HawblitzelHawblitzel, Chris Microsoft ResearchUnited States AutoVerus: Automated Proof Generation for Rust Code
Musa HaydarHaydar, Musa University of Michigan Scalable and Accurate Application-level Crash-Consistency Testing via Representative Testing
Dongjie HeHe, Dongjie Chongqing University, ChinaChina Fast Client-Driven CFL-Reachability via Regularization-Based Graph Simplification
Fei HeHe, Fei Tsinghua UniversityChina Structural Abstraction and Refinement for Probabilistic Programs
Jingzhu HeHe, Jingzhu ShanghaiTech UniversityChina Artemis: Toward Accurate Detection of Server-Side Request Forgeries through LLM-Assisted Inter-Procedural Path-Sensitive Taint Analysis
Ningyu HeHe, Ningyu Hong Kong Polytechnic UniversityHong Kong SAR China Committee Member in Program Committee within the SAS -track
Pinjia HeHe, Pinjia Chinese University of Hong Kong, ShenzhenChina Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Siyuan HeHe, 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 HeHe, Wenyu Shanghai Jiao Tong University Binary Cryptographic Function Identification via Similarity Analysis with Path-insensitive Emulation
Yituo HeHe, Yituo Shanghai Jiao Tong University Binary Cryptographic Function Identification via Similarity Analysis with Path-insensitive Emulation
Yumeng HeHe, Yumeng University of Utah Formalizing Linear Motion G-code for Invariant Checking and Differential Testing of Fabrication Tools
Andrew HeadHead, Andrew University of Pennsylvania QED in Context: An Observation Study of Proof Assistant Users
Fritz HengleinHenglein, Fritz University of CopenhagenDenmark Committee Member in ICFP Programme Committee within the ICFP Papers-track
Troels HenriksenHenriksen, Troels University of CopenhagenDenmark Correctness Meets Performance: From Agda to Futhark
Martin HenzHenz, Martin National University of SingaporeSingapore SPLASH-E Co-Chair in Organizing Committee for SPLASH 2025 SPLASH-E Co-Chair in Program Commitee within the SPLASH -E-track
Kihong HeoHeo, Kihong KAISTSouth Korea Co-chair in SAS Artifact Evaluation Committee within the SAS Artifact-track
Felienne HermansHermans, Felienne Vrije Universiteit AmsterdamNetherlands SPLASH-E Co-Chair in Organizing Committee for SPLASH 2025 SPLASH-E Co-Chair in Program Commitee within the SPLASH -E-track
Manuel HermenegildoHermenegildo, Manuel Technical University of Madrid (UPM) and IMDEA Software InstituteSpain Committee Member in Steering Committee within the SAS -track
Daniel HillerströmHillerström, Daniel Category Labs and The University of EdinburghUnited Kingdom Modal Effect Types
Ralf HinzeHinze, Ralf RPTU Kaiserslautern-Landau Truly Functional Solutions to the Longest Uptrend Problem (Functional Pearl)
Andrew K. HirschHirsch, Andrew K. University at Buffalo, SUNYUnited States Choreographic Quick Changes: First-Class Location (Set) Polymorphism Session Chair of Concurrency (part of ICFP Papers)
Robert HirschfeldHirschfeld, Robert Hasso Plattner Institute; University of PotsdamGermany 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 HirzelHirzel, Martin IBM ResearchUnited States Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Son HoHo, Son InriaFrance Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Jan HoffmannHoffmann, Jan Carnegie Mellon UniversityUnited States Integrating Resource Analyses via Resource Decomposition Committee Member in ICFP Programme Committee within the ICFP Papers-track
Reid HolmesHolmes, Reid University of British ColumbiaCanada 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 HoltzenHoltzen, Steven Northeastern UniversityUnited States Multi-Language Probabilistic Programming Scaling Optimization Over Uncertainty via Compilation
Michael HomerHomer, Michael Victoria University of WellingtonNew Zealand Exploring The Design Space For Runtime Enforcement of Dynamic Capabilities
Changwan HongHong, Changwan Massachusetts Institute of Technology Finch: Sparse and Structured Tensor Programming with Control Flow
Weijiang HongHong, Weijiang National University of Defense Technology, Changsha, China Multi-Modal Sketch-based Behavior Tree Synthesis
Manoel Horta RibeiroHorta Ribeiro, Manoel Interactive Theorem Provers for Proof Education
Tony HoskingHosking, Tony Australian National UniversityAustralia Session Chair of Parallelism (part of SPLASH OOPSLA)
Cătălin HriţcuHriţcu, Cătălin MPI-SPGermany SecRef: Securely Sharing Mutable References between Verified and Unverified Code in F Committee Member in ICFP Programme Committee within the ICFP Papers-track
Justin HsuHsu, Justin Cornell UniversityUnited States SafeTree: Expressive Tree Policies for Microservices A Hoare Logic For Symmetry Properties
Guangyu HuHu, 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. HuHu, Jason Z. S. AmazonUnited States Normalization by Evaluation for Non-cumulativity McTT: A Verified Kernel for a Proof Assistant
Jingmei HuHu, Jingmei Amazon Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Yikun HuHu, Yikun Shanghai Jiao Tong UniversityChina Binary Cryptographic Function Identification via Similarity Analysis with Path-insensitive Emulation
Zhenjiang HuHu, Zhenjiang Peking UniversityChina Associate Chair in OOPSLA Review Committee within the SPLASH OOPSLA-track Effectful Lenses: There and Back with Different Monads
Heqing HuangHuang, Heqing City University of Hong Kong Publicity Co-Chair, Web Co-Chair in Organizing Committee for SPLASH 2025
Jeff HuangHuang, Jeff Texas A&M UniversityUnited 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 HuangHuang, Lei ShanghaiTech University Verification of Bit-Flip Attacks against Quantized Neural Networks
Tianshu HuangHuang, Tianshu Carnegie Mellon University Unveiling Heisenbugs with Diversified Execution
Xuejing HuangHuang, Xuejing IRIFFrance (TOPLAS) Type-Safe Compilation of Dynamic Inheritance via Merging Liberating Merges via Apartness and Guarded Subtyping
Zixin HuangHuang, Zixin University of Illinois at Urbana-Champaign, USA Precise Abstract Interpretation of Probabilistic Programs with Interval Data Uncertainty
Jan HueckelheimHueckelheim, Jan Argonne National Laboratory Synthesizing Sound and Precise Abstract Transformers for Nonlinear Hyperbolic PDE Solvers
Chris HughesHughes, Chris Independent Researcher Certified Decision Procedures for Width-Independent Bitvector Predicates
Jacob HughesHughes, Jacob King's College LondonUnited Kingdom Garbage Collection for Rust: The Finalizer Frontier
Chung-Kil HurHur, Chung-Kil Seoul National UniversitySouth Korea Lilo: A Higher-Order, Relational Concurrent Separation Logic for Liveness
Nathan HurtigHurtig, Nathan University of WashingtonUnited States Polynomial-Time Program Equivalence for Machine Knitting
Doha HwangHwang, Doha Samsung PAFL: Enhancing Fault Localizers by Leveraging Project-Specific Fault Patterns
I Ruxandra IcleanuIcleanu, Ruxandra University of Edinburgh SecRef: Securely Sharing Mutable References between Verified and Unverified Code in F
Yuka IkarashiIkarashi, Yuka Massachusetts Institute of TechnologyUnited States Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Kazuki IkemoriIkemori, Kazuki Tokyo Institute of Technology Continuations for All: Language Design Considerations for Accessible Continuations
Lef IoannidisIoannidis, Lef University of PennsylvaniaUnited States Structural temporal logic for mechanized program verification
Anastasia IsychevIsychev, Anastasia TU WienAustria Cost of Soundness in Mixed-Precision Tuning
Shachar ItzhakyItzhaky, Shachar TechnionIsrael Ductape: Optimizing Dynamically Typed Programs using Ahead-of-Time Compilation and Data-Flow Analysis
J Daniel JacksonJackson, Daniel MIT What You See Is What It Does: A Structural Pattern for Legible Software
Jules JacobsJacobs, Jules Cornell UniversityUnited States Committee Member in ICFP Programme Committee within the ICFP Papers-track
Koen JacobsJacobs, Koen InriaFrance Robust Dynamic Embedding for Gradual Typing
Seyed Mohammad Reza JafariJafari, Seyed Mohammad Reza Iowa State University Embedding Quantum Program Verification into Dafny
Joxan JaffarJaffar, Joxan National University of SingaporeSingapore Incremental and Unbounded Loop Analysis
Suresh JagannathanJagannathan, Suresh Purdue UniversityUnited States We’ve Got You Covered: Type-Guided Repair of Incomplete Input Generators
Devansh JainJain, 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 JakubovicJakubovic, Joel Charles University in PragueCzechia The Unix Executable as a Smalltalk Method Committee Member in Program Committee within the SPLASH Onward! Papers-track
Vincent James BeardsleyJames Beardsley, Vincent Carapace: Static–Dynamic Information Flow Control in Rust
Dustin JamnerJamner, Dustin MIT CSAIL, USA Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Dustin JamnerJamner, Dustin MIT CSAIL Pyrosome: Verified Compilation for Modular Metatheory
Junyoung JangJang, Junyoung McGill UniversityCanada McTT: A Verified Kernel for a Proof Assistant
Sujin JangJang, Sujin KAISTSouth Korea Committee Member in SAS Artifact Evaluation Committee within the SAS Artifact-track
Nikhil JayakumarJayakumar, Nikhil University of Texas at Austin GALA: A High Performance Graph Neural Network Acceleration LAnguage and Compiler
Thomas P. JensenJensen, Thomas P. INRIA Rennes Contextual Equality Saturation
Minseok JeonJeon, Minseok DGISTSouth Korea PAFL: Enhancing Fault Localizers by Leveraging Project-Specific Fault Patterns Committee Member in ICFP Programme Committee within the ICFP Papers-track
Mingyeong JeongJeong, Mingyeong Chungnam National University Type Checking for Python Using Intersection Types
Artur JezJez, Artur University of Wroclaw The Power of Regular Constraint Propagation
Ranjit JhalaJhala, Ranjit University of California at San DiegoUnited States Counterexample-Guided Inference of Modular Specifications
Ranjit JhalaJhala, Ranjit University of California at San DiegoUnited States On the Impact of Formal Verification on Software Development Laurel: Unblocking Automated Verification with Large Language Models
Ruyi JiJi, Ruyi Peking UniversityChina Tunneling Through the Hill: Multi-Way Intersection for Version-Space Algebras in Program Synthesis
Yuchen JiJi, Yuchen ShanghaiTech University Artemis: Toward Accurate Detection of Server-Side Request Forgeries through LLM-Assisted Inter-Procedural Path-Sensitive Taint Analysis
Limin JiaJia, Limin Carnegie Mellon University Session Chair of Verification 1 (part of SPLASH OOPSLA) Session Chair of Calculus (part of SPLASH OOPSLA)
Limin JiaJia, Limin Carnegie Mellon UniversityUnited States Quantified Underapproximation via Labeled Bunches
Limin JiaJia, Limin Carnegie Mellon University Associate Chair in OOPSLA Review Committee within the SPLASH OOPSLA-track
Songlin JiaJia, Songlin Purdue University, USAUnited 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 JiangJiang, Jiajun Tianjin UniversityChina DESIL: Detecting Silent Bugs in MLIR Compiler Infrastructure
Nan JiangJiang, Nan Purdue UniversityUnited States Show Me Why It's Correct: Saving 1/3 of Debugging Time in Program Repair with Interactive Runtime Comparison
Shengyi JiangJiang, Shengyi The University of Hong KongChina Normalization by Evaluation for Non-cumulativity
Yuchao JiangJiang, Yuchao UNSWAustralia Committee Member in Review Committee within the SPLASH Student Research Competition-track
Yuchen JiangJiang, Yuchen University of MichiganUnited States Notions of Stack-manipulating Computation and Relative Monads
Mingyu JoJo, Mingyu Korea University Lemma Discovery for Inductive Equational Proofs via Recursive Function Synthesis
Iris JohnsonJohnson, Iris NHL Stenden University of Applied SciencesNetherlands Committee Member in Program Committee within the SPLASH FARM-track
Max JungJung, Max University of Waterloo Zero-Overhead Lexical Effect Handlers
Ralf JungJung, Ralf ETH ZurichSwitzerland Committee Member in ICFP Programme Committee within the ICFP Papers-track
Sebastian JungesJunges, Sebastian Radboud University A Unifying Approach to Product Constructions for Quantitative Temporal Inference
K Anan KabahaKabaha, Anan Technion, Israel Institute of TechnologyIsrael Quantization with Guaranteed Floating-Point Neural Network Classifications Guarding the Privacy of Label-Only Access to Neural Network Classifiers via Formal Verification
Rohan KadekodiKadekodi, Rohan University of Washington Scalable and Accurate Application-level Crash-Consistency Testing via Representative Testing
Gowtham KakiKaki, Gowtham University of Colorado at BoulderUnited States Bolt-On Strong Consistency: Specification, Implementation, and Verification
Konstantinos KallasKallas, Konstantinos University of California, Los AngelesUnited States Opportunistically Parallel Lambda Calculus
Shoaib KamilKamil, Shoaib Adobe Research Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Arsyad KamiliKamili, Arsyad Singapore A Concurrency-Testing Approach for Detecting Isolation Level Bugs in Database Systems
Ohad KammarKammar, Ohad University of EdinburghUnited Kingdom Frex: Dependently Typed Algebraic Simplification Committee Member in ICFP Programme Committee within the ICFP Papers-track
Gabriel KammerKammer, Gabriel MIT Pyrosome: Verified Compilation for Modular Metatheory
Matthew KaneyKaney, Matthew Weft—Enabling Tidal on the Web
Byeongjee KangKang, Byeongjee Carnegie Mellon UniversityUnited States Fray: An Efficient General-Purpose Concurrency Testing Platform for the JVM
Eunsuk KangKang, Eunsuk Carnegie Mellon UniversityUnited States Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Jeehoon KangKang, Jeehoon FuriosaAISouth Korea Lilo: A Higher-Order, Relational Concurrent Separation Logic for Liveness Revamping Verilog Semantics for Foundational Verification
Yiping KangKang, Yiping University of Michigan MTP: A Meaning-Typed Language Abstraction for AI-Integrated Programming
Ambrus KaposiKaposi, Ambrus ELTE Eötvös Loránd University, Budapest, HungaryHungary Session Chair of Dependent Types (part of ICFP Papers) Type Theory in Type Theory using a Strictified Syntax
Savini KashmiraKashmira, Savini University of Michigan MTP: A Meaning-Typed Language Abstraction for AI-Integrated Programming
Baris KasikciKasikci, Baris University of Michigan, USA Scalable and Accurate Application-level Crash-Consistency Testing via Representative Testing
Jun KatoKato, Jun National Institute of Advanced Industrial Science and Technology (AIST)Japan Committee Member in Program Committee within the SPLASH Onward! Papers-track
Joost-Pieter KatoenKatoen, Joost-Pieter RWTH Aachen UniversityGermany Foundations for Deductive Verification of Continuous Probabilistic Programs: From Lebesgue to Riemann and Back
Hiroyuki KatsuraKatsura, Hiroyuki Automated Catamorphism Synthesis for Solving Constrained Horn Clauses over Algebraic Data Types
Tomer KatzKatz, Tomer Technion Israel Institute of Technology ScooPy: Enhancing Program Synthesis with Nested Example Specifications
Ryan KavanaghKavanagh, Ryan Université du Québec à MontréalCanada Fusing Session-Typed Concurrent Programming into Functional Programming
Alex KavvosKavvos, Alex University of BristolUnited 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 KeizerKeizer, Alex University of Cambridge Interactive Bit Vector Reasoning using Verified Bitblasting
Stephen KellKell, Stephen King's College LondonUnited 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 KelloggKellogg, Martin New Jersey Institute of TechnologyUnited States Sponsorship Co-Chair in Organizing Committee for SPLASH 2025
Marie KerjeanKerjean, Marie CNRS, Université Sorbonne Paris NordFrance Committee Member in ICFP Programme Committee within the ICFP Papers-track
Harun KhanKhan, Harun Stanford University Interactive Bit Vector Reasoning using Verified Bitblasting
Raffi KhatchadourianKhatchadourian, Raffi CUNY Hunter CollegeUnited States Committee Member in Program Committee within the SPLASH Onward! Papers-track
Kaustubh KhulbeKhulbe, Kaustubh University of Illinois at Urbana-Champaign End-to-End Compiler Infrastructure for Emerging Tensor Accelerators
Sandra KieferKiefer, Sandra University of Oxford Detecting and explaining (in-)equivalence of context-free grammars
Donguk KimKim, Donguk South Korea PAFL: Enhancing Fault Localizers by Leveraging Project-Specific Fault Patterns
Hanjun KimKim, Hanjun Yonsei University Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Hannuri KimKim, Hannuri Chungnam National University Toward Automated Verification of Static Analysis Results of Android Applications
Jaewoo KimKim, Jaewoo KAISTSouth Korea Revamping Verilog Semantics for Foundational Verification
Jieung KimKim, Jieung Yonsei UniversitySouth Korea Session Chair of Verification 4 (part of SPLASH OOPSLA)
Jinwoo KimKim, Jinwoo University of Wisconsin-Madison; Seoul National UniversityUnited States Semantics of Sets of Programs
Zachary KincaidKincaid, Zachary Princeton UniversityUnited States Software Model Checking via Summary-Guided Search
Elad KinsbrunerKinsbruner, Elad TechnionIsrael Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Marisa KirisameKirisame, Marisa University of UtahUnited States Incremental Bidirectional Typing via Order Maintenance
Fredrik KjolstadKjolstad, Fredrik Stanford UniversityUnited States REPTILE: Performant Tiling of Recurrences
Mark KleinKlein, Mark Carnegie Mellon University Quantified Underapproximation via Labeled Bunches
Vasileios KlimisKlimis, Vasileios Queen Mary University of London Shaking Up Quantum Simulators with Fuzzing and Rigour
Naoki KobayashiKobayashi, Naoki University of TokyoJapan Automated Catamorphism Synthesis for Solving Constrained Horn Clauses over Algebraic Data Types
Mark KochKoch, Mark Quantinuum Fulls Seldom Differ
Maximilian KodetzkiKodetzki, Maximilian Karlsruhe Institute of TechnologyGermany X-by-Construction: Towards Ensuring Non-Functional Properties in by-Construction Engineering
John C. KolesarKolesar, John C. Yale UniversityUnited States Coinductive Proofs of Regular Expression Equivalence in Zero Knowledge
Ekaterina KomendantskayaKomendantskaya, Ekaterina Heriot-Watt University and Southampton UniversityUnited Kingdom Proof-Carrying Neuro-Symbolic Code
Paulette KoronkevichKoronkevich, Paulette University of British Columbia Type-Preserving Flat Closure Optimization Type Universes as Kripke Worlds
Eric KoskinenKoskinen, Eric Stevens Institute of TechnologyUnited States Abstract Interpretation of Temporal Safety Effects of Higher Order Programs Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Nikita KovalKoval, Nikita JetBrainsNetherlands 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ácsKovács, András University of Gothenburg and Chalmers University of Technology Committee Member in ICFP Programme Committee within the ICFP Papers-track
Laura KovácsKovács, Laura TU WienAustria Divide and Conquer: A Compositional Approach to Game-Theoretic Security
Gintas KraptavičiusKraptavičius, Gintas Concert: Merzmania
Anastasiya Kravchuk-KirilyukKravchuk-Kirilyuk, Anastasiya Harvard UniversityUnited States Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Robbert KrebbersKrebbers, Robbert Radboud University NijmegenNetherlands Verified Interpreters for Dynamic Languages with Applications to the Nix Expression Language
V Krishna NandivadaKrishna 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 KrishnamurthiKrishnamurthi, Shriram Brown UniversityUnited States Steering Committee Member in Steering Committee for SPLASH 2025 OOPSLA Review Committee Co-Chair in Organizing Committee for SPLASH 2025 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 KrogmeierKrogmeier, Paul University of Illinois at Urbana-ChampaignUnited States Synthesizing DSLs for Few-Shot Learning
Sachit KuharKuhar, Sachit Amazon Web Services UTFix: Change Aware Unit Test Repairing using LLM
Iona KuhnKuhn, Iona Saarland UniversityGermany Almost Fair Simulations
Burcu Kulahcioglu OzkanKulahcioglu Ozkan, Burcu Delft University of TechnologyNetherlands Model-guided Fuzzing of Distributed Systems
Kouta KumamotoKumamoto, Kouta An Interactive Learning Environment for Program Design
Lindsey KuperKuper, Lindsey University of California, Santa CruzUnited 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 KurajKuraj, Ivan Massachusetts Institute of Technology Peepco: Batch-Based Consistency Optimization
Ismail KuruKuru, Ismail Drexel UniversityUnited States Modal Abstractions for Virtualizing Memory Addresses
Christian KästnerKästner, Christian Carnegie Mellon University Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Filip KřikavaKřikava, Filip Czech Technical University in PragueCzechia Rebase Chair in Organizing Committee for SPLASH 2025
L Ambroise LafontLafont, Ambroise Inria, France 2-Functoriality of Initial Semantics, and Applications
Patrick LaFontaineLaFontaine, Patrick Purdue UniversityUnited States We’ve Got You Covered: Type-Guided Repair of Incomplete Input Generators
Ignacio LagunaLaguna, Ignacio Lawrence Livermore National LaboratoryUnited States Synthesizing Sound and Precise Abstract Transformers for Nonlinear Hyperbolic PDE Solvers
Shuvendu K. LahiriLahiri, Shuvendu K. Microsoft ResearchUnited States AutoVerus: Automated Proof Generation for Rust Code
Sumit LahiriLahiri, Sumit Indian Institute of Technology KanpurIndia Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Cheuk Tung LAILAI, Cheuk Tung VX Research LimitedUnited Kingdom Extraction and Mutation at a High Level: Template-Based Fuzzing for JavaScript Engines
Jianxin LaiLai, Jianxin Ant Group MetaKernel: Enabling Efficient Encrypted Neural Network Inference Through Unified MVM and Convolution
Akash LalLal, Akash Microsoft ResearchIndia Memory-Safety Verification of Open Programs With Angelic Assumptions
Kait LamLam, Kait Defence Science and Technology Group / School of EECS, University of Queensland Translation Validation for LLVM's AArch64 Backend
Patrick LamLam, Patrick University of Waterloo Committee Member in Program Committee within the SPLASH Onward! Papers-track
Ada LambaLamba, Ada Ohio State University Carapace: Static–Dynamic Information Flow Control in Rust
Thomas LamiauxLamiaux, Thomas University of Paris-Saclay, Ens Paris-Saclay 2-Functoriality of Initial Semantics, and Applications
Leonidas LampropoulosLampropoulos, Leonidas University of Maryland, College ParkGreece Compositional Quantum Control Flow with Efficient Compilation in Qunity
Yingjun LanLan, Yingjun Formal Verification of Graham's Scan Algorithm
Jens Kanstrup LarsenLarsen, Jens Kanstrup DTUDenmark Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Jacob LaurelLaurel, Jacob Georgia Institute of TechnologyUnited States Synthesizing Sound and Precise Abstract Transformers for Nonlinear Hyperbolic PDE Solvers Precise Abstract Interpretation of Probabilistic Programs with Interval Data Uncertainty
Jonathan LaurentLaurent, Jonathan Carnegie Mellon University / Karlsruhe Institute of Technology Adaptive Shielding via Parametric Safety Proofs
Tom LauwaertsLauwaerts, Tom Universiteit Gent, BelgiumBelgium MIO: Multiverse Debugging in the face of Input/Output
Tony LawLaw, Tony Univ Rennes, Inria, CNRS, IRISA A Mechanized Semantics for Dataflow Circuits
Julia LawallLawall, Julia InriaFrance Automating maintenance of the Linux kernel: a perspective over 20 years
Alan LawrenceLawrence, Alan Quantinuum Fulls Seldom Differ
Isabella LaybournLaybourn, Isabella Carnegie Mellon UniversityUnited States Fray: An Efficient General-Purpose Concurrency Testing Platform for the JVM
Tristan Le GallLe Gall, Tristan CEA LIST Verifying Neural Networks with PyRAT
Quang Loc LeLe, Quang Loc University College LondonUnited Kingdom Committee Member in Program Committee within the SAS -track
Van-Hoang LeLe, Van-Hoang The University of NewcastleAustralia Committee Member in Review Committee within the SPLASH Student Research Competition-track
Doug LeaLea, Doug State University of New York (SUNY) OswegoUnited States Soundness of Predictive Concurrency Analyses
Ashley LeeLee, Ashley University of California, Santa Cruz SafeRace: Assessing and Addressing WebGPU Memory Safety in the Presence of Data Races
Dongjae LeeLee, Dongjae Massachusetts Institute of Technology Lilo: A Higher-Order, Relational Concurrent Separation Logic for Liveness
Edward LeeLee, Edward University of Waterloo; University of Toronto ScarboroughCanada Qualified Types with Boolean Algebras
HYEONJIN LEELEE, HYEONJIN On A Multitier Actor Programming Language
Jaeseo LeeLee, Jaeseo POSTECHSouth Korea Formal Analysis of Networked PLC Controllers Interacting with Physical Environments
Janggun LeeLee, Janggun KAIST Lilo: A Higher-Order, Relational Concurrent Separation Logic for Liveness
Jay LeeLee, Jay Seoul National UniversitySouth Korea React-tRace: A Semantics for Understanding React Hooks
Juneyoung LeeLee, Juneyoung AWS Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Keonho LeeLee, Keonho University of California, Irvine Towards Verifying Crash Consistency
Leo Seojun LeeLee, Leo Seojun University of Oxford Mind the Abstraction Gap: Bringing Equality Saturation to Real-World ML Compilers
Shaun Christopher LeeLee, Shaun Christopher University of Washington Scalable and Accurate Application-level Crash-Consistency Testing via Representative Testing
Sungho LeeLee, Sungho Chungnam National University, KoreaSouth 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 LeeLee, Woosuk Hanyang UniversitySouth Korea Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Yunjeong LeeLee, Yunjeong National University of SingaporeSingapore Student Volunteer Co-Chair in Organizing Committee for SPLASH 2025
Zheng Han LeeLee, Zheng Han National University of Singapore, Singapore Efficient Decrease-And-Conquer Linearizability Monitoring
Owolabi LegunsenLegunsen, Owolabi Cornell UniversityUnited States Session Chair of Testing 2 (part of SPLASH OOPSLA) Faster Explicit-Trace Monitoring-Oriented Programming for Runtime Verification of Software Tests
Julien LehmannLehmann, Julien CEA, LIST, FranceFrance Verifying Neural Networks with PyRAT
Daan LeijenLeijen, Daan Microsoft ResearchUnited States Committee Member in Program Committee within the SPLASH Onward! Papers-track First-Order Laziness
Augustin LemesleLemesle, Augustin CEA, LIST, France Verifying Neural Networks with PyRAT
Caroline LemieuxLemieux, Caroline University of British ColumbiaCanada Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Damitha LenadoraLenadora, Damitha University of Illinois at Urbana-Champaign GALA: A High Performance Graph Neural Network Acceleration LAnguage and Compiler
Connor LenihanLenihan, Connor King's College London Shaking Up Quantum Simulators with Fuzzing and Rigour AccelerQ: Accelerating Quantum Eigensolvers With Machine Learning on Quantum Simulators
Sorin LernerLerner, Sorin University of California at San DiegoUnited States Committee Member in Program Committee within the SPLASH Onward! Papers-track
Mohsen LesaniLesani, Mohsen University of California at Santa Cruz Hambazi: Spatial Coordination Synthesis for Augmented Reality
Martin LesterLester, Martin University of ReadingUnited Kingdom Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Danya LetteLette, Danya Committee Member in SAS Artifact Evaluation Committee within the SAS Artifact-track
Kyla H. LevinLevin, Kyla H. University of Massachusetts Amherst, USAUnited States RestPi: Path-Sensitive Type Inference for REST APIs
Reese LevineLevine, Reese SafeRace: Assessing and Addressing WebGPU Memory Safety in the Presence of Data Races
Nicholas V. LewchenkoLewchenko, Nicholas V. University of Colorado BoulderUnited States Bolt-On Strong Consistency: Specification, Implementation, and Verification
Ondřej LhotákLhoták, Ondřej University of WaterlooCanada Flix: A Design for Language-Integrated Datalog Qualified Types with Boolean Algebras
Ao LiLi, Ao Carnegie Mellon UniversityUnited States Fray: An Efficient General-Purpose Concurrency Testing Platform for the JVM
Baichuan LiLi, Baichuan University of Michigan MTP: A Meaning-Typed Language Abstraction for AI-Integrated Programming
Baixuan LiLi, 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 LiLi, Chenxi Nanjing University, China Two Approaches to Fast Bytecode Frontend for Static Analysis
Chenxing LiLi, Chenxing Shanghai Tree-Graph Blockchain Research InstituteChina HEMVM: a Heterogeneous Blockchain Framework for Interoperable Virtual Machines
Ding LiLi, Ding Peking UniversityChina Orax: A Feedback-Driven Framework for Efficiently Solving Satisfiability Modulo Theories and Oracles
Elaine LiLi, Elaine NYUUnited States Characterizing Implementability of Global Protocols with Infinite States and Data
Guanyan LiLi, Guanyan University of Oxford Structural Abstraction and Refinement for Probabilistic Programs
Haofeng LiLi, Haofeng SKLP, Institute of Computing Technology, CASChina Fast Client-Driven CFL-Reachability via Regularization-Based Graph Simplification
Haoran LiLi, Haoran Shanghai Jiao Tong University Binary Cryptographic Function Identification via Similarity Analysis with Path-insensitive Emulation
Jianlin LiLi, Jianlin University of WaterlooCanada Compiling with Generating Functions
John LiLi, John Northeastern UniversityUnited States Multi-Language Probabilistic Programming From Linearity to Borrowing
Juanen LiLi, Juanen Beijing Normal University Structural Abstraction and Refinement for Probabilistic Programs
Kwing Hei LiLi, Kwing Hei Aarhus UniversityDenmark Separation Logics for Probability, Concurrency, and Security Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs
Lian LiLi, Lian Institute of Computing Technology at Chinese Academy of Sciences; University of Chinese Academy of SciencesChina Fast Client-Driven CFL-Reachability via Regularization-Based Graph Simplification
Liyi LiLi, Liyi Iowa State UniversityUnited States Embedding Quantum Program Verification into Dafny A Haskell Adiabatic DSL: Solving Classical Optimization Problems on Quantum Hardware
Long LiLi, Long Ant Group MetaKernel: Enabling Efficient Encrypted Neural Network Inference Through Unified MVM and Convolution
Mingyi LiLi, Mingyi Institute of Computing Technology, CASChina Stencil-Lifting: Hierarchical Recursive Lifting System for Extracting Summary of Stencil Kernel in Legacy Codes
Peilun LiLi, Peilun Shanghai Tree-Graph Blockchain Research Institute HEMVM: a Heterogeneous Blockchain Framework for Interoperable Virtual Machines
Shangyu LiLi, Shangyu The Hong Kong University of Science and Technology A Sound Static Analysis Approach to I/O API Migration
Shaohua LiLi, Shaohua The Chinese University of Hong KongHong Kong SAR China An Empirical Study of Bugs in the rustc Compiler Interleaving Large Language Models for Compiler Testing
Tianchi LiLi, Tianchi Peking University, ChinaChina Combining Formal and Informal Information in Bayesian Program Analysis via Soft Evidences
Wu Angela LiLi, Wu Angela Rice University Efficient Algorithms for the Uniform Tokenization Problem
Xuandong LiLi, Xuandong Nanjing UniversityChina 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 LiLi, Xuheng Columbia University AutoVerus: Automated Proof Generation for Rust Code
Yi LiLi, Yi Nanyang Technological UniversitySingapore TailTracer: Continuous Tail Tracing for Production Use
Yihe LiLi, Yihe National University of Singapore Large Language Model powered Symbolic Execution
Yue LiLi, Yue Nanjing UniversityChina Two Approaches to Fast Bytecode Frontend for Static Analysis Co-chair in SAS Artifact Evaluation Committee within the SAS Artifact-track
Zhong LiLi, Zhong Nanjing UniversityChina PReMM: LLM-Based Program Repair for Multi-Method Bugs via Divide and Conquer
Qihao LianLian, Qihao Peking UniversityChina Automatic Linear Resource Bound Analysis for Rust via Prophecy Potentials
Peng LiangLiang, Peng Wuhan University, ChinaChina Finding Compiler Bugs through Cross-Language Code Generator and Differential Testing
Nathan LiittschwagerLiittschwager, Nathan University of California, Santa Cruz CRDT Emulation, Simulation, and Representation Independence
Anthony Widjaja LinLin, Anthony Widjaja RPTU Kaiserslautern-Landau and Max-Planck Institute for Software Systems The Power of Regular Constraint Propagation
Haoran LinLin, Haoran Nanjing University, China Two Approaches to Fast Bytecode Frontend for Static Analysis
Jenny Han LinLin, Jenny Han University of UtahUnited States Polynomial-Time Program Equivalence for Machine Knitting
Youfang LinLin, Youfang Beijing Jiaotong University Fuzzing C++ Compilers via Type-Driven Mutation
Sam LindleyLindley, Sam University of EdinburghUnited Kingdom Modal Effect Types First-Order Laziness
Teodors LisovenkoLisovenko, Teodors Ca' Foscari University of VeniceItaly Committee Member in SAS Artifact Evaluation Committee within the SAS Artifact-track
Kyle LittleLittle, Kyle University of Utah SafeRace: Assessing and Addressing WebGPU Memory Safety in the Presence of Data Races
Amanda LiuLiu, Amanda Massachusetts Institute of TechnologyUnited States Gauguin, Descartes, Bayes: A Diurnal Golem's Brain
Cyrus LiuLiu, Cyrus Samsung SemiconductorUnited States Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Hanzhi LiuLiu, Hanzhi University of California, Santa Barbara & Riema LabsUnited States Tabby: A Synthesis-Aided Compiler for High-Performance Zero-Knowledge Proof Circuits
Jie LiuLiu, Jie ByteDanceChina Committee Member in SAS Artifact Evaluation Committee within the SAS Artifact-track
Junrui LiuLiu, Junrui University of California, Santa BarbaraUnited States Tabby: A Synthesis-Aided Compiler for High-Performance Zero-Knowledge Proof Circuits
Kui LiuLiu, Kui HuaweiChina PReMM: LLM-Based Program Repair for Multi-Method Bugs via Divide and Conquer
Lang LiuLiu, Lang Illinois Institute of Technology Quantified Underapproximation via Labeled Bunches
Shuyang LiuLiu, Shuyang Soundness of Predictive Concurrency Analyses
Tianyi LiuLiu, Tianyi Nanjing UniversityChina TailTracer: Continuous Tail Tracing for Production Use
Xinxin LiuLiu, Xinxin Institute of software, Chinese academy of sciences HpC: A Calculus for Hybrid and Mobile Systems
Yan LiuLiu, Yan Ant Group MetaKernel: Enabling Efficient Encrypted Neural Network Inference Through Unified MVM and Convolution
Yang LiuLiu, Yang Nanyang Technological UniversitySingapore [Closed Session] Adjudication meeting for SIGPLAN's John Vlissides award Committee Member in Program Committee and Panel within the SPLASH Doctoral Symposium-track
Yue LiuLiu, Yue Data61, CSIRO Committee Member in Review Committee within the SPLASH Student Research Competition-track
Zixi LiuLiu, Zixi Nanjing UniversityChina An Empirical Study of Bugs in the rustc Compiler
Francesco LogozzoLogozzo, Francesco MetaUnited States Revealing Sources of (Memory) Errors via Backward Analysis
Debasmita LoharLohar, Debasmita Karlsruhe Institute of TechnologyGermany Cost of Soundness in Mixed-Precision Tuning
Tommie LombartsLombarts, Tommie Eindhoven University of Technology Personalization of Programming Education: An NLP-based Bi-dimensional Classification of Programming Exercises
Fan LongLong, Fan University of TorontoCanada HEMVM: a Heterogeneous Blockchain Framework for Interoperable Virtual Machines
Huan LongLong, Huan Shanghai Jiao Tong University A Programming Language for Feasible Solutions
Nuno P. LopesLopes, Nuno P. INESC-ID; Instituto Superior Técnico - University of LisbonPortugal Translation Validation for LLVM's AArch64 Backend
Jacob R. LorchLorch, Jacob R. Microsoft Research, n.n. AutoVerus: Automated Proof Generation for Rust Code
Anton LorenzenLorenzen, Anton University of EdinburghUnited Kingdom Modal Effect Types First-Order Laziness
Yiling LouLou, Yiling University of Illinois at Urbana-ChampaignUnited States Show Me Why It's Correct: Saving 1/3 of Debugging Time in Program Repair with Interactive Runtime Comparison
Jiayi LuLu, Jiayi Zhejiang University A complete formal semantics of eBPF instruction set architecture for Solana
Jie LuLu, Jie SKLP, Institute of Computing Technology, CAS, China Fast Client-Driven CFL-Reachability via Regularization-Based Graph Simplification
Longlong LuLu, 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 LuLu, Shan Microsoft; University of ChicagoUnited States AutoVerus: Automated Proof Generation for Rust Code
Shuai LuLu, Shuai Microsoft ResearchChina AutoVerus: Automated Proof Generation for Rust Code
Sirui LuLu, Sirui OpenAIUnited States HieraSynth: A Parallel Framework for Complete Super-Optimization with Hierarchical Space Decomposition
Yifei LuLu, 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 LuLu, Yunping Fudan University JavART: a Lightweight Rule-Based JIT Compiler Using Translation Rules Extracted from a Learning Approach
Mingyuan LuoLuo, Mingyuan Fudan University ApkDiffer: Accurate and Scalable Cross-Version Diffing Analysis for Android Applications
Ning LuoLuo, Ning UIUCUnited States Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Matthew LutzeLutze, Matthew Aarhus University The Simple Essence of Monomorphization Type-safe Blazon - Enforcing Pedantry in Heraldic Design
Pedro López-GarcíaLópez-García, Pedro IMDEA Software Institute Committee Member in Program Committee within the SAS -track
Júnior LöffLöff, Júnior Università della Svizzera italiana HeapBuffers: Why not just using a binary serialization format for your managed memory?
Andreas LööwLööw, Andreas Imperial College LondonUnited Kingdom The Simulation Semantics of Synthesisable Verilog Compositional Symbolic Execution for the Next 700 Memory Models
M Chenyang MaMa, Chenyang Nanjing University of Science and Technology DepFuzz: Efficient Smart Contract Fuzzing with Function Dependence Guidance
Cong MaMa, Cong University of WaterlooCanada Lexical Effect Handler: Fast by Design, Correct by Proof Zero-Overhead Lexical Effect Handlers
Hui MaMa, 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 MaMa, Xiaofei AWS AI Labs UTFix: Change Aware Unit Test Repairing using LLM
Xiaotian MaMa, Xiaotian Nanjing University of Science and TechnologyChina Finding Compiler Bugs through Cross-Language Code Generator and Differential Testing
Zhongkui MaMa, Zhongkui The University of QueenslandAustralia Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track Convex Hull Approximation for Activation Functions
Aravind MachiryMachiry, Aravind Purdue UniversityUnited States Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Julian MackayMackay, Julian Kry10 Ltd Reasoning about External Calls
Stefan MadaMada, Stefan University of Utah Translation Validation for LLVM's AArch64 Backend
Anil MadhavapeddyMadhavapeddy, Anil University of Cambridge, UKUnited Kingdom A guided tour through Oxidized OCaml Functional Networking for Millions of Docker Desktops (Experience Report)
P. MadhusudanMadhusudan, P. University of Illinois at Urbana-ChampaignUnited States FO-Complete Program Verification for Heap Logics Synthesizing DSLs for Few-Shot Learning
Jean-Marie MadiotMadiot, Jean-Marie InriaFrance Formal Semantics and Program Logics for a Fragment of OCaml
Magnus MadsenMadsen, Magnus Aarhus UniversityDenmark 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 MadsenMadsen, Ole Lehrmann Aarhus UniversityDenmark Committee Member in Program Committee within the SPLASH Onward! Papers-track
Enrico MagnagoMagnago, Enrico Amazon Web Services Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Romina MahinpeiMahinpei, Romina Princeton University Interactive Theorem Provers for Proof Education
Daryl MaierMaier, Daryl IBM CanadaCanada CoSSJIT: Combining Static Analysis and Speculation in JIT Compilers
Kenji MaillardMaillard, Kenji Inria – LS2N, Université de NantesFrance Incremental Certified Programming
Rupak MajumdarMajumdar, Rupak MPI-SWSGermany Model-guided Fuzzing of Distributed Systems
Caleb MalchikMalchik, Caleb Yale University On Collective Control over User Interfaces in the Face of Network Eﬀects
Konstantinos MamourasMamouras, Konstantinos Rice UniversityUnited States Efficient Algorithms for the Uniform Tokenization Problem
Wensen MaoMao, Wensen Rutgers University Abstraction Refinement-guided Program Synthesis for Robot Learning from Demonstrations
Michaël MarcozziMarcozzi, Michaël Université Paris-Saclay, CEA, ListFrance Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Dylan MarinhoMarinho, Dylan Sorbonne Université, CNRS UMR 7606, LIP6, Paris, FranceFrance Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Oliver MarkgrafMarkgraf, Oliver RPTU Kaiserslautern-Landau The Power of Regular Constraint Propagation
Stefan MarrMarr, Stefan Johannes Kepler University LinzAustria 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 MarsMars, Jason University of Michigan MTP: A Meaning-Typed Language Abstraction for AI-Integrated Programming
Brianna MarshallMarshall, Brianna Northeastern UniversityUnited States From Linearity to Borrowing
Chris MartensMartens, Chris Northeastern UniversityUnited States PC Member in Program Committee within the SPLASH Onward! Essays-track Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Ruben MartinsMartins, Ruben Carnegie Mellon UniversityUnited States Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Guido MartínezMartínez, Guido Microsoft ResearchUnited States SecRef: Securely Sharing Mutable References between Verified and Unverified Code in F
Kristóf MarussyMarussy, Kristóf Budapest University of Technology and EconomicsHungary Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Isabella MastroeniMastroeni, Isabella University of VeronaItaly Relating Distances and Abstractions: An Abstract Interpretation Perspective
Hidehiko MasuharaMasuhara, Hidehiko Institute of Science TokyoJapan 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 NicolajsenMateos Nicolajsen, Sebastian IT University of CopenhagenDenmark Committee Member in Program Commitee within the SPLASH -E-track
Umang MathurMathur, Umang National University of SingaporeSingapore Efficient Decrease-And-Conquer Linearizability Monitoring Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Umang MathurMathur, Umang National University of Singapore, SingaporeSingapore View Types in Rust
Damiano MazzaMazza, Damiano CNRS, LIPN, Université Sorbonne Paris NordFrance Committee Member in ICFP Programme Committee within the ICFP Papers-track
Riccardo MazzaMazza, Riccardo APM SaluzzoItaly Sonic Earth - An Algorithmic Performance Approach to Real-Time Environmental Sonification Concert: Sonic Earth
Conor McBrideMcBride, Conor University of Strathclyde Fulls Seldom Differ
James McCannMcCann, James Carnegie Mellon UniversityUnited States Committee Member in Program Committee within the SPLASH FARM-track Polynomial-Time Program Equivalence for Machine Knitting
Kathryn S McKinleyMcKinley, 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 McLoughlinMcLoughlin, Michael Carnegie Mellon UniversityUnited States Scaling Instruction-Selection Verification against Authoritative ISA Semantics
S Hessam M MehrMehr, S Hessam M University of Glasgow TideScript: A Domain Specific Language for Peptide Chemistry
Vaibhav MehtaMehta, Vaibhav Cornell UniversityUnited States A Hoare Logic For Symmetry Properties
Olivier MelançonMelançon, Olivier Université de MontréalCanada Float Self-Tagging
Stephen MellMell, Stephen University of Pennsylvania Opportunistically Parallel Lambda Calculus
Guillaume MelquiondMelquiond, Guillaume Université Paris-Saclay - CNRS - ENS Paris-Saclay - InriaFrance Committee Member in ICFP Programme Committee within the ICFP Papers-track
Charith MendisMendis, Charith University of Illinois at Urbana-ChampaignUnited 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 MengMeng, Eagon MIT What You See Is What It Does: A Structural Pattern for Legible Software
Ruijie MengMeng, Ruijie National University of Singapore, SingaporeSingapore Large Language Model powered Symbolic Execution
Mira MeziniMezini, Mira TU Darmstadt; hessian.AI; National Research Center for Applied Cybersecurity ATHENEGermany Steering Committee Member in Steering Committee for SPLASH 2025
Benjamin MikekMikek, Benjamin Georgia Institute of Technology Towards Compiler-Guided Static Analysis
Mae MilanoMilano, Mae Princeton UniversityUnited 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 MiliusMilius, Stefan Friedrich-Alexander University Erlangen-NürnbergGermany Bialgebraic Reasoning on Stateful Languages
Heather MillerMiller, Heather Carnegie Mellon University and Two Sigma Debugging WebAssembly? Put some Whamm on it!
Todd MillsteinMillstein, Todd University of California at Los AngelesUnited 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 MintsMints, Mikhail California Institute of TechnologyUnited 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 MisailovicMisailovic, Sasa University of Illinois at Urbana-ChampaignUnited 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 MishraMishra, Ashish IIT HyderabadIndia 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 MisuMisu, Md Rakib Hossain University of California IrvineUnited States AutoVerus: Automated Proof Generation for Rust Code
Sidi Mohamed BeillahiMohamed Beillahi, Sidi University of TorontoCanada HEMVM: a Heterogeneous Blockchain Framework for Interoperable Virtual Machines Committee Member in Program Committee within the SAS -track
Abdalrhman MohamedMohamed, Abdalrhman Stanford University Interactive Bit Vector Reasoning using Verified Bitblasting
Isidore MohrMohr, Isidore Concert: Girard’s Paradox Girard's Paradox as Structure Music
Alexandre MoineMoine, Alexandre New York UniversityUnited States Committee Member in ICFP Programme Committee within the ICFP Papers-track
Evgenii MoiseenkoMoiseenko, Evgenii JetBrains Research Testing concurrent code on JVM with Lincheck
Abtin MolaviMolavi, Abtin University of Wisconsin-Madison Dependency-Aware Compilation for Surface Code Quantum Architectures Compiling Quantum Circuits
Raphaël MonatMonat, Raphaël Inria and University of LilleFrance Committee Member in Program Committee within the SAS -track
Fabrizio MontesiMontesi, Fabrizio University of Southern DenmarkDenmark Relax! The Semilenient Core of Choreographic Programming (Functional Pearl)
Arjan J. MooijMooij, Arjan J. Zürich University of Applied Sciences Language-Parametric Reference Synthesis
David MoonMoon, David University of MichiganUnited States Syntactic Completions with Material Obligations
José MoralesMorales, José IMDEA Software InstituteSpain Committee Member in Steering Committee within the SAS -track
Angelica MoreiraMoreira, Angelica Microsoft ResearchCanada Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Gabriel A. MorenoMoreno, Gabriel A. Carnegie Mellon University Software Engineering InstituteUnited States Quantified Underapproximation via Labeled Bunches
Nicholas MorrisMorris, Nicholas University of Glasgow TideScript: A Domain Specific Language for Peptide Chemistry
Cameron MoyMoy, Cameron Northeastern UniversityUnited States Teaching Software Specification (Experience Report)
Fabian MuehlboeckMuehlboeck, Fabian Australian National UniversityAustralia View Types in Rust
Eric MugnierMugnier, Eric University of California San Diego On the Impact of Formal Verification on Software Development Laurel: Unblocking Automated Verification with Large Language Models
Serkan MuhcuMuhcu, Serkan Technische Universität Berlin Multiple Resumptions and Local Mutable State, Directly
Prasita MukherjeeMukherjee, Prasita Purdue University KestRel: Relational Verification Using E-Graphs for Program Alignment
Adithya MuraliMurali, Adithya University of Illinois at Urbana-ChampaignUnited States FO-Complete Program Verification for Heap Logics
Charlie MurphyMurphy, Charlie Amazon Web Services, USAUnited States Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Gail MurphyMurphy, Gail University of British ColumbiaCanada An Exploration of How Generative AI Affects Workflow and Collaboration in a Software Engineering Course
Andrew MyersMyers, Andrew Cornell University SIGPLAN Chair in Steering Committee for SPLASH 2025
Anders MøllerMøller, Anders Aarhus UniversityDenmark SIGPLAN Vice Chair in Steering Committee for SPLASH 2025
Marius MüllerMüller, Marius University of TübingenGermany Compiling Classical Sequent Calculus to Stock Hardware: The Duality of Compilation
Peter MüllerMüller, Peter ETH ZurichSwitzerland 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
N Ritam NagNag, Ritam MIT Pyrosome: Verified Compilation for Modular Metatheory
Kartik NagarNagar, Kartik IIT MadrasIndia Automatically Verifying Replication-aware Linearizability Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Santosh NagarakatteNagarakatte, Santosh Rutgers UniversityUnited States Comparing the Precision of Abstract Operators in the eBPF Verifier using Differential Synthesis
Srinidhi NagendraNagendra, Srinidhi IRIF, Chennai Mathematical InstituteFrance Model-guided Fuzzing of Distributed Systems
Shaan NagyNagy, Shaan University of Wisconsin-Madison Semantics of Sets of Programs
Tomoki NakamaruNakamaru, Tomoki The University of TokyoJapan Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Kedar NamjoshiNamjoshi, Kedar Nokia Bell LabsUnited States Committee Member in Steering Committee within the SAS -track
Chandrakana NandiNandi, Chandrakana CertoraUnited 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 NanevskiNanevski, Aleksandar IMDEA Software InstituteSpain Verifying Graph Algorithms in Separation Logic: A Case for an Algebraic Approach
Daniele Nantes-SobrinhoNantes-Sobrinho, Daniele Imperial College LondonUnited Kingdom Compositional Symbolic Execution for the Next 700 Memory Models
Srinivas NarayanaNarayana, Srinivas Rutgers University Comparing the Precision of Abstract Operators in the eBPF Verifier using Differential Synthesis
Nuntipat NarkthongNarkthong, Nuntipat Northeastern UniversityUnited States Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Jorge A. NavasNavas, Jorge A. CertoraUnited States A Flow-Sensitive Refinement Type System for Verifying eBPF Programs Committee Member in Program Committee within the SAS -track
Amirmohammad NazariNazari, Amirmohammad University of Southern CaliforniaUnited States Committee Member in SAS Artifact Evaluation Committee within the SAS Artifact-track
Ian NealNeal, Ian University of Michigan and Veridise Scalable and Accurate Application-level Crash-Consistency Testing via Representative Testing
Luca NegriniNegrini, Luca Ca’ Foscari University of VeniceItaly Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Vladyslav NekriachNekriach, Vladyslav University Of TorontoCanada HEMVM: a Heterogeneous Blockchain Framework for Interoperable Virtual Machines
Tim NelsonNelson, Tim Brown UniversityUnited States Committee Member in Program Commitee within the SPLASH -E-track
Max S. NewNew, Max S. University of MichiganUnited States Notions of Stack-manipulating Computation and Relative Monads
Hoan NguyenNguyen, Hoan Amazon Web Services Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Yunbo NiNi, Yunbo The Chinese University of Hong KongHong 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 NicolaNicola, Mihai Stevens Institute of Technology Abstract Interpretation of Temporal Safety Effects of Higher Order Programs
Oscar NierstraszNierstrasz, Oscar feenk.comSwitzerland PC Member in Program Committee within the SPLASH Onward! Essays-track
Yue NiuNiu, Yue National Institute of Informatics Integrating Resource Analyses via Resource Decomposition
James NobleNoble, James Independent. Wellington, NZNew Zealand Reasoning about External Calls Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track Exploring The Design Space For Runtime Enforcement of Dynamic Capabilities
Michael NorrishNorrish, Michael Australian National UniversityAustralia Reproducibility Debt in Scientific Software
Aman NougrahiyaNougrahiya, Aman IIT MadrasIndia IncIDFA: An Efficient and Generic Algorithm for Incremental Iterative Dataflow Analysis
Clemens Nylandsted KlokmoseNylandsted Klokmose, Clemens Aarhus UniversityDenmark 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
O Liam O'ConnorO'Connor, Liam Australian National UniversityAustralia ICFP Contest Report Committee Member in ICFP Programme Committee within the ICFP Papers-track
Lina OchoaOchoa, Lina Eindhoven University of Technology Personalization of Programming Education: An NLP-based Bi-dimensional Classification of Programming Exercises
Martin OderskyOdersky, Martin EPFLSwitzerland What's in the Box: Ergonomic and Expressive Capture Tracking over Generic Data Structures
Hakjoo OhOh, Hakjoo Korea UniversitySouth 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 ) Session Chair of Abstract Interpretation (part of SAS ) Co-chair in Program Committee within the SAS -track
Wonseok OhOh, Wonseok Korea UniversitySouth Korea Committee Member in SAS Artifact Evaluation Committee within the SAS Artifact-track
Bruno C. d. S. OliveiraOliveira, Bruno C. d. S. University of Hong KongChina 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 OlivieriOlivieri, Luca Ca’ Foscari University of VeniceItaly Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Cyrus OmarOmar, Cyrus University of MichiganUnited States Incremental Bidirectional Typing via Order Maintenance Syntactic Completions with Material Obligations
Steve OneyOney, Steve University of Michigan Committee Member in Program Committee within the SPLASH Onward! Papers-track
Emily OngOng, Emily National University of SingaporeSingapore Siloso: Finding Logic Bugs in RDBMS via Dialect-Adaptable Reference Engine Construction
Dominic OrchardOrchard, Dominic University of Cambridge; University of KentUnited Kingdom Session Chair of Types and Specifications (part of ICFP Papers)
Klaus OstermannOstermann, Klaus University of TübingenGermany Compiling Classical Sequent Calculus to Stock Hardware: The Duality of Compilation Committee Member in ICFP Programme Committee within the ICFP Papers-track
Rodrigo OtoniOtoni, Rodrigo USI LuganoSwitzerland A Language for Quantifying Quantum Network Behavior
P Rohan PadhyePadhye, Rohan Carnegie Mellon UniversityUnited States Fray: An Efficient General-Purpose Concurrency Testing Platform for the JVM
Oded PadonPadon, Oded Weizmann Institute of ScienceIsrael Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Sreepathi PaiPai, Sreepathi University of RochesterUnited States Formalizing Linear Motion G-code for Invariant Checking and Differential Testing of Fabrication Tools
Sasha PakPak, Sasha Australian National UniversityAustralia Verifying Extract Method Refactoring in Rust View Types in Rust
Jens PalsbergPalsberg, Jens University of California, Los Angeles (UCLA)United States Session Chair of Quantum (part of SPLASH OOPSLA) Soundness of Predictive Concurrency Analyses
Minxue PanPan, Minxue Nanjing UniversityChina Towards a Theoretically-Backed and Practical Framework for Selective Object-Sensitive Pointer Analysis
Pavel PanchekhaPanchekha, Pavel University of UtahUnited States Incremental Bidirectional Typing via Order Maintenance
Naomi PandaPanda, Naomi Waddle: A Serious Game to Teach Writing, Reading, and Debugging Programs
Awanish PandeyPandey, Awanish IIT RoorkeeIndia Committee Member in Review Committee within the SPLASH Student Research Competition-track
Akash PardeshiPardeshi, Akash University of Illinois at Urbana-ChampaignUnited States End-to-End Compiler Infrastructure for Emerging Tensor Accelerators
Pavel ParizekParizek, Pavel Charles University Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Jihee ParkPark, Jihee KAISTSouth Korea Bridging the Gap between Real-World and Formal Binary Lifting through Filtered-Simulation
Jihyeok ParkPark, Jihyeok Korea UniversitySouth Korea Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track Committee Member in Program Committee within the SAS -track
Kanghee ParkPark, Kanghee University of Wisconsin-MadisonUnited States LOUD: Synthesizing Strongest and Weakest Specifications
Seung Hoon ParkPark, Seung Hoon Imperial College London Compositional Symbolic Execution for the Next 700 Memory Models
Tae Hong ParkPark, Tae Hong Purdue UniversityUnited States Program Chair in Organizing Committee within the SPLASH FARM-track
Bryan ParnoParno, Bryan Carnegie Mellon UniversityUnited States Scaling Instruction-Selection Verification against Authoritative ISA Semantics
Lionel ParreauxParreaux, 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 PartowPartow, Pouya Birmingham University Big Steps in Higher-Order Mathematical Operational Semantics
Radha PatelPatel, Radha MIT CSAIL Finch: Sparse and Structured Tensor Programming with Control Flow
Daniel PattersonPatterson, Daniel Northeastern UniversityUnited 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 PaynePayne, William UNC School of Information and Library Science Weft—Enabling Tidal on the Web
Luke PearsonPearson, Luke Polychain Capital Tabby: A Synthesis-Aided Compiler for High-Performance Zero-Knowledge Proof Circuits
Anurudh PeduriPeduri, Anurudh Ruhr University Bochum QbC: Quantum Correctness by Construction
Yu PeiPei, Yu Hong Kong Polytechnic UniversityChina PReMM: LLM-Based Program Repair for Multi-Method Bugs via Divide and Conquer
Hila PelegPeleg, Hila TechnionIsrael ScooPy: Enhancing Program Synthesis with Nested Example Specifications
Daniel A. A. PelsmaekerPelsmaeker, Daniel A. A. Delft University of Technology, NetherlandsNetherlands Language-Parametric Reference Synthesis
Mai Jacob PengPeng, Mai Jacob McGill UniversityCanada Sound and Modular Activity Analysis for Automatic Differentiation in MLIR
Wei PengPeng, Wei Fudan University JavART: a Lightweight Rule-Based JIT Compiler Using Translation Rules Extracted from a Learning Approach
Xuanyu PengPeng, Xuanyu University of California, San DiegoUnited States LOUD: Synthesizing Strongest and Weakest Specifications
Yiteng PengPeng, Yiteng Hong Kong University of Science and TechnologyChina Extraction and Mutation at a High Level: Template-Based Fuzzing for JavaScript Engines
João PereiraPereira, João ETH Zurich Modular Reasoning about Global Variables and Their Initialization A Refinement Methodology for Distributed Programs in Rust
Mário PereiraPereira, Mário NOVA LINCS & DI -- Nova School of Science and TechnologyPortugal Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Daniel PerelmanPerelman, Daniel MicrosoftUnited States Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Roly PereraPerera, Roly University of Cambridge/University of BristolUnited Kingdom Committee Member in Program Committee within the SPLASH Onward! Papers-track
Basile PesinPesin, Basile Ecole Nationale de l'Aviation Civile (ENAC) Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Edward PetersPeters, Edward Pushing the Information-Theoretic Limits of Random Access Lists
Anja Petković KomelPetković Komel, Anja Argot Collective Divide and Conquer: A Compositional Approach to Game-Theoretic Security
Tomas PetricekPetricek, Tomas Charles UniversityCzechia 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 PetrisanPetrisan, Daniela IRIF, Université Paris DiderotFrance Committee Member in ICFP Programme Committee within the ICFP Papers-track
Loïc PeyrotPeyrot, Loïc IMDEA Software Institute Polymorphic Records for Dynamic Languages
Simon Peyton JonesPeyton Jones, Simon Epic Games United Kingdom Committee Member in ICFP Programme Committee within the ICFP Papers-track
Frank PfenningPfenning, Frank Carnegie Mellon University, USA Structural Information Flow: A Fresh Look at Types for Non-Interference
Long PhamPham, Long Carnegie Mellon UniversityUnited States Integrating Resource Analyses via Resource Decomposition
Nguyen PhamPham, Nguyen EPFL, LAMPSwitzerland What's in the Box: Ergonomic and Expressive Capture Tracking over Generic Data Structures
Phitchaya Mangpo PhothilimthanaPhothilimthana, Phitchaya Mangpo OpenAI Mind the Abstraction Gap: Bringing Equality Saturation to Real-World ML Compilers
David PichardiePichardie, David MetaFrance 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-PharabodPichon-Pharabod, Jean Aarhus UniversityDenmark Synchronous Programming for Kids: A Manifesto
Lauren PickPick, Lauren The Chinese University of Hong Kong Checking Observational Correctness of Database Systems
Brigitte PientkaPientka, Brigitte McGill UniversityCanada McTT: A Verified Kernel for a Proof Assistant Fusing Session-Typed Concurrent Programming into Functional Programming
Benjamin C. PiercePierce, Benjamin C. University of PennsylvaniaUnited 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 PiessensPiessens, Frank KU LeuvenBelgium Software Stacks for Confidential Computing Hardware
Ruzica PiskacPiskac, Ruzica Yale UniversityUnited States Counterexample-Guided Inference of Modular Specifications Coinductive Proofs of Regular Expression Equivalence in Zero Knowledge
Goran PiskachevPiskachev, Goran Amazon Web ServicesGermany Committee Member in Program Committee within the SAS -track
Clément Pit-ClaudelPit-Claudel, Clément EPFLSwitzerland Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
André PlatzerPlatzer, André Karlsruhe Institute of Technology (KIT)Germany Adaptive Shielding via Parametric Safety Proofs
Dan PlyukhinPlyukhin, Dan University of Southern DenmarkDenmark Relax! The Semilenient Core of Choreographic Programming (Functional Pearl)
Gabriel PoesiaPoesia, Gabriel Stanford University Automated Discovery of Tactic Libraries for Interactive Theorem Proving
Nadia PolikarpovaPolikarpova, Nadia University of California at San DiegoUnited States Peepco: Batch-Based Consistency Optimization Laurel: Unblocking Automated Verification with Large Language Models
Guillermo PolitoPolito, Guillermo Univ. Lille, Inria, CNRS, Centrale Lille, UMR 9189 CRIStALFrance Committee Member in Program Committee within the SPLASH Onward! Papers-track
Thomas J. PorterPorter, Thomas J. University of MichiganUnited States Incremental Bidirectional Typing via Order Maintenance Syntactic Completions with Material Obligations
Alex PotaninPotanin, Alex Australian National UniversityAustralia 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 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 PottierPottier, François InriaFrance Formal Semantics and Program Logics for a Fragment of OCaml
Jyoti PrakashPrakash, Jyoti University of PassauGermany Committee Member in SAS Artifact Evaluation Committee within the SAS Artifact-track
Pontakorn PrasertsukPrasertsuk, Pontakorn Singapore Evolving How We Teach Memory Models
Thomas S. PricePrice, Thomas S. Carnegie Mellon UniversityUnited States Polynomial-Time Program Equivalence for Machine Knitting
Aleksandar ProkopecProkopec, Aleksandar Oracle LabsSwitzerland Heap-Snapshot Matching and Ordering using CAHPs: A Context-Augmented Heap-Path Representation for Exact and Partial Path Matching using Prefix Trees
Loïc PujetPujet, Loïc Stockholm University Type Theory in Type Theory using a Strictified Syntax
Q Yong Qi FooQi Foo, Yong National University of SingaporeSingapore Pushing the Information-Theoretic Limits of Random Access Lists
Xueying QinQin, Xueying University of Southern DenmarkDenmark Relax! The Semilenient Core of Choreographic Programming (Functional Pearl)
Xiaokang QiuQiu, Xiaokang Purdue UniversityUnited States Committee Member in Program Committee within the SAS -track
Weihao QuQu, Weihao University at Buffalo, SUNY Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Andrew QuinnQuinn, Andrew University of California at Santa CruzUnited States Scalable and Accurate Application-level Crash-Consistency Testing via Representative Testing
Benjamin QuiringQuiring, Benjamin University of Maryland at College ParkUnited States Environment-Sharing Analysis and Caller-Provided Environments for Higher-Order Languages
R Azalea RaadRaad, Azalea Imperial College LondonUnited Kingdom Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Dimi RacordonRacordon, Dimi EPFL, LAMPSwitzerland PC Member in Program Committee within the SPLASH Onward! Essays-track
Dimi RacordonRacordon, Dimi EPFLSwitzerland Existentialize your Generics
Arjun RadhakrishnaRadhakrishna, Arjun MicrosoftUnited States Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Jonathan Ragan-KelleyRagan-Kelley, Jonathan Massachusetts Institute of TechnologyUnited 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 RahmanRahman, Shanto The University of Texas at AustinUnited States UTFix: Change Aware Unit Test Repairing using LLM Understanding and Improving Flaky Test Classification
Sophie RainRain, Sophie Argot Collective Divide and Conquer: A Compositional Approach to Game-Theoretic Security
Ramya RamalingamRamalingam, Ramya University of Pennsylvania Active Learning for Neurosymbolic Program Synthesis
Arjun RameshRamesh, Arjun Carnegie Mellon University Unveiling Heisenbugs with Diversified Execution
Robert RandRand, Robert University of ChicagoUnited States Compositional Quantum Control Flow with Efficient Compilation in Qunity A Language for Quantifying Quantum Network Behavior
Francesca RandoneRandone, 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 RapoportRapoport, Marianna Amazon Web ServicesCanada Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Joseph RaskindRaskind, Joseph SUNY Binghamton Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Aseem RastogiRastogi, Aseem Microsoft ResearchIndia Automatically Verifying Replication-aware Linearizability
Savitha RaviRavi, Savitha UC San Diego An Empirical Evaluation of Property-Based Testing in Python
Michael RawsonRawson, Michael University of SouthamptonUnited Kingdom Divide and Conquer: A Compositional Approach to Game-Theoretic Security
Baishakhi RayRay, Baishakhi Columbia UniversityUnited States UTFix: Change Aware Unit Test Repairing using LLM
Patrick RedmondRedmond, Patrick University of California, Santa Cruz Exploring the Theory and Practice of Concurrency in the Entity-Component-System Pattern
John RegehrRegehr, John University of UtahUnited States PC Member in Program Committee within the SPLASH Onward! Essays-track Translation Validation for LLVM's AArch64 Backend
Baber RehmanRehman, Baber University of Hong KongHong 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 RemmalRemmal, Hamza EPFL, LAMPSwitzerland Existentialize your Generics
Alexander RepenningRepenning, Alexander University of Colorado, BoulderUnited States Committee Member in Program Committee within the SPLASH Onward! Papers-track
John ReppyReppy, John University of ChicagoUnited 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 RepsReps, Thomas University of Wisconsin-MadisonUnited 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 RezaalipourRezaalipour, Mohammad University of PassauGermany Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Jaspreet RiarRiar, Jaspreet Carnegie Mellon University Unveiling Heisenbugs with Diversified Execution
Jay RichardsRichards, Jay University of Kent Symbolic MRD: Dynamic Memory, Undefined Behaviour, and Extrinsic Choice
Manuel RiggerRigger, Manuel National University of SingaporeSingapore Flexible and Expressive Typed Path Patterns for GQL Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Talia Lily RingerRinger, Talia Lily University of Illinois Urbana-ChampaignUnited States Proof Repair across Quotient Type Equivalences
Xavier RivalRival, Xavier Inria - CNRS - Ecole Normale Superieure de Paris - PSL UniversityFrance 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 RivasRivas, Exequiel Tallinn University of Technology; Ahrefs SecRef: Securely Sharing Mutable References between Verified and Unverified Code in F
Cody RiveraRivera, Cody University of Illinois, Urbana-Champaign Checking $\delta$-Satisfiability of Reals with Integrals
Alice RixteRixte, Alice Generalizing Turtle Geometry: An Extensible Language for Vector Graphics Drawing
Neil RolnickRolnick, Neil Concert: Mirages
Tiark RompfRompf, Tiark Purdue UniversityUnited 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 RosemannRosemann, Julian Saarland University, Saarland Informatics CampusGermany Non-interference Preserving Optimising Compilation
Andrea RosàRosà, Andrea USI LuganoSwitzerland 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 RotRot, Jurriaan Radboud University Nijmegen A Unifying Approach to Product Constructions for Quantitative Temporal Inference
Anthony RoweRowe, Anthony Carnegie Mellon University Unveiling Heisenbugs with Diversified Execution
Radosław Jan RowickiRowicki, Radosław Jan Technical University of DenmarkDenmark Correct Black-Box Monitors for Distributed Deadlock Detection: Formalisation and Implementation
Craig RoyRoy, Craig Quantinuum Fulls Seldom Differ
Subhajit RoyRoy, Subhajit IIT KanpurIndia 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 RuemmerRuemmer, Philipp University of Regensburg and Uppsala UniversityGermany The Power of Regular Constraint Propagation
Neea RuschRusch, Neea United States Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Yeonhee RyouRyou, Yeonhee KAISTSouth Korea Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Sukyoung RyuRyu, Sukyoung KAISTSouth Korea Steering Committee Member in Steering Committee for SPLASH 2025 OOPSLA Review Committee Co-Chair in Organizing Committee for SPLASH 2025 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
S William S. MosesS. Moses, William University of Illinois Urbana-ChampaignUnited States Sound and Modular Activity Analysis for Automatic Differentiation in MLIR Mind the Abstraction Gap: Bringing Equality Saturation to Real-World ML Compilers
Feras SaadSaad, Feras Carnegie Mellon UniversityUnited States Integrating Resource Analyses via Resource Decomposition
Amr SabrySabry, Amr Indiana UniversityUnited States A Haskell Adiabatic DSL: Solving Classical Optimization Problems on Quantum Hardware
Hannes SaffrichSaffrich, Hannes University of Freiburg Borrowing From Session Types
Sunita SahaSaha, Sunita German Research Center for Artificial Intelligence (DFKI), Saarbrücken, Germany im2im: Automatically Converting In-Memory Image Representations using A Knowledge Graph Approach
Ayman SaidSaid, Ayman University of Michigan Scalable and Accurate Application-level Crash-Consistency Testing via Representative Testing
Kazuhiko SakaguchiSakaguchi, Kazuhiko CNRS - ENS Lyon - Université Claude Bernard Lyon 1 - LIP - UMR 5668France A Bargain for Mergesorts: How to Prove Your Mergesort Correct and Stable, Almost for Free
Ken SakayoriSakayori, Ken University of TokyoJapan Automated Catamorphism Synthesis for Solving Constrained Horn Clauses over Algebraic Data Types
Marie SalomonSalomon, Marie University of British ColumbiaCanada An Exploration of How Generative AI Affects Workflow and Collaboration in a Software Engineering Course
Michael SammlerSammler, Michael Institute of Science and Technology AustriaAustria Committee Member in ICFP Programme Committee within the ICFP Papers-track
Adrian SampsonSampson, Adrian Cornell University PC Member in Program Committee within the SPLASH Onward! Essays-track
Ashley SamuelsonSamuelson, Ashley University of Wisconsin-MadisonUnited States Choreographic Quick Changes: First-Class Location (Set) Polymorphism
David SananSanan, David Singapore Institute of TechnologySingapore A complete formal semantics of eBPF instruction set architecture for Solana
Chuta SanoSano, Chuta McGill UniversityCanada Fusing Session-Typed Concurrent Programming into Functional Programming
André L. SantosSantos, André L. University Institute of Lisbon, Portugal Committee Member in Program Commitee within the SPLASH -E-track
Yasmin Chandini SaritaSarita, Yasmin Chandini UIUC Automated Verification of Soundness of DNN Certifiers
Kartik SathyanarayananSathyanarayanan, Kartik Netflix, Inc. Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Ryosuke SatoSato, Ryosuke Tokyo University of Agriculture and TechnologyJapan Automated Catamorphism Synthesis for Solving Constrained Horn Clauses over Algebraic Data Types
Alceste ScalasScalas, Alceste Technical University of DenmarkDenmark Correct Black-Box Monitors for Distributed Deadlock Detection: Formalisation and Implementation
Ina SchaeferSchaefer, Ina KITGermany QbC: Quantum Correctness by Construction X-by-Construction: Towards Ensuring Non-Functional Properties in by-Construction Engineering
Daniel SchemmelSchemmel, Daniel Imperial College London P³: Reasoning about Patches via Product Programs
Gabriel SchererScherer, Gabriel Université Paris Cité - Inria - CNRSFrance Committee Member in ICFP Programme Committee within the ICFP Papers-track
Marko SchmellenkampSchmellenkamp, Marko Ruhr University BochumGermany Detecting and explaining (in-)equivalence of context-free grammars
Bradley SchmerlSchmerl, Bradley School of Computer Science, Carnegie Mellon University ROSpec: A Domain-Specific Language for ROS-based Robot Software
Valentin SchneebergerSchneeberger, Valentin EPFL Logically Qualified Types for Scala
Matthew SchneiderSchneider, Matthew Carnegie Mellon UniversityUnited States Debugging WebAssembly? Put some Whamm on it!
Christophe ScholliersScholliers, Christophe Universiteit Gent, Belgium MIO: Multiverse Debugging in the face of Input/Output
Tom SchrijversSchrijvers, Tom KU LeuvenBelgium Effectful Lenses: There and Back with Different Monads
Lutz SchröderSchröder, Lutz Friedrich-Alexander University Erlangen-NürnbergGermany Bialgebraic Reasoning on Stateful Languages
Michael SchröderSchröder, Michael TU WienAustria Static Inference of Regular Grammars for Ad Hoc Parsers
Manuela SchulerSchuler, 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 SchulzSchulz, Adriana University of WashingtonUnited States Polynomial-Time Program Equivalence for Machine Knitting
Philipp SchusterSchuster, Philipp University of TübingenGermany 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. ScottScott, David J. Docker, Inc. Functional Networking for Millions of Docker Desktops (Experience Report)
Remy SeassauSeassau, Remy InriaFrance Formal Semantics and Program Logics for a Fragment of OCaml
Taro SekiyamaSekiyama, Taro National Institute of InformaticsJapan On Higher-Order Model Checking of Effectful Answer-Type-Polymorphic Programs
Mazyar SerajSeraj, Mazyar Eindhoven University of TechnologyNetherlands Personalization of Programming Education: An NLP-based Bi-dimensional Classification of Programming Exercises Committee Member in Program Commitee within the SPLASH -E-track
Ilya SergeySergey, Ilya National University of SingaporeSingapore 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 SerranoSerrano, Manuel Inria; Université Côte d’AzurFrance 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. SeshiaSeshia, Sanjit A. University of California, BerkeleyUnited States Checking Observational Correctness of Database Systems
Matan ShachnaiShachnai, Matan Comparing the Precision of Abstract Operators in the eBPF Verifier using Differential Synthesis
Amir ShaikhhaShaikhha, Amir University of EdinburghUnited Kingdom Compressed and Parallelized Structured Tensor Algebra
Arindam SharmaSharma, Arindam Imperial College London P³: Reasoning about Patches via Product Programs
Dongdong SheShe, Dongdong HKUST (The Hong Kong University of Science and Technology)Hong Kong SAR China Publications Chair in Organizing Committee for SPLASH 2025
Jiasi ShenShen, 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 ShenShen, Qingchao Tianjin UniversityChina DESIL: Detecting Silent Bugs in MLIR Compiler Infrastructure
Ashley ShengSheng, Ashley Wellesley CollegeUnited States Scaling Instruction-Selection Verification against Authoritative ISA Semantics
Stephen SherrattSherratt, Stephen Tarides Software-defined declarative synthesizer live-coding in a jupyter notebook
August ShiShi, August The University of Texas at AustinUnited States Understanding and Improving Flaky Test Classification
Chenghang ShiShi, Chenghang SKLP, Institute of Computing Technology, CASChina Fast Client-Driven CFL-Reachability via Regularization-Based Graph Simplification
Chuanqi ShiShi, 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 ShiShi, Jessica University of Pennsylvania QED in Context: An Observation Study of Proof Assistant Users
Qingkai ShiShi, Qingkai Nanjing UniversityChina An Empirical Study of Bugs in the rustc Compiler
Yuanfeng ShiShi, Yuanfeng Peking UniversityChina On Abstraction Refinement for Bayesian Program Analysis
Olin ShiversShivers, Olin Northeastern UniversityUnited States Environment-Sharing Analysis and Caller-Provided Environments for Higher-Order Languages
Xujie SiSi, Xujie University of Toronto Committee Member in Program Committee within the SAS -track
Jeremy G. SiekSiek, Jeremy G. Indiana UniversityUnited States Session Chair of Gradual Typing and Security (part of ICFP Papers) Committee Member in ICFP Programme Committee within the ICFP Papers-track
Cedric SiemsSiems, Cedric Ruhr University Bochum Detecting and explaining (in-)equivalence of context-free grammars
Ho Siew FoongSiew Foong, Ho National University of SingaporeSingapore Local Arrangements Chair in Organizing Committee for SPLASH 2025
Mihaela SighireanuSighireanu, Mihaela University Paris-Saclay, ENS Paris-Saclay, CNRS, LMFFrance Steering Committee Member in Steering Committee for SPLASH 2025 Committee Member in Steering Committee within the SAS -track
Florian SihlerSihler, Florian Ulm UniversityGermany Statically Analyzing the Dataflow of R Programs Waddle: A Serious Game to Teach Writing, Reading, and Debugging Programs
Alexandra SilvaSilva, Alexandra Cornell UniversityUnited States Associate Chair in OOPSLA Review Committee within the SPLASH OOPSLA-track
Robert SimmonsSimmons, Robert IndependentUnited States Committee Member in Program Commitee within the SPLASH -E-track
Jeremy SingerSinger, Jeremy University of GlasgowUnited Kingdom Let's Take Esoteric Programming Languages Seriously
Abhishek Kr SinghSingh, Abhishek Kr IIIT HyderabadSingapore Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Avaljot SinghSingh, Avaljot UIUCUnited States Automated Verification of Soundness of DNN Certifiers
Gagandeep SinghSingh, Gagandeep University of Illinois at Urbana-Champaign; VMware ResearchUnited 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 SinghSingh, Satnam IndependentUnited States Functional Programming for Hardware Design
Somesh SinghSingh, Somesh Siemens EDAFrance Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
A. Prasad SistlaSistla, A. Prasad University of Illinois at Chicago Checking $\delta$-Satisfiability of Reals with Integrals
KC SivaramakrishnanSivaramakrishnan, KC IIT Madras and TaridesIndia 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 SivaramanSivaraman, Aishwarya Meta Synthesizing Implication Lemmas for Interactive Theorem Proving
Kugesan SivasothynathanSivasothynathan, Kugesan Jaseci Labs MTP: A Meaning-Typed Language Abstraction for AI-Integrated Programming
Dang SixuanSixuan, Dang Duke University Agora: Trust Less and Open More in Verification for Confidential Computing
Opale SjöstedtSjöstedt, Opale Imperial College London Compositional Symbolic Execution for the Next 700 Memory Models
Philipp SlusallekSlusallek, Philipp DFKI, GermanyGermany im2im: Automatically Converting In-Memory Image Representations using A Knowledge Graph Approach
Yannis SmaragdakisSmaragdakis, Yannis University of AthensGreece Universal Scalability in Declarative Program Analysis (with Choice-Based Combination Pruning)
Calvin SmithSmith, Calvin University of Texas AustinUnited States Committee Member in Review Committee within the SPLASH Student Research Competition-track
Sunbeom SoSo, Sunbeom GIST (Gwangju Institute of Science and Technology) Committee Member in Program Committee within the SAS -track
Armando Solar-LezamaSolar-Lezama, Armando Massachusetts Institute of TechnologyUnited States Peepco: Batch-Based Consistency Optimization
Dowon SongSong, Dowon Korea UniversitySouth Korea Enhancing APR with PRISM: A Semantic-Based Approach to Overfitting Patch Detection
Fu SongSong, Fu Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences; Nanjing Institute of Software TechnologyChina Verification of Bit-Flip Attacks against Quantized Neural Networks Committee Member in Program Committee within the SAS -track
Jiaxin SongSong, Jiaxin University of Illinois at Urbana-ChampaignUnited States Tabby: A Synthesis-Aided Compiler for High-Performance Zero-Knowledge Proof Circuits
Wei SongSong, Wei Nanjing University of Science and TechnologyChina DepFuzz: Efficient Smart Contract Fuzzing with Function Dependence Guidance Finding Compiler Bugs through Cross-Language Code Generator and Differential Testing
Yahui SongSong, Yahui Standard Chartered BankSingapore 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 SorensenSorensen, Tyler Microsoft Research and University of California at Santa CruzUnited 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 SossSoss, Skye University of ChicagoUnited States Environment-Sharing Analysis and Caller-Provided Environments for Higher-Order Languages
Thodoris SotiropoulosSotiropoulos, Thodoris ETH ZurichSwitzerland Validating Soundness and Completeness in Pattern-Match Coverage Analyzers
Matthew SotoudehSotoudeh, 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 SoundarapandianSoundarapandian, Vimala IIT MadrasIndia Automatically Verifying Replication-aware Linearizability
Janek SpadernaSpaderna, Janek University of Freiburg, Germany Borrowing From Session Types
Michael SperberSperber, Michael Active Group GmbHGermany PC Member in Program Committee within the SPLASH Onward! Essays-track
Arnaud SpiwackSpiwack, Arnaud TweagFrance Destination calculus: A linear λ-calculus for purely functional memory writes
Manu SridharanSridharan, Manu University of California at RiversideUnited 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 StanfordStanford, Caleb University of California, DavisUnited States Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Jonathan Lindegaard StarupStarup, Jonathan Lindegaard Denmark Qualified Types with Boolean Algebras
Fynn StebelStebel, Fynn Ruhr University Bochum Detecting and explaining (in-)equivalence of context-free grammars
Maarten SteevensSteevens, Maarten Ghent University, BelgiumBelgium MIO: Multiverse Debugging in the face of Input/Output
Leo StefanescoStefanesco, Leo University of CambridgeUnited 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 SteimannSteimann, Friedrich Fernuniversität in HagenGermany PC Member in Program Committee within the SPLASH Onward! Essays-track
Jonathan SterlingSterling, Jonathan University of CambridgeUnited Kingdom Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Michel SteuwerSteuwer, Michel Technische Universität BerlinGermany Multiple Resumptions and Local Mutable State, Directly
Sam StitesStites, Sam Northeastern UniversityUnited States Multi-Language Probabilistic Programming
Quentin StiévenartStiévenart, Quentin Université du Québec à MontréalCanada Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track Abstracting Concolic Execution for Soft Contract Verification
Filip StrömbäckStrömbäck, Filip Linköping UniversitySweden Continuations for All: Language Design Considerations for Accessible Continuations
Felix StutzStutz, 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 SuSu, Zhendong ETH ZurichSwitzerland 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 SucciSucci, Giancarlo Committee Member in Program Committee within the SPLASH Onward! Papers-track
Chamika SudusingheSudusinghe, Chamika University of Illinois at Urbana-Champaign GALA: A High Performance Graph Neural Network Acceleration LAnguage and Compiler
Tianxiang SuiSui, Tianxiang Ant Group MetaKernel: Enabling Efficient Encrypted Neural Network Inference Through Unified MVM and Convolution
Yulei SuiSui, Yulei University of New South WalesAustralia 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. SummersSummers, Alexander J. University of British ColumbiaCanada Session Chair of Rust (part of SPLASH OOPSLA) Place Capability Graphs: A General-Purpose Model of Rust’s Ownership and Borrowing Guarantees
Chengnian SunSun, Chengnian University of WaterlooCanada Boosting Program Reduction with the Missing Piece of Syntax-Guided Transformations
Jun SunSun, Jun Singapore Management UniversitySingapore 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 SunSun, Maolin Nanjing UniversityChina 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 SunSun, Yaozhu National Institute of InformaticsJapan Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track (TOPLAS) Type-Safe Compilation of Dynamic Inheritance via Merging
Vaishnavi SundararajanSundararajan, Vaishnavi IIT DelhiIndia Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Vijay SundaresanSundaresan, Vijay IBM CanadaCanada CoSSJIT: Combining Static Analysis and Speculation in JIT Compilers
Shiv SundramSundram, Shiv Stanford University REPTILE: Performant Tiling of Recurrences
Chenyao SuoSuo, Chenyao Tianjin UniversityChina DESIL: Detecting Silent Bugs in MLIR Compiler Infrastructure
Milijana SurbatovichSurbatovich, 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 SwamySwamy, Nikhil Microsoft ResearchUnited States Committee Member in ICFP Programme Committee within the ICFP Papers-track
Wouter SwierstraSwierstra, Wouter Utrecht University, NetherlandsNetherlands First-Order Laziness
Emma SöderbergSöderberg, Emma Lund UniversitySweden Committee Member in Program Committee within the SPLASH Onward! Papers-track
T Marco T MorazanT Morazan, Marco Seton Hall UniversityUnited States Derivation Visualization for Context-Free Grammar Design: Helping Students Understand Context-Free Grammars
Nicolas TabareauTabareau, Nicolas InriaFrance Incremental Certified Programming Robust Dynamic Embedding for Gradual Typing
Marcel TaeumelTaeumel, Marcel University of Potsdam; Hasso Plattner InstituteGermany 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 TakharTakhar, Gourav Indian Institute of Technology - KanpurIndia 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 TalpinTalpin, Jean-Pierre INRIA, France HpC: A Calculus for Hybrid and Mobile Systems
Gang (Gary) TanTan, Gang (Gary) Pennsylvania State UniversityUnited States Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Grace TanTan, Grace National University of Singapore Evolving How We Teach Memory Models
Guangming TanTan, Guangming Chinese Academy of Sciences(CAS) Stencil-Lifting: Hierarchical Recursive Lifting System for Extracting Summary of Stencil Kernel in Legacy Codes
Lin TanTan, Lin Purdue UniversityUnited States Show Me Why It's Correct: Saving 1/3 of Debugging Time in Program Repair with Interactive Runtime Comparison
Shangyin TanTan, Shangyin University of California, BerkeleyUnited States Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Tian TanTan, Tian Nanjing UniversityChina Two Approaches to Fast Bytecode Frontend for Static Analysis Committee Member in Program Committee within the SAS -track
Yudai TanabeTanabe, Yudai Institute of Science TokyoJapan Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Dixin TangTang, Dixin University of Texas Austin Homomorphism Calculus for User-Defined Aggregations
Lingjia TangTang, Lingjia University of Michigan MTP: A Meaning-Typed Language Abstraction for AI-Integrated Programming
Wenhao TangTang, Wenhao The University of EdinburghUnited Kingdom Modal Effect Types
Yutian TangTang, Yutian University of Glasgow, United KingdomUnited Kingdom Artemis: Toward Accurate Detection of Server-Side Request Forgeries through LLM-Assisted Inter-Procedural Path-Sensitive Taint Analysis
Swamit TannuTannu, Swamit University of Wisconsin-Madison Dependency-Aware Compilation for Surface Code Quantum Architectures Compiling Quantum Circuits
Éric TanterTanter, Éric University of ChileChile Incremental Certified Programming Robust Dynamic Embedding for Gradual Typing
Muhammad Usman TariqTariq, Muhammad Usman Stanford University REPTILE: Performant Tiling of Recurrences
Joseph TassarottiTassarotti, Joseph New York UniversityUnited States Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs
Christine TassonTasson, Christine Sorbonne Université — LIP6France Committee Member in ICFP Programme Committee within the ICFP Papers-track
Ross TateTate, Ross Independent Researcher and ConsultantUnited States Type-Outference with Label-Listeners: Foundations for Decidable Type-Consistency for Nominal Object-Oriented Generics
Mohit TekriwalTekriwal, Mohit Lawrence Livermore National LaboratoryUnited States Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Mohit TekriwalTekriwal, Mohit Lawrence Livermore National LaboratoryUnited States Committee Member in Program Committee within the SAS -track
Joshua B. TenenbaumTenenbaum, Joshua B. Massachusetts Institute of TechnologyUnited 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 TerauchiTerauchi, Tachio Waseda UniversityJapan Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Manas ThakurThakur, Manas IIT BombayIndia 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 ThalakotturThalakottur, Michelle Northeastern UniversityUnited States Student Volunteer Co-Chair in Organizing Committee for SPLASH 2025
Suhas ThalankiThalanki, Suhas Carnegie Mellon University Debugging WebAssembly? Put some Whamm on it!
Peter ThiemannThiemann, Peter University of FreiburgGermany 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ßenThießen, Thore University of Münster Porpoise: An LLM-Based Sandbox for Novices to Practice Writing Purpose Statements
Yongqiang TianTian, Yongqiang Monash UniversityHong 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 TichyTichy, Matthias Ulm UniversityGermany Statically Analyzing the Dataflow of R Programs Waddle: A Serious Game to Teach Writing, Reading, and Debugging Programs
Eli TilevichTilevich, Eli Virginia TechUnited States Committee Member in Program Commitee within the SPLASH -E-track
Amin TimanyTimany, Amin Aarhus UniversityDenmark Reasoning about Weak Isolation Levels in Separation Logic
Christopher Steven TimperleyTimperley, Christopher Steven Carnegie Mellon UniversityUnited States ROSpec: A Domain-Specific Language for ROS-based Robot Software
Frank TipTip, Frank Northeastern UniversityUnited States Steering Committee Member in Steering Committee for SPLASH 2025
Tanmay TirpankarTirpankar, Tanmay University of Utah Translation Validation for LLVM's AArch64 Backend
Ben L. TitzerTitzer, Ben L. Carnegie Mellon UniversityUnited 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 TiwariTiwari, Shrey Carnegie Mellon UniversityUnited States Fray: An Efficient General-Purpose Concurrency Testing Platform for the JVM
Ryan TjoaTjoa, Ryan University of Washington; Jane StreetUnited States Tuning Random Generators: Property-Based Testing as Probabilistic Programming
Sam Tobin-HochstadtTobin-Hochstadt, Sam Indiana UniversityUnited States ICFP 2026 Announcement
Bernardo ToninhoToninho, Bernardo NOVA-LINCS; Nova University of LisbonPortugal Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Bernardo ToninhoToninho, Bernardo Instituto Superior Técnico - University of LisbonPortugal Fusing Session-Typed Concurrent Programming into Functional Programming
Cassia TorczonTorczon, Cassia University of Pennsylvania QED in Context: An Observation Study of Proof Assistant Users
Matías ToroToro, Matías University of ChileChile 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 TrattTratt, Laurence King's College LondonUnited Kingdom Garbage Collection for Rust: The Finalizer Frontier
Christoph TreudeTreude, Christoph Singapore Management UniversitySingapore Reproducibility Debt in Scientific Software
Conan TruongTruong, Conan University of California, Irvine Towards Verifying Crash Consistency
Yi-Zhen TsaiTsai, Yi-Zhen University of California, Riverside Hambazi: Spatial Coordination Synthesis for Augmented Reality
Stelios TsampasTsampas, Stelios University of Southern DenmarkDenmark Bialgebraic Reasoning on Stateful Languages CRDT Emulation, Simulation, and Representation Independence Big Steps in Higher-Order Mathematical Operational Semantics
Ilias TsatirisTsatiris, Ilias DedaubGreece Universal Scalability in Declarative Program Analysis (with Choice-Based Combination Pruning)
Saar Tzour-ShadayTzour-Shaday, Saar Technion – Israel Institute of TechnologyIsrael Mini-Batch Robustness Verification of Deep Neural Networks
U Thien UdomsrirungruangUdomsrirungruang, Thien University of Oxford qblaze: An Efficient and Scalable Sparse Quantum Simulator
Hiroshi UnnoUnno, Hiroshi Tohoku UniversityJapan On Higher-Order Model Checking of Effectful Answer-Type-Polymorphic Programs Committee Member in ICFP Programme Committee within the ICFP Papers-track
Caterina UrbanUrban, Caterina Inria & ENS \| PSLFrance 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 UrbatUrbat, Henning Friedrich-Alexander University Erlangen-NürnbergGermany Session Chair of Semantics (part of ICFP Papers) Bialgebraic Reasoning on Stateful Languages
V Jan VahrenholdVahrenhold, Jan University of MünsterGermany Porpoise: An LLM-Based Sandbox for Novices to Practice Writing Purpose Statements
Nachiappan ValliappanValliappan, Nachiappan University of EdinburghUnited Kingdom Committee Member in ICFP Programme Committee within the ICFP Papers-track
Milla ValnetValnet, Milla Sorbonne UniversitéFrance Committee Member in SAS Artifact Evaluation Committee within the SAS Artifact-track
Isaac van Bakelvan Bakel, Isaac ETH ZurichSwitzerland Modular Reasoning about Global Variables and Their Initialization
Mark van den Brandvan den Brand, Mark Eindhoven University of TechnologyNetherlands Personalization of Programming Education: An NLP-based Bi-dimensional Classification of Programming Exercises
Guy Van den BroeckVan den Broeck, Guy University of California at Los Angeles Tuning Random Generators: Property-Based Testing as Probabilistic Programming
Andre van der Hoekvan der Hoek, Andre University of California, IrvineUnited States PC Member in Program Committee within the SPLASH Onward! Essays-track
Tijs van der Stormvan der Storm, Tijs CWI & University of GroningenNetherlands 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 EsVan Es, Noah Sofware Languages Lab, Vrije Universiteit BrusselBelgium Delta Store Semantics: Abstract Garbage Collection for Abstract Definitional Interpreters Monarch: A Modular Framework for Abstract Definitional Interpreters in Haskell
Jacob Van GeffenVan Geffen, Jacob Veridise Inc. Scalable and Accurate Application-level Crash-Consistency Testing via Representative Testing
Eric Van WykVan Wyk, Eric University of Minnesota, Twin CitiesUnited States Steering Committee Member in Steering Committee for SPLASH 2025
Bram VandenbogaerdeVandenbogaerde, Bram Software Languages Lab, Vrije Universiteit BrusselBelgium 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 VandeputteVandeputte, Frederik Nokia Bell Labs Foundational Design Principles and Patterns for Building Robust & Adaptive GenAI-Native Systems
Sushen VangeepuramVangeepuram, Sushen Iowa State University Embedding Quantum Program Verification into Dafny
Alexa VanHattumVanHattum, Alexa Wellesley CollegeUnited States Scaling Instruction-Selection Verification against Authoritative ISA Semantics
Vasco T. VasconcelosVasconcelos, Vasco T. LASIGE, University of LisbonPortugal Steering Committee Member in Steering Committee for SPLASH 2025 Steering Committee Member in Onward! Steering Committee within the SPLASH Onward! Essays-track Session Chair of Verification 2 (part of SPLASH OOPSLA) 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 VechevVechev, Martin ETH ZurichSwitzerland qblaze: An Efficient and Scalable Sparse Quantum Simulator
Jyothi VeduradaVedurada, Jyothi IIT HyderabadIndia Committee Member in Review Committee within the SPLASH Student Research Competition-track
Andreas VenerisVeneris, Andreas University of TorontoCanada HEMVM: a Heterogeneous Blockchain Framework for Interoperable Virtual Machines
Hristo VenevVenev, Hristo INSAIT, Sofia University "St. Kliment Ohridski"Bulgaria qblaze: An Efficient and Scalable Sparse Quantum Simulator
Sarah VerbelenVerbelen, Sarah Vrije Universiteit Brussel, Belgium Monarch: A Modular Framework for Abstract Definitional Interpreters in Haskell
Vasudev VikramVikram, Vasudev Carnegie Mellon UniversityUnited States Fray: An Efficient General-Purpose Concurrency Testing Platform for the JVM
Polina VinogradovaVinogradova, Polina Restoring Data Sovereignty: A Human-Centered Approach Blockchain Health Technology
Cosmo ViolaViola, Cosmo University of Illinois Urbana-Champaign Proof Repair across Quotient Type Equivalences
Harishankar VishwanathanVishwanathan, Harishankar Comparing the Precision of Abstract Operators in the eBPF Verifier using Differential Synthesis
Mahesh ViswanathanViswanathan, Mahesh University of Illinois at Urbana-ChampaignUnited States Checking $\delta$-Satisfiability of Reals with Integrals
Jan VitekVitek, Jan Northeastern UniversityUnited States Steering Committee Chair in Steering Committee for SPLASH 2025
Yakir VizelVizel, Yakir Technion—Israel Institute of TechnologyIsrael Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Arya VohraVohra, Arya University of Chicago Mind the Abstraction Gap: Bringing Equality Saturation to Real-World ML Compilers
Finn VoichickVoichick, Finn University of MarylandUnited States Compositional Quantum Control Flow with Efficient Compilation in Qunity
David VoigtVoigt, 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
W Philip WadlerWadler, Philip IOG; University of EdinburghUnited 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 WagnerWagner, Andrew Northeastern UniversityUnited States From Linearity to Borrowing
Gijs WalravensWalravens, Gijs Eindhoven University of Technology Personalization of Programming Education: An NLP-based Bi-dimensional Classification of Programming Exercises
Michael WalterWalter, Michael Ruhr-Universität Bochum QbC: Quantum Correctness by Construction
Bo WangWang, Bo Beijing Jiaotong UniversityChina Fuzzing C++ Compilers via Type-Driven Mutation
Chao WangWang, Chao University of Southern CaliforniaUnited States Probabilistic Inference for Datalog with Correlated Inputs
Claire WangWang, Claire University of Pennsylvania Rocq N'Roll Concert: RocqNRoll
Di WangWang, Di Peking UniversityChina Automatic Linear Resource Bound Analysis for Rust via Prophecy Potentials
Hanzhang WangWang, Hanzhang Fudan University, ChinaChina JavART: a Lightweight Rule-Based JIT Compiler Using Translation Rules Extracted from a Learning Approach
Jianrong WangWang, Jianrong Tianjin UniversityChina DESIL: Detecting Silent Bugs in MLIR Compiler Infrastructure
Jiawei WangWang, Jiawei UNSW Efficient Abstract Interpretation via Selective Widening
Jingbo WangWang, Jingbo Purdue University Probabilistic Inference for Datalog with Correlated Inputs
Ke WangWang, Ke Peking University Synchronized Behavior Checking: A Method for Finding Missed Compiler Optimizations
Linzhang WangWang, Linzhang Nanjing University Synchronized Behavior Checking: A Method for Finding Missed Compiler Optimizations
Peixin WangWang, Peixin East China Normal University Structural Abstraction and Refinement for Probabilistic Programs
Ruixin WangWang, Ruixin Purdue UniversityUnited States Show Me Why It's Correct: Saving 1/3 of Debugging Time in Program Repair with Interactive Runtime Comparison
Shengyi WangWang, Shengyi Princeton UniversityUnited States Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Shiqi WangWang, Shiqi AWS AI LabsUnited States UTFix: Change Aware Unit Test Repairing using LLM
Shuai WangWang, Shuai Hong Kong University of Science and TechnologyChina 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 WangWang, Shuling Institute of Software, Chinese Academy of Sciences HpC: A Calculus for Hybrid and Mobile Systems
Wenwen WangWang, Wenwen University of GeorgiaUnited States JavART: a Lightweight Rule-Based JIT Compiler Using Translation Rules Extracted from a Learning Approach
Wenxi WangWang, Wenxi University of VirginaUnited States Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
XiaoFeng WangWang, XiaoFeng Nanyang Technological University Agora: Trust Less and Open More in Verification for Confidential Computing
Xinyu WangWang, Xinyu University of MichiganUnited States Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Yongjia WangWang, Yongjia College of Intelligence and Computing, Tianjin University DESIL: Detecting Silent Bugs in MLIR Compiler Infrastructure
Yongzhi WangWang, Yongzhi Xidian University HybridPersist: A Compiler Support for User-Friendly and Efficient PM Programming
Yu WangWang, Yu Nanjing UniversityChina Synchronized Behavior Checking: A Method for Finding Missed Compiler Optimizations
Yuepeng WangWang, Yuepeng Simon Fraser UniversityCanada Committee Member in Program Committee within the SAS -track
Yuning WangWang, Yuning Rutgers University Abstraction Refinement-guided Program Synthesis for Robot Learning from Demonstrations
Zhuangda WangWang, Zhuangda Xiamen UniversityChina TailTracer: Continuous Tail Tracing for Production Use
Zihan WangWang, Zihan The University of Queensland and CSIRO's Data61Australia Convex Hull Approximation for Activation Functions
Ziteng WangWang, Ziteng University of Texas at AustinUnited States Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track Homomorphism Calculus for User-Defined Aggregations
Kazuki WatanabeWatanabe, Kazuki National Institute of Informatics; SOKENDAIJapan A Unifying Approach to Product Constructions for Quantitative Temporal Inference
Conrad WattWatt, Conrad Nanyang Technological UniversitySingapore 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 WattWatt, Joe *Institute for Infocomm Research, ASTARSingapore** Student Volunteer Co-Chair in Organizing Committee for SPLASH 2025
Tan Wei HanWei Han, Tan Local Arrangements Chair in Organizing Committee for SPLASH 2025
Anjiang WeiWei, Anjiang Stanford UniversityUnited States Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Guannan WeiWei, Guannan Tufts UniversityUnited 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 WeiWei, Ivan University of Michigan Incremental Bidirectional Typing via Order Maintenance
Stephanie WeirichWeirich, Stephanie University of PennsylvaniaUnited States Committee Member in ICFP Programme Committee within the ICFP Papers-track
Hongbo WenWen, Hongbo University of California, Santa Barbara & Riema Labs Tabby: A Synthesis-Aided Compiler for High-Performance Zero-Knowledge Proof Circuits
Zhongzhen WenWen, Zhongzhen Nanjing UniversityChina PReMM: LLM-Based Program Repair for Multi-Method Bugs via Divide and Conquer
Sam WestrickWestrick, Sam New York UniversityUnited States Committee Member in Program Committee within the SPLASH FARM-track
Leo WhiteWhite, Leo Jane StreetUnited Kingdom Modal Effect Types Committee Member in ICFP Programme Committee within the ICFP Papers-track
John WickersonWickerson, John Imperial College LondonUnited Kingdom Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Thomas WiesWies, Thomas New York UniversityUnited States Abstract Interpretation of Temporal Safety Effects of Higher Order Programs Characterizing Implementability of Global Protocols with Infinite States and Data
Graham WilliamsWilliams, Graham Australian National University Reproducibility Debt in Scientific Software
Richard WillieWillie, Richard National University of Singapore View Types in Rust
Christian WimmerWimmer, Christian Amazon Web ServicesUnited States Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Tobias WinklerWinkler, Tobias RWTH Aachen UniversityGermany Foundations for Deductive Verification of Continuous Probabilistic Programs: From Lebesgue to Riemann and Back
Daniel Winograd-CortWinograd-Cort, Daniel Nectry Inc.United States Sponsorship Co-Chair in Organizing Committee for SPLASH 2025
Théo WinterhalterWinterhalter, Théo INRIAFrance SecRef: Securely Sharing Mutable References between Verified and Unverified Code in F Committee Member in ICFP Programme Committee within the ICFP Papers-track
Jaeyeon WonWon, Jaeyeon MIT The Continuous Tensor Abstraction: Where Indices are Real
Jotham WongWong, Jotham National University of Singapore, SingaporeSingapore Evolving How We Teach Memory Models
Wai Kin WongWong, Wai Kin Hong Kong University of Science and Technology Extraction and Mutation at a High Level: Template-Based Fuzzing for JavaScript Engines
Daniel WrightWright, Daniel University of Surrey Symbolic MRD: Dynamic Memory, Undefined Behaviour, and Extrinsic Choice
Tobias WrigstadWrigstad, Tobias Uppsala UniversitySweden Associate Chair in OOPSLA Review Committee within the SPLASH OOPSLA-track
Daoyuan WuWu, Daoyuan Lingnan UniversityHong 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 WuWu, Jiangchang State Key Laboratory for Novel Software Technology, Nanjing University Validating SMT Rewriters via Rewrite Space Exploration Supported by Generative Equality Saturation
Ming WuWu, Ming Shanghai Tree-Graph Blockchain Research Institute HEMVM: a Heterogeneous Blockchain Framework for Interoperable Virtual Machines
Rongxin WuWu, Rongxin Xiamen UniversityChina TailTracer: Continuous Tail Tracing for Production Use
Shushu WuWu, Shushu Shanghai Jiao Tong University Encode the $\forall\exists$ Relational Hoare Logic into Standard Hoare Logic
Xiwei WuWu, Xiwei Shanghai Jiao Tong UniversityChina Encode the $\forall\exists$ Relational Hoare Logic into Standard Hoare Logic
X Dongwei XiaoXiao, Dongwei Hong Kong University of Science and TechnologyHong 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 XiaoXiao, Junmin Stencil-Lifting: Hierarchical Recursive Lifting System for Extracting Summary of Stencil Kernel in Legacy Codes
Linjie XiaoXiao, Linjie Ant Group MetaKernel: Enabling Efficient Encrypted Neural Network Inference Through Unified MVM and Convolution
Linna XieXie, Linna Nanjing UniversityChina PReMM: LLM-Based Program Repair for Multi-Method Bugs via Divide and Conquer
Ningning XieXie, Ningning University of TorontoCanada Multi-stage Programming with Splice Variables Committee Member in ICFP Programme Committee within the ICFP Papers-track
Ruifeng XieXie, Ruifeng Peking University Effectful Lenses: There and Back with Different Monads
Zifan XieXie, Zifan Huazhong University of Science and TechnologyChina Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Jimmy XinXin, Jimmy The University of Texas at Austin Automated Discovery of Tactic Libraries for Interactive Theorem Proving
Yutong XinXin, Yutong The University of Texas at Austin Automated Discovery of Tactic Libraries for Interactive Theorem Proving
Chris XiongXiong, Chris Ohio State University Carapace: Static–Dynamic Information Flow Control in Rust
Yingfei XiongXiong, Yingfei Peking UniversityChina Session Chair of Synthesis 1 (part of SPLASH OOPSLA) Tunneling Through the Hill: Multi-Way Intersection for Version-Space Algebras in Program Synthesis
Amanda XuXu, 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 XuXu, Baowen Nanjing University An Empirical Study of Bugs in the rustc Compiler
Han XuXu, Han Princeton UniversityUnited States Liberating Merges via Apartness and Guarded Subtyping
Jiexiao XuXu, Jiexiao University of Washington Scalable and Accurate Application-level Crash-Consistency Testing via Representative Testing
Xiangzhe XuXu, Xiangzhe Purdue UniversityUnited 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 XuXu, Xiong Institute of Software, Chinese Academy of Sciences HpC: A Calculus for Hybrid and Mobile Systems
Yichen XuXu, Yichen EPFL What's in the Box: Ergonomic and Expressive Capture Tracking over Generic Data Structures
Zhenyang XuXu, Zhenyang University of WaterlooCanada Boosting Program Reduction with the Missing Piece of Syntax-Guided Transformations
Jingling XueXue, Jingling University of New South WalesAustralia Fast Client-Driven CFL-Reachability via Regularization-Based Graph Simplification MetaKernel: Enabling Efficient Encrypted Neural Network Inference Through Unified MVM and Convolution
Runze XueXue, Runze University of Michigan; University of Cambridge; Indiana UniversityUnited States Notions of Stack-manipulating Computation and Relative Monads
Xu XueXue, Xu The University of Hong Kong Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Y Berk YagliYagli, Berk Concert: False Awakening on a Mediterranean Island
Jeremy YallopYallop, Jeremy University of CambridgeUnited Kingdom Frex: Dependently Typed Algebraic Simplification
Zhenyu YanYan, Zhenyu Peking UniversityChina Committee Member in SAS Artifact Evaluation Committee within the SAS Artifact-track
Chenyuan YangYang, Chenyuan University of Illinois Urbana-ChampaignUnited States AutoVerus: Automated Proof Generation for Rust Code
Fan YangYang, Fan Microsoft Research Asia AutoVerus: Automated Proof Generation for Rust Code
Min YangYang, Min Fudan UniversityChina ApkDiffer: Accurate and Scalable Cross-Version Diffing Analysis for Android Applications
Minghui YangYang, Minghui OPPO ApkDiffer: Accurate and Scalable Cross-Version Diffing Analysis for Android Applications
Sen YangYang, Sen Yale University Agora: Trust Less and Open More in Verification for Confidential Computing
Shengyuan YangYang, Shengyuan University of Wisconsin-Madison Committee Member in SAS Artifact Evaluation Committee within the SAS Artifact-track
Yibiao YangYang, Yibiao Nanjing UniversityChina Validating SMT Rewriters via Rewrite Space Exploration Supported by Generative Equality Saturation
Yixin YangYang, Yixin Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Ziyi YangYang, Ziyi National University of SingaporeSingapore Inductive Synthesis of Inductive Heap Predicates
Jianan YaoYao, Jianan University of Toronto AutoVerus: Automated Proof Generation for Rust Code
Peisen YaoYao, Peisen Zhejiang UniversityChina 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 YeYe, Wenjia National University of SingaporeSingapore Flexible and Expressive Typed Path Patterns for GQL
Pen-Chung YewYew, Pen-Chung University of Minnesota at Twin CitiesUnited States JavART: a Lightweight Rule-Based JIT Compiler Using Translation Rules Extracted from a Learning Approach
Jooyong YiYi, Jooyong UNISTSouth Korea Committee Member in Program Committee within the SAS -track
Kwangkeun YiYi, Kwangkeun Seoul National University React-tRace: A Semantics for Understanding React Hooks
Xizhe YinYin, Xizhe Nanjing UniversityChina An Empirical Study of Bugs in the rustc Compiler
Irene YoonYoon, Irene InriaFrance Formal Semantics and Program Logics for a Fragment of OCaml Committee Member in ICFP Programme Committee within the ICFP Papers-track
Taeyoung YoonYoon, Taeyoung Seoul National University Lilo: A Higher-Order, Relational Concurrent Separation Logic for Liveness
Nobuko YoshidaYoshida, Nobuko University of OxfordUnited Kingdom Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Shu-Hung YouYou, Shu-Hung Institute of Information Science, Academia Sinica, TaiwanTaiwan Contract System Metatheories à la Carte: A Transition-System View of Contracts
David YoungYoung, David University of Kansas, USA A Haskell Adiabatic DSL: Solving Classical Optimization Problems on Quantum Hardware
Neringa YoungYoung, Neringa Lithuania SIGPLAN Conference Manager in Organizing Committee for SPLASH 2025
Nengkun YuYu, Nengkun Stony Brook University, USAUnited States Scalable Equivalence Checking and Verification of Shallow Quantum Circuits
Liang YuanYuan, Liang Chinese Academy of Sciences Stencil-Lifting: Hierarchical Recursive Lifting System for Extracting Summary of Stencil Kernel in Legacy Codes
Peng YuanYuan, Peng Ant Group MetaKernel: Enabling Efficient Encrypted Neural Network Inference Through Unified MVM and Convolution
Shenghao YuanYuan, Shenghao Zhejiang University A complete formal semantics of eBPF instruction set architecture for Solana
Yongwei YuanYuan, Yongwei Purdue UniversityUnited States Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Yueming YuanYuan, Yueming University of Illinois Urbana-Champaign SPLAT: A framework for optimised GPU code-generation for SParse reguLar ATtention
Zhou YuanyuanYuanyuan, Zhou UCSD On the Impact of Formal Verification on Software Development Laurel: Unblocking Automated Verification with Large Language Models
Insu YunYun, Insu KAIST Bridging the Gap between Real-World and Formal Binary Lifting through Filtered-Simulation
Tom YuvilerYuviler, Tom Technion Enhancing Neural Network Robustness via Synthesis of Repair Programs
Z Enea ZaffanellaZaffanella, Enea University of ParmaItaly Committee Member in Program Committee within the SAS -track
Yannick ZakowskiZakowski, Yannick InriaFrance Structural temporal logic for mechanized program verification Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Giacomo ZanattaZanatta, Giacomo Ca’ Foscari University of VeniceItaly Committee Member in SAS Artifact Evaluation Committee within the SAS Artifact-track
Lucas ZavaliaZavalia, Lucas Florida State University TallahasseeUnited States A Flow-Sensitive Refinement Type System for Verifying eBPF Programs
Steve ZdancewicZdancewic, Steve University of PennsylvaniaUnited States Opportunistically Parallel Lambda Calculus Structural temporal logic for mechanized program verification
Stefan ZetzscheZetzsche, Stefan AmazonUnited Kingdom Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Thomas ZeumeZeume, Thomas Ruhr University BochumGermany Detecting and explaining (in-)equivalence of context-free grammars
Bohua ZhanZhan, Bohua Huawei Technologies Co., Ltd. HpC: A Calculus for Hybrid and Mobile Systems
Naijun ZhanZhan, Naijun Peking University HpC: A Calculus for Hybrid and Mobile Systems
Chaoyue ZhangZhang, Chaoyue Nanjing UniversityChina Towards a Theoretically-Backed and Practical Framework for Selective Object-Sensitive Pointer Analysis
Charles ZhangZhang, Charles The Hong Kong University of Science and TechnologyChina Steering Committee Member in Steering Committee for SPLASH 2025 General Chair in Organizing Committee for SPLASH 2025 Session Chair of TOPLAS and Remote (part of SPLASH OOPSLA) SPLASH Awards General Chair Report
Cheng ZhangZhang, Cheng Worcester Polytechnic InstituteUnited States Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Chengyu ZhangZhang, Chengyu ETH Zurich Validating Soundness and Completeness in Pattern-Match Coverage Analyzers
Danfeng ZhangZhang, Danfeng Duke UniversityUnited States Agora: Trust Less and Open More in Verification for Confidential Computing
Fan ZhangZhang, Fan Yale University Agora: Trust Less and Open More in Verification for Confidential Computing
Jialu ZhangZhang, Jialu University of WaterlooCanada Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Mengxiao ZhangZhang, Mengxiao Boosting Program Reduction with the Missing Piece of Syntax-Guided Transformations
Nuda ZhangZhang, Nuda University of Michigan Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Qirun ZhangZhang, Qirun Georgia Institute of TechnologyUnited 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 ZhangZhang, Ruihan Singapore Management University (SMU) Correct-By-Construction: Certified Individual Fairness through Neural Network Training
Shuhao ZhangZhang, Shuhao Peking UniversityChina Tunneling Through the Hill: Multi-Way Intersection for Version-Space Algebras in Program Synthesis
Teng ZhangZhang, Teng Nanjing UniversityChina Committee Member in SAS Artifact Evaluation Committee within the SAS Artifact-track
Tian ZhangZhang, Tian Nanjing UniversityChina PReMM: LLM-Based Program Repair for Multi-Method Bugs via Divide and Conquer
Tianyi ZhangZhang, Tianyi Purdue UniversityUnited States Show Me Why It's Correct: Saving 1/3 of Debugging Time in Program Repair with Interactive Runtime Comparison
Weihua ZhangZhang, Weihua Fudan UniversityChina JavART: a Lightweight Rule-Based JIT Compiler Using Translation Rules Extracted from a Learning Approach
Wenmeng ZhangZhang, Wenmeng College of Computer Science and Technology, National University of Defense Technology, Changsha, China Multi-Modal Sketch-based Behavior Tree Synthesis
Xiangyu ZhangZhang, Xiangyu Purdue UniversityUnited States Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Xiaojing ZhangZhang, Xiaojing Ant Group MetaKernel: Enabling Efficient Encrypted Neural Network Inference Through Unified MVM and Convolution
Xin ZhangZhang, Xin Peking UniversityChina 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 ZhangZhang, Xing Peking UniversityChina Fuzzing C++ Compilers via Type-Driven Mutation
Yedi ZhangZhang, Yedi National University of Singapore Verification of Bit-Flip Attacks against Quantized Neural Networks
Yi ZhangZhang, Yi Nanjing UniversityChina Synchronized Behavior Checking: A Method for Finding Missed Compiler Optimizations
Yifan ZhangZhang, Yifan Peking UniversityChina On Abstraction Refinement for Bayesian Program Analysis
Ying ZhangZhang, Ying Wake Forest UniversityUnited States Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Yiyu ZhangZhang, Yiyu Nanjing UniversityChina HybridPersist: A Compiler Support for User-Friendly and Efficient PM Programming TailTracer: Continuous Tail Tracing for Production Use
Yizhou ZhangZhang, Yizhou University of WaterlooCanada Zero-Overhead Lexical Effect Handlers Compiling with Generating Functions
Yuan ZhangZhang, Yuan Fudan UniversityChina ApkDiffer: Accurate and Scalable Cross-Version Diffing Analysis for Android Applications
Zhaoyang ZhangZhang, Zhaoyang The Hong Kong University of Science and Technology A Sound Static Analysis Approach to I/O API Migration
Zhuoruo ZhangZhang, Zhuoruo Zhejiang University A complete formal semantics of eBPF instruction set architecture for Solana
Ziqi ZhangZhang, Ziqi University of Illinois Urbana-ChampaignChina Orax: A Feedback-Driven Framework for Efficiently Solving Satisfiability Modulo Theories and Oracles
Pinhan ZhaoZhao, Pinhan University of MichiganUnited States Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Wenyu ZhaoZhao, Wenyu Australian National UniversityAustralia 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 ZhaoZhao, Yongwang Zhejiang University A complete formal semantics of eBPF instruction set architecture for Solana
Yubo ZhaoZhao, Yubo Shanghai Jiao Tong University Binary Cryptographic Function Identification via Similarity Analysis with Path-insensitive Emulation
Zhongkai ZhaoZhao, 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 ZhengZheng, Junda Bounded-Exhaustive Subspace Diversification for SMT Solver Testing
Linus ZhengZheng, Linus University of Texas at Austin Homomorphism Calculus for User-Defined Aggregations
Xusheng ZhiZhi, Xusheng University of Wisconsin-MadisonUnited States (TOPLAS) Polynomial Bounds of CFLOBDDs against BDDs
Byron ZhongZhong, Byron University of ChicagoUnited States Environment-Sharing Analysis and Caller-Provided Environments for Higher-Order Languages
Sizhe ZhongZhong, Sizhe The Hong Kong University of Science and Technology A Sound Static Analysis Approach to I/O API Migration
Zhineng ZhongZhong, 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 ZhouZhou, Diyu Peking University A Sound Static Analysis Approach to I/O API Migration
Litao ZhouZhou, Litao University of Hong KongChina Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Quan ZhouZhou, Quan Penn State University Agora: Trust Less and Open More in Verification for Confidential Computing
Xiangyu ZhouZhou, Xiangyu University of Michigan Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Yanqi ZhouZhou, Yanqi Google SPLAT: A framework for optimised GPU code-generation for SParse reguLar ATtention
Yuming ZhouZhou, Yuming Nanjing UniversityChina Validating SMT Rewriters via Rewrite Space Exploration Supported by Generative Equality Saturation
Zhe ZhouZhou, Zhe Purdue University We’ve Got You Covered: Type-Guided Repair of Incomplete Input Generators
Zhichao ZhouZhou, Zhichao School of Information Science and Technology, ShanghaiTech UniversityChina Artemis: Toward Accurate Detection of Server-Side Request Forgeries through LLM-Assisted Inter-Procedural Path-Sensitive Taint Analysis
Ziqiao ZhouZhou, Ziqiao Microsoft ResearchUnited States AutoVerus: Automated Proof Generation for Rust Code
He ZhuZhu, He Rutgers University, USA Abstraction Refinement-guided Program Synthesis for Robot Learning from Demonstrations
Jun ZhuZhu, Jun Nankai University Adaptive Shielding via Parametric Safety Proofs
Qing ZhuZhu, Qing Ant Group MetaKernel: Enabling Efficient Encrypted Neural Network Inference Through Unified MVM and Convolution
Siyuan ZhuZhu, Siyuan Peking University, China Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Oleksandr ZinenkoZinenko, 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 ZongjieZongjie, Li Hong Kong University of Science and TechnologyChina API-guided Dataset Synthesis to Finetune Large Code Models
Damien ZuffereyZufferey, Damien SonarSourceSwitzerland Characterizing Implementability of Global Protocols with Infinite States and Data
Zhiqiang ZuoZuo, Zhiqiang Nanjing UniversityChina HybridPersist: A Compiler Support for User-Friendly and Efficient PM Programming TailTracer: Continuous Tail Tracing for Production Use
Aron ZwaanZwaan, Aron Delft University of TechnologyNetherlands Language-Parametric Reference Synthesis
Š Artjoms ŠinkarovsŠinkarovs, Artjoms University of Southampton Correctness Meets Performance: From Agda to Futhark

SPLASH 2025 Contributors

Results (1384)

Tracks

ICFP/SPLASH 2025

Co-hosted Conferences

Workshops

Co-hosted Symposia