SPLASH 2025 Contributors

Filter

Role Type

Contributing to

Number of Roles

Country

Results (1185)

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
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
Amal AhmedAhmed, Amal Northeastern University, USAUnited States Steering Committee Member in Steering Committee for SPLASH 2025 From Linearity to Borrowing Committee Member in Program Committee and Panel within the SPLASH Doctoral Symposium-track
Joongwon AhnAhn, Joongwon Seoul National University React-tRace: A Semantics for Understanding React Hooks
Willow AhrensAhrens, Willow Massachusetts Institute of TechnologyUnited States The Continuous Tensor Abstraction: Where Indices are Real Finch: Sparse and Structured Tensor Programming with Control Flow
Marat AkhinAkhin, Marat JetBrainsNetherlands Finding Compiler Bugs through Cross-Language Code Generator and Differential Testing
Aws AlbarghouthiAlbarghouthi, Aws University of Wisconsin-MadisonUnited States Checking Observational Correctness of Database Systems Dependency-Aware Compilation for Surface Code Quantum Architectures
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 Committee Member in ICFP Programme Committee within the ICFP Papers-track
Henry AllardAllard, Henry Iowa State UniversityUnited States Embedding Quantum Program Verification into Dafny
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 The Continuous Tensor Abstraction: Where Indices are Real Finch: Sparse and Structured Tensor Programming with Control Flow
Nada AminAmin, Nada Harvard UniversityUnited States Committee Member in ICFP Programme Committee within the ICFP Papers-track
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
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
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
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
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 Metamorph: Synthesizing Large Objects from Dafny Specifications Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Alexander Y. BaiBai, Alexander Y. MPI-SWS Debugging WebAssembly? Put some Whamm on it!
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
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) Heap-Snapshot Matching and Ordering using CAHPs: A Context-Augmented Heap-Path Representation for Exact and Partial Path Matching using Prefix Trees HeapBuffers: Why not just using a binary serialization format for your managed memory?
Osbert BastaniBastani, Osbert University of PennsylvaniaUnited States Active Learning for Neurosymbolic Program Synthesis Opportunistically Parallel Lambda Calculus
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 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
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
Jean-Philippe BernardyBernardy, Jean-Philippe University of Gothenburg, Sweden Committee Member in ICFP Programme Committee within the ICFP Papers-track
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 Interactive Bit Vector Reasoning using Verified Bitblasting Certified Decision Procedures for Width-Independent Bitvector Predicates
Bishnu BhusalBhusal, Bishnu University of MissouriNepal Checking ?-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
Walter BinderBinder, Walter USI LuganoSwitzerland Heap-Snapshot Matching and Ordering using CAHPs: A Context-Augmented Heap-Path Representation for Exact and Partial Path Matching using Prefix Trees HeapBuffers: Why not just using a binary serialization format for your managed memory?
Stephen M. BlackburnBlackburn, Stephen M. Google; Australian National UniversityAustralia Work Packets: A New Abstraction for GC Software Engineering, Optimization, and Innovation Advancing Performance via a Systematic Application of Research and Industrial Best Practice
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
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?
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
Wavid BowmanBowman, Wavid University of FloridaUnited States Debugging WebAssembly? Put some Whamm on it!
William J. BowmanBowman, William J. University of British ColumbiaCanada Type-Preserving Flat Closure Optimization PC Member in Program Committee within the SPLASH Onward! Essays-track Committee Member in ICFP Programme Committee within the ICFP Papers-track
Jonathan Immanuel BrachthäuserBrachthäuser, Jonathan Immanuel University of TübingenGermany Compiling Classical Sequent Calculus to Stock Hardware: The Duality of Compilation The Simple Essence of Monomorphization Dynamic Wind for Effect Handlers The Simple Essence of Overloading: Making ad-hoc polymorphism more algebraic with flow-based variational type-checking Tracing Just-in-time Compilation for Effects and Handlers Committee Member in ICFP Programme Committee within the ICFP Papers-track
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 Texas at AustinUnited States Synthesizing Implication Lemmas for Interactive Theorem Proving
Mitch BrilesBriles, Mitch University of Utah Translation Validation for LLVM's AArch64 Backend
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 Pennsylvania Demo: 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
Aurel BílýBílý, Aurel ETH Zurich A Refinement Methodology for Distributed Programs in Rust Place Capability Graphs: A General-Purpose Model of Rust’s Ownership and Borrowing Guarantees
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
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 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
Jacques CaretteCarette, Jacques McMaster UniversityCanada Committee Member in Program Committee within the SPLASH Onward! Papers-track
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
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 ?-Satisfiability of Reals with Integrals
Kartik ChandraChandra, Kartik MITUnited States A Domain-Specific Probabilistic Programming Language for Reasoning about Reasoning (or: a memo on memo) Gauguin, Descartes, Bayes: A Diurnal Golem's Brain
Bor-Yuh Evan ChangChang, Bor-Yuh Evan University of Colorado Boulder & AmazonUnited States Steering Committee Member in Steering Committee for SPLASH 2025 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 Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Fei ChenChen, Fei 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 Spatial Coordination Synthesis for Augmented Reality
Jocelyn Qiaochu ChenChen, Jocelyn Qiaochu New York University, University of AlbertaUnited States Active Learning for Neurosymbolic Program Synthesis Automated Discovery of Tactic Libraries for Interactive Theorem Proving
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
Alvin CheungCheung, Alvin University of California at BerkeleyUnited States Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Michele ChiariChiari, Michele TU WienAustria Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Shigeru ChibaChiba, Shigeru University of TokyoJapan 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 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 Northeastern UniversityUnited States Scaling Optimization Over Uncertainty via Compilation
Joonwon ChoiChoi, Joonwon Amazon Web ServicesUnited States Revamping Verilog Semantics for Foundational Verification
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
Christopher ClarkeClarke, Christopher University of Michigan Meaning-Typed Programming: Language Abstraction and Runtime for Model-Integrated Applications
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 RestPi: Path-Sensitive Type Inference for REST APIs An Empirical Evaluation of Property-Based Testing On the Impact of Formal Verification on Software Development PC Member in Program Committee within the SPLASH Onward! Essays-track
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
Sam CohenCohen, Sam University of Chicago Code Style Sheets: CSS for Code
Simon CookseyCooksey, Simon Symbolic MRD: Dynamic Memory, Undefined Behaviour, and Extrinsic Choice
Lucas C. CordeiroCordeiro, Lucas C. University of Manchester, UKUnited Kingdom Committee Member in Program Committee within the SAS -track
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
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 Semantics of Sets of Programs LOUD: Synthesizing Strongest and Weakest Specifications Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Francesco DagninoDagnino, Francesco Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
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 L. DantanarayanaDantanarayana, Jayanaka L. University of Michigan Meaning-Typed Programming: Language Abstraction and Runtime for Model-Integrated Applications
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
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 Delta Store Semantics: Abstract Garbage Collection for Abstract Definitional Interpreters Monarch: A Modular Framework for Abstract Definitional Interpreters in Haskell Abstracting Concolic Execution for Soft Contract Verification
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 PC Chair in ICFP Programme Committee within the ICFP Papers-track
Samvid DharanikotaDharanikota, Samvid Efficient ComputerUnited States Fray: An Efficient General-Purpose Concurrency Testing Platform for the JVM
Tomás DiazDiaz, Tomás University of Chile, 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 Probabilistic Inference for Datalog with Correlated Inputs Active Learning for Neurosymbolic Program Synthesis Automated Discovery of Tactic Libraries for Interactive Theorem Proving Homomorphism Calculus for User-Defined Aggregations 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
Shuo DingDing, Shuo Georgia Institute of TechnologyChina Fast Constraint Synthesis for C++ Function Templates
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
Dana Drachsler CohenDrachsler Cohen, Dana TechnionIsrael Enhancing Neural Network Robustness via Synthesis of Repair Programs Mini-Batch Robustness Verification of Deep Neural Networks Quantization with Guaranteed Floating-Point Neural Network Classifications Guarding the Privacy of Label-Only Access to Neural Network Classifiers via Formal Verification
Steve DraperDraper, Steve University of Glasgow Let's Take Esoteric Programming Languages Seriously
Alexandre DreweryDrewery, Alexandre INRIA Contextual Equality Saturation
Sophia DrossopoulouDrossopoulou, Sophia Imperial College LondonUnited Kingdom Steering Committee Member in Steering Committee for SPLASH 2025 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 University 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
Saikat DuttaDutta, Saikat University of Illinois at Urbana-ChampaignUnited States Precise Abstract Interpretation of Probabilistic Programs with Interval Data Uncertainty
Saikat DuttaDutta, Saikat Cornell UniversityUnited States Understanding and Improving Flaky Test Classification
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 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 State
Susan EisenbachEisenbach, Susan Imperial College LondonUnited Kingdom Reasoning about External Calls
Richard A. EisenbergEisenberg, Richard A. Jane StreetUnited States Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Joel S EmerEmer, Joel S MIT/NVIDIA 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
Patrick EugsterEugster, Patrick USI Lugano; Purdue UniversitySwitzerland 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 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 The Continuous Tensor Abstraction: Where Indices are Real Finch: Sparse and Structured Tensor Programming with Control Flow
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
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
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
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
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 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
Patricia FirlejczykFirlejczyk, Patricia ETH ZurichSwitzerland Modular Reasoning about Global State
Emily FirstFirst, Emily University of California, San DiegoUnited States Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Krisztian FlautnerFlautner, Krisztian University of Michigan Meaning-Typed Programming: Language Abstraction and Runtime for Model-Integrated Applications
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 Steering Committee Member in Steering Committee for SPLASH 2025 Metamorph: Synthesizing Large Objects from Dafny Specifications RestPi: Path-Sensitive Type Inference for REST APIs
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
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
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 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
François GauthierGauthier, François Oracle LabsAustralia Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
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 Columbia 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 Demo: 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
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
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 of Maryland College ParkUnited States Tuning Random Generators: Property-Based Testing as Probabilistic Programming QED in Context: An Observation Study of Proof Assistant Users
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 Onward! Essays Co-chair in Organizing Committee for SPLASH 2025 Modal Abstractions for Virtualizing Memory Addresses Program Chair in Program Committee within the SPLASH Onward! Essays-track 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
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
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
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
Karuna GrewalGrewal, Karuna SafeTree: Expressive Tree Policies for Microservices
Tobias GrosserGrosser, Tobias University of CambridgeUnited Kingdom Interactive Bit Vector Reasoning using Verified Bitblasting Compressed and Parallelized Structured Tensor Algebra Certified Decision Procedures for Width-Independent Bitvector Predicates
David GroveGrove, David IBM ResearchUnited States Steering Committee Member in Steering Committee for SPLASH 2025
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
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 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 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 University 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
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 Complete the Cycle: Reachability Types with Expressive Cyclic References Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
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 Department of Computer Science, University of Copenhagen (DIKU) and Deon DigitalDenmark Committee Member in ICFP Programme Committee within the ICFP Papers-track
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
Andrew K. HirschHirsch, Andrew K. University at Buffalo, SUNYUnited States Choreographic Quick Changes: First-Class Location (Set) Polymorphism
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
Steven HoltzenHoltzen, Steven Northeastern UniversityUnited States Multi-Language Probabilistic Programming Scaling Optimization Over Uncertainty via Compilation
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
Tony HoskingHosking, Tony Australian National UniversityAustralia Steering Committee Member in Steering Committee for SPLASH 2025
Cătălin HriţcuHriţcu, Cătălin MPI-SPGermany Committee Member in ICFP Programme Committee within the ICFP Papers-track
Justin HsuHsu, Justin Cornell UniversityUnited States A Hoare Logic For Symmetry Properties SafeTree: Expressive Tree Policies for Microservices
Guangyu HuHu, Guangyu HKUST (The Hong Kong University of Science and Technology) Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
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
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 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 London 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
Doha HwangHwang, Doha Samsung PAFL: Enhancing Fault Localizers by Leveraging Project-Specific Fault Patterns
I Yuka IkarashiIkarashi, Yuka Massachusetts Institute of TechnologyUnited States Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
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 Jules JacobsJacobs, Jules Cornell UniversityUnited States Committee Member in ICFP Programme Committee within the ICFP Papers-track
Seyed Mohammad Reza JafariJafari, Seyed Mohammad Reza Iowa State University Embedding Quantum Program Verification into Dafny
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
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 Pyrosome: Verified Compilation for Modular Metatheory
Dustin JamnerJamner, Dustin MIT CSAIL, USA Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
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 Korea UniversitySouth Korea PAFL: Enhancing Fault Localizers by Leveraging Project-Specific Fault Patterns Committee Member in ICFP Programme Committee within the ICFP Papers-track
Jessy Ayala Jessy Ayala University of California, IrvineUnited States Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Artur JezJez, Artur University of Wroclaw The Power of Regular Constraint Propagation
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
Ranjit JhalaJhala, Ranjit University of California at San DiegoUnited States Counterexample-Guided Inference of Modular Specifications
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 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 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 Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
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
Yuchao JiangJiang, Yuchao UNSWAustralia Committee Member in Committee within the SPLASH Student Research Competition-track
Yuchen JiangJiang, Yuchen University of Michigan Notions of Stack-manipulating Computation and Relative Monads
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
Ohad KammarKammar, Ohad University of EdinburghUnited Kingdom Committee Member in ICFP Programme Committee within the ICFP Papers-track
Gabriel KammerKammer, Gabriel MIT Pyrosome: Verified Compilation for Modular Metatheory
Matthew KaneyKaney, Matthew Demo: 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 Meaning-Typed Programming: Language Abstraction and Runtime for Model-Integrated Applications
Savini KashmiraKashmira, Savini University of Michigan Meaning-Typed Programming: Language Abstraction and Runtime for Model-Integrated Applications
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
Alex KavvosKavvos, Alex University of BristolUnited Kingdom Adequacy for Algebraic Effects Revisited Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track 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 Chair in Onward! Steering Committee within the SPLASH Onward! Essays-track 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 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
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
Jaewoo KimKim, Jaewoo KAISTSouth Korea Revamping Verilog Semantics for Foundational Verification
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
John C. KolesarKolesar, John C. Yale UniversityUnited States Coinductive Proofs of Regular Expression Equivalence in Zero Knowledge
Paulette KoronkevichKoronkevich, Paulette University of British Columbia Type-Preserving Flat Closure Optimization
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
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
Anastasiya Kravchuk-KirilyukKravchuk-Kirilyuk, Anastasiya Harvard UniversityUnited States Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
V Krishna NandivadaKrishna Nandivada, V IIT Madras 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 Co-chair in OOPSLA Review Committee within the SPLASH OOPSLA-track
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
Burcu Kulahcioglu OzkanKulahcioglu Ozkan, Burcu Delft University of TechnologyNetherlands Model-guided Fuzzing of Distributed Systems
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
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 Co-chair in REBASE within the SPLASH REBASE-track
L 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
Leonidas LampropoulosLampropoulos, Leonidas University of Maryland, College ParkGreece Compositional Quantum Control Flow with Efficient Compilation in Qunity
Jens Kanstrup LarsenLarsen, Jens Kanstrup DTUDenmark Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Jacob LaurelLaurel, Jacob Georgia Institute of Technology Precise Abstract Interpretation of Probabilistic Programs with Interval Data Uncertainty Synthesizing Sound and Precise Abstract Transformers for Nonlinear Hyperbolic PDE Solvers
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
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 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
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
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 Faster Explicit-Trace Monitoring-Oriented Programming for Runtime Verification of Software Tests
Julien LehmannLehmann, Julien CEA, LIST, France Verifying Neural Networks with PyRAT
Daan LeijenLeijen, Daan Microsoft ResearchUnited States Committee Member in Program Committee within the SPLASH Onward! Papers-track
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 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 Qualified Types with Boolean Algebras Flix: A Design for Language-Integrated Datalog
Ao LiLi, Ao Carnegie Mellon UniversityUnited States Fray: An Efficient General-Purpose Concurrency Testing Platform for the JVM
Baichuan LiLi, Baichuan University of Michigan Meaning-Typed Programming: Language Abstraction and Runtime for Model-Integrated Applications
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 Institute 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
John LiLi, John Northeastern UniversityUnited States From Linearity to Borrowing Multi-Language Probabilistic Programming
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
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
Long LiLi, Long Ant Group MetaKernel: Enabling Efficient Encrypted Neural Network Inference Through Unified MVM and Convolution
Mingyi LiLi, Mingyi Institute of Computing Technology, Chinese Academy of Sciences 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 TailTracer: Continuous Tail Tracing for Production Use Towards a Theoretically-Backed and Practical Framework for Selective Object-Sensitive Pointer Analysis PReMM: LLM-Based Program Repair for Multi-Method Bugs via Divide and Conquer HybridPersist: A Compiler Support for User-Friendly and Efficient PM Programming
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 University 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
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
Youfang LinLin, Youfang Beijing Jiaotong University Fuzzing C++ Compilers via Type-Driven Mutation
Sam LindleyLindley, Sam The University of EdinburghUnited Kingdom Modal Effect Types
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 Labs 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 Committee Member in Program Committee and Panel within the SPLASH Doctoral Symposium-track
Yue LiuLiu, Yue Data61, CSIRO Committee Member in Committee within the SPLASH Student Research Competition-track
Zixi LiuLiu, Zixi Nanjing UniversityChina An Empirical Study of Bugs in the rustc Compiler
Zixi LiuLiu, Zixi Nanjing UniversityChina Debugging WebAssembly? Put some Whamm on it!
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
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
Yiling LouLou, Yiling Fudan UniversityChina 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 University of WashingtonUnited 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 Paper: Type-safe Blazon - Enforcing Pedantry in Heraldic Design The Simple Essence of Monomorphization
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 Compositional Symbolic Execution for the Next 700 Memory Models The Simulation Semantics of Synthesisable Verilog
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 Convex Hull Approximation for Activation Functions Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
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
P. MadhusudanMadhusudan, P. University of Illinois at Urbana-ChampaignUnited States Synthesizing DSLs for Few-Shot Learning FO-Complete Program Verification for Heap Logics
Magnus MadsenMadsen, Magnus Aarhus UniversityDenmark Qualified Types with Boolean Algebras Flix: A Design for Language-Integrated Datalog 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
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
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 University of KentUnited Kingdom 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 Meaning-Typed Programming: Language Abstraction and Runtime for Model-Integrated Applications
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
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 Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track Committee Member in Program Committee within the SPLASH Onward! Papers-track Steering Committee Member in Steering Committee within the SPLASH Onward! Papers-track
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
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 Demo: Sonic Earth - An Algorithmic Performance Approach to Real-Time Environmental Sonification Paper: Sonic Earth - An Algorithmic Performance Approach to Real-Time Environmental Sonification
Kathryn S McKinleyMcKinley, Kathryn S Google Work Packets: A New Abstraction for GC Software Engineering, Optimization, and Innovation Advancing Performance via a Systematic Application of Research and Industrial Best Practice
Michael McLoughlinMcLoughlin, Michael Carnegie Mellon University Scaling Instruction-Selection Verification against Authoritative ISA Semantics
Vaibhav MehtaMehta, Vaibhav Princeton 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 GALA: A High Performance Graph Neural Network Acceleration LAnguage and Compiler Automated Verification of Soundness of DNN Certifiers SPLAT: A framework for optimised GPU code-generation for SParse reguLar ATtention
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 General Chair in Organizing Committee within the SPLASH FARM Performance-track
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 Synthesizing Implication Lemmas for Interactive Theorem Proving Tuning Random Generators: Property-Based Testing as Probabilistic Programming
Mikhail MintsMints, Mikhail California Institute of Technology 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 Precise Abstract Interpretation of Probabilistic Programs with Interval Data Uncertainty Workshops Co-Chair in Workshop Selection Committee within the ICFP/SPLASH Workshops-track
Ashish MishraMishra, Ashish IIT HyderabadIndia We’ve Got You Covered: Type-Guided Repair of Incomplete Input Generators Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track 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 Demo: Girard's Paradox as Structure Music Concert: Girard’s Paradox
Alexandre MoineMoine, Alexandre New York UniversityUnited States Committee Member in ICFP Programme Committee within the ICFP Papers-track
Abtin MolaviMolavi, Abtin University of Wisconsin-Madison Dependency-Aware Compilation for Surface Code Quantum Architectures
Raphaël MonatMonat, Raphaël Inria and University of LilleFrance Committee Member in Program Committee within the SAS -track
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
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
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
Anders MøllerMøller, Anders Aarhus UniversityDenmark Steering Committee Member 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 A Refinement Methodology for Distributed Programs in Rust Place Capability Graphs: A General-Purpose Model of Rust’s Ownership and Borrowing Guarantees Modular Reasoning about Global State
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
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 Toronto 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
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
Aman NougrahiyaNougrahiya, Aman IIT MadrasIndia IncIDFA: An Efficient and Generic Algorithm for Incremental Iterative Dataflow Analysis
Clemens Nylandsted KlokmoseNylandsted Klokmose, Clemens Aarhus UniversityDenmark 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 Committee Member in ICFP Programme Committee within the ICFP Papers-track
Martin OderskyOdersky, Martin EPFLSwitzerland What's in the Box: Ergonomic and Expressive Capture Tracking over Generic Data Structures
Hakjoo OhOh, Hakjoo Korea UniversitySouth Korea 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 Program Co-Chair in Organizing Committee within the SAS -track Committee Member in ICFP Programme Committee within the ICFP Papers-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 Liberating Merges via Apartness and Guarded Subtyping Flexible and Expressive Typed Path Patterns for GQL
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
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
Jens PalsbergPalsberg, Jens University of California, Los Angeles (UCLA)United States 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
Awanish PandeyPandey, Awanish IIT RoorkeeIndia Committee Member in Committee within the SPLASH Student Research Competition-track
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 Performance-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 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
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
William PaynePayne, William UNC School of Information and Library Science Demo: 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
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 A Refinement Methodology for Distributed Programs in Rust Modular Reasoning about Global State
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
Anja Petković KomelPetković Komel, Anja TU Wien, Vienna, Austria 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 Contextual Equality Saturation Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track Committee Member in Steering Committee within the SAS -track
Lauren PickPick, Lauren The Chinese University of Hong Kong Checking Observational Correctness of Database Systems
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 Coinductive Proofs of Regular Expression Equivalence in Zero Knowledge Counterexample-Guided Inference of Modular Specifications
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
Gabriel PoesiaPoesia, Gabriel Stanford University Automated Discovery of Tactic Libraries for Interactive Theorem Proving
Nadia PolikarpovaPolikarpova, Nadia University of California at San DiegoUnited States Laurel: Unblocking Automated Verification with Large Language Models Peepco: Batch-Based Consistency Optimization
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 Embedding Quantum Program Verification into Dafny
Jyoti PrakashPrakash, Jyoti University of PassauGermany Committee Member in SAS Artifact Evaluation Committee within the SAS Artifact-track
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
Q 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
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
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 A Domain-Specific Probabilistic Programming Language for Reasoning about Reasoning (or: a memo on memo) Gauguin, Descartes, Bayes: A Diurnal Golem's Brain
Shanto RahmanRahman, Shanto The University of Texas at AustinUnited States Understanding and Improving Flaky Test Classification UTFix: Change Aware Unit Test Repairing using LLM
Sophie RainRain, Sophie Argot Collective Divide and Conquer: A Compositional Approach to Game-Theoretic Security
Hridesh RajanRajan, Hridesh Tulane UniversityUnited States Steering Committee Member in Steering Committee for SPLASH 2025
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 A Language for Quantifying Quantum Network Behavior Compositional Quantum Control Flow with Efficient Compilation in Qunity
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
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 UC Santa Cruz Exploring the Theory and Practice of Concurrency in the Entity-Component-System Pattern
John RegehrRegehr, John University of UtahUnited States Translation Validation for LLVM's AArch64 Backend PC Member in Program Committee within the SPLASH Onward! Essays-track
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
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 Committee Member in ICFP Programme Committee within the ICFP Papers-track
Thomas RepsReps, Thomas University of Wisconsin-MadisonUnited States Scalable Equivalence Checking and Verification of Shallow Quantum Circuits Software Model Checking via Summary-Guided Search Semantics of Sets of Programs
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; ENS; CNRS; PSL UniversityFrance Committee Member in Program Committee within the SAS -track
Cody RiveraRivera, Cody University of Illinois, Urbana-Champaign Checking ?-Satisfiability of Reals with Integrals
Alice RixteRixte, Alice Paper: 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
Subhajit RoyRoy, Subhajit IIT KanpurIndia Student Research Competition Chair in Organizing Committee for SPLASH 2025 Memory-Safety Verification of Open Programs With Angelic Assumptions Co-chair in 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 Co-chair in OOPSLA Review Committee within the SPLASH OOPSLA-track
S William S. MosesS. Moses, William University of Illinois Urbana-ChampaignUnited States Mind the Abstraction Gap: Bringing Equality Saturation to Real-World ML Compilers Sound and Modular Activity Analysis for Automatic Differentiation in MLIR
Feras SaadSaad, Feras Carnegie Mellon UniversityUnited States Integrating Resource Analyses via Resource Decomposition
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
Ken SakayoriSakayori, Ken University of TokyoJapan Automated Catamorphism Synthesis for Solving Constrained Horn Clauses over Algebraic Data Types
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-Madison 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
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
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
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
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
Philipp SchusterSchuster, Philipp University of TübingenGermany Compiling Classical Sequent Calculus to Stock Hardware: The Duality of Compilation The Simple Essence of Monomorphization Dynamic Wind for Effect Handlers Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
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 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
Manuel SerranoSerrano, Manuel Inria; Université Côte d’AzurFrance 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 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 College Scaling Instruction-Selection Verification against Authoritative ISA Semantics
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 Committee Member in Organizing Committee within the SPLASH Sponsor Industrial Forum-track
Yuanfeng ShiShi, Yuanfeng Peking UniversityChina On Abstraction Refinement for Bayesian Program Analysis
Xujie SiSi, Xujie University of Toronto Committee Member in Program Committee within the SAS -track
Jeremy G. SiekSiek, Jeremy G. Indiana University, USAUnited States 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 Committee Member in Steering Committee within the SAS -track
Florian SihlerSihler, Florian Ulm UniversityGermany Statically Analyzing the Dataflow of R 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
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 ?-Satisfiability of Reals with Integrals
KC SivaramakrishnanSivaramakrishnan, KC IIT Madras and TaridesIndia Automatically Verifying Replication-aware Linearizability Associate Chair in OOPSLA Review Committee within the SPLASH OOPSLA-track 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 Meaning-Typed Programming: Language Abstraction and Runtime for Model-Integrated Applications
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 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 Urbana-Champaign & Riema Labs Tabby: A Synthesis-Aided Compiler for High-Performance Zero-Knowledge Proof Circuits
Wei SongSong, Wei Nanjing University of Science and TechnologyChina Finding Compiler Bugs through Cross-Language Code Generator and Differential Testing DepFuzz: Efficient Smart Contract Fuzzing with Function Dependence Guidance
Yahui SongSong, Yahui Standard Chartered BankSingapore Specifying and Verifying Future Conditions Committee Member in Committee within the SPLASH Student Research Competition-track Committee Member in ICFP Programme Committee within the ICFP Papers-track
Tyler SorensenSorensen, Tyler 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
Thodoris SotiropoulosSotiropoulos, Thodoris ETH ZurichSwitzerland Validating Soundness and Completeness in Pattern-Match Coverage Analyzers
Matthew SotoudehSotoudeh, Matthew Stanford University Pathological Cases for Garbage Collection
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 Aarhus UniversityDenmark 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 Interactive Bit Vector Reasoning using Verified Bitblasting Certified Decision Procedures for Width-Independent Bitvector Predicates
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
Sam StitesStites, Sam Northeastern University Multi-Language Probabilistic Programming
Quentin StiévenartStiévenart, Quentin Université du Québec à MontréalCanada Abstracting Concolic Execution for Soft Contract Verification Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
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 API-guided Dataset Synthesis to Finetune Large Code Models An Empirical Study of Bugs in the rustc Compiler
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 Program Co-Chair in Organizing Committee within the SAS -track Co-chair in Committee within the SPLASH Student Research Competition-track
Alexander J. SummersSummers, Alexander J. University of British ColumbiaCanada 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 Fuzzing C++ Compilers via Type-Driven Mutation Verification of Bit-Flip Attacks against Quantized Neural Networks Correct-By-Construction: Certified Individual Fairness through Neural Network Training
Maolin SunSun, Maolin Nanjing UniversityChina Validating SMT Rewriters via Rewrite Space Exploration Supported by Generative Equality Saturation Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Yaozhu SunSun, Yaozhu National Institute of InformaticsJapan Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
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
Nikhil SwamySwamy, Nikhil Microsoft ResearchUnited States Committee Member in ICFP Programme Committee within the ICFP Papers-track
Emma SöderbergSöderberg, Emma Lund UniversitySweden Committee Member in Program Committee within the SPLASH Onward! Papers-track
T Nicolas TabareauTabareau, Nicolas InriaFrance Incremental Certified Programming
Marcel TaeumelTaeumel, Marcel University of Potsdam; Hasso Plattner InstituteGermany 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 - Kanpur Memory-Safety Verification of Open Programs With Angelic Assumptions
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
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 Meaning-Typed Programming: Language Abstraction and Runtime for Model-Integrated Applications
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
Éric TanterTanter, Éric University of ChileChile Incremental Certified Programming
Muhammad Usman TariqTariq, Muhammad Usman Stanford University REPTILE: Performant Tiling of Recurrences
Christine TassonTasson, Christine Sorbonne Université — LIP6France Committee Member in ICFP Programme Committee within the ICFP Papers-track
Ross TateTate, Ross NoneUnited States Type-Consistency, Type-Outference, and Label-Listeners: Foundations for Decidability 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 A Domain-Specific Probabilistic Programming Language for Reasoning about Reasoning (or: a memo on memo) Gauguin, Descartes, Bayes: A Diurnal Golem's Brain
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 Committee Member in Program Committee within the SAS -track Committee Member in Committee within the SPLASH Student Research Competition-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 Freiburg, Germany Borrowing From Session Types Associate Chair in ICFP Programme Committee within the ICFP Papers-track
Yongqiang TianTian, Yongqiang Monash UniversityHong Kong SAR China Boosting Program Reduction with the Missing Piece of Syntax-Guided Transformations Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Matthias TichyTichy, Matthias Ulm UniversityGermany Statically Analyzing the Dataflow of R Programs
Eli TilevichTilevich, Eli Virginia TechUnited States Committee Member in Program Commitee within the SPLASH -E-track
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! Co-chair in REBASE within the SPLASH REBASE-track
Shrey TiwariTiwari, Shrey Carnegie Mellon UniversityUnited States Fray: An Efficient General-Purpose Concurrency Testing Platform for the JVM
Ryan TjoaTjoa, Ryan University of WashingtonUnited States Tuning Random Generators: Property-Based Testing as Probabilistic Programming
Bernardo ToninhoToninho, Bernardo NOVA-LINCS; Nova University of LisbonPortugal Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
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 Committee Member in ICFP Programme Committee within the ICFP Papers-track
Laurence TrattTratt, Laurence Software Development Team, King's College London Garbage Collection for Rust: The Finalizer Frontier
Conan TruongTruong, Conan University of California, Irvine Towards Verifying Crash Consistency
Yi-Zhen TsaiTsai, Yi-Zhen University of California, Riverside Spatial Coordination Synthesis for Augmented Reality
Ilias TsatirisTsatiris, Ilias DedaubGreece Universal Scalability in Declarative Program Analysis (with Choice-Based Combination Pruning)
Saar Tzour-ShadayTzour-Shaday, Saar Technion – Israel Institute of Technology 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
V 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 Zurich Modular Reasoning about Global State
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 Steering Committee for SPLASH 2025 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
Bram VandenbogaerdeVandenbogaerde, Bram Delta Store Semantics: Abstract Garbage Collection for Abstract Definitional Interpreters Monarch: A Modular Framework for Abstract Definitional Interpreters in Haskell Abstracting Concolic Execution for Soft Contract Verification
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 Borrowing From Session Types 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 VechevVechev, Martin ETH ZurichSwitzerland qblaze: An Efficient and Scalable Sparse Quantum Simulator
Jyothi VeduradaVedurada, Jyothi IIT HyderabadIndia Committee Member in 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
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 ?-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 University of Edinburgh Committee Member in Program Committee and Panel within the SPLASH Doctoral Symposium-track
Andrew WagnerWagner, Andrew Northeastern UniversityUnited States From Linearity to Borrowing
WONG Wai KinWai Kin, WONG Hong Kong University of Science and Technology Extraction and Mutation at a High Level: Template-Based Fuzzing for JavaScript Engines
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 Demo: 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 API-guided Dataset Synthesis to Finetune Large Code Models Binary Cryptographic Function Identification via Similarity Analysis with Path-insensitive Emulation Extraction and Mutation at a High Level: Template-Based Fuzzing for JavaScript Engines
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 Convex Hull Approximation for Activation Functions
Ziteng WangWang, Ziteng University of Texas at AustinUnited States Homomorphism Calculus for User-Defined Aggregations Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
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 Organizing Chair in Program Committee and Panel within the SPLASH Doctoral Symposium-track Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
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
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
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 Committee Member in ICFP Programme Committee within the ICFP Papers-track
Jaeyeon WonWon, Jaeyeon MIT The Continuous Tensor Abstraction: Where Indices are Real
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 Hong Kong University of Science and TechnologyChina API-guided Dataset Synthesis to Finetune Large Code Models Extraction and Mutation at a High Level: Template-Based Fuzzing for JavaScript Engines
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 TechnologyChina Extraction and Mutation at a High Level: Template-Based Fuzzing for JavaScript Engines Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
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 Committee Member in ICFP Programme Committee within the ICFP Papers-track
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 Tunneling Through the Hill: Multi-Way Intersection for Version-Space Algebras in Program Synthesis
Amanda XuXu, Amanda University of Wisconsin-Madison Synthesizing Quantum-Circuit Optimizers Checking Observational Correctness of Database Systems Dependency-Aware Compilation for Surface Code Quantum Architectures
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 SAS Artifact Evaluation Committee within the SAS Artifact-track Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-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 CambridgeUnited Kingdom 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
Zhenyu YanYan, Zhenyu Peking UniversityChina Committee Member in SAS Artifact Evaluation Committee within the SAS Artifact-track
Chenyuan YangYang, Chenyuan University of Illinois at 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 Fudan 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 Bounded-Exhaustive Subspace Diversification for SMT Solver Testing Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track 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 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 Northwestern University, USATaiwan Contract System Metatheories à la Carte: A Transition-System View of Contracts
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 Committee Member in Organizing Committee within the SPLASH Sponsor Industrial Forum-track
Cheng ZhangZhang, Cheng University College London (UCL)United Kingdom 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
Guanqin ZhangZhang, Guanqin University of New South Wales & CSIRO's Data61Australia Committee Member in Committee within the SPLASH Student Research Competition-track
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 Committee Member in Program Committee within the SAS -track Chair in Organizing Committee within the SPLASH Posters-track
Ruihan ZhangZhang, Ruihan Singapore Management University (SMU) Correct-By-Construction: Certified Individual Fairness through Neural Network Training
Shuhao ZhangZhang, Shuhao Peking University 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 On Abstraction Refinement for Bayesian Program Analysis Combining Formal and Informal Information in Bayesian Program Analysis via Soft Evidences 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 TailTracer: Continuous Tail Tracing for Production Use HybridPersist: A Compiler Support for User-Friendly and Efficient PM Programming
Yizhou ZhangZhang, Yizhou University of WaterlooCanada Zero-Overhead Lexical Effect Handlers
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 Work Packets: A New Abstraction for GC Software Engineering, Optimization, and Innovation Advancing Performance via a Systematic Application of Research and Industrial Best Practice
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
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 Mind the Abstraction Gap: Bringing Equality Saturation to Real-World ML Compilers Sound and Modular Activity Analysis for Automatic Differentiation in MLIR
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 TailTracer: Continuous Tail Tracing for Production Use HybridPersist: A Compiler Support for User-Friendly and Efficient PM Programming
Aron ZwaanZwaan, Aron Delft University of TechnologyNetherlands Language-Parametric Reference Synthesis

SPLASH 2025 Contributors

Results (1185)

Tracks

ICFP/SPLASH 2025

Co-hosted Conferences

Workshops

Co-hosted Symposia