Stanford's deterministic CUDA kernel verifier

Equivalence Checking of ML GPU Kernels (SPLASH 2026 - OOPSLA) - SPLASH 2026

SPLASH 2026Sat 3 - Fri 9 October 2026 Oakland, California, United States co-located with SPLASH/ISSTA 2026

Toggle navigation Attending Hotel: Oakland Marriott City Center SPLASH/ISSTA 2026 Visa Letter Registration Travel and Child Care Support Grants

Tracks SPLASH 2026 OOPSLA Onward! Essays Onward! Papers Onward! Steering Committee SIGPLAN track SPLASH Keynotes SPLASH/OOPSLA @ 40 Panel SPLASH-E Artifact evaluation SPLASH/ISSTA 2026 Doctoral symposium PLMW @ SPLASH/ISSTA'26 Posters Social Events Student Research Competition Student Volunteers Summer School Tool Demonstrations REBASE industry track Workshops Sponsorship

Co-hosted Conferences ISSTA ISSTA ISSTA Research papers ISSTA Artifact evaluation ISSTA Keynotes

Workshops EXPRESS Expression of software system DevOps FTA Firmware Testing and Analysis HATRA IWACO LMPL NSAD PLSS PL Standardization and Specification SpecOps Specification-Driven Development Life Cycle SSNL VMIL Co-hosted Symposia SAS Static Analysis SymposiumSAS SAS Artifact

Organization SPLASH 2026 Committees Track Committees OOPSLA Onward! Essays Onward! Papers Onward! Steering Committee SIGPLAN track SPLASH/OOPSLA @ 40 Panel SPLASH-E Artifact evaluation SPLASH/ISSTA Doctoral symposium PLMW @ SPLASH/ISSTA'26 Posters Social Events Student Research Competition Student Volunteers Summer School Speakers Organizers

Tool Demonstrations REBASE industry track Workshops Sponsorship Contributors People Index

Co-hosted Conferences ISSTA Research papers Artifact evaluation

Workshops EXPRESS Expression of software system DevOpsOrganizing Committee Steering Committee Program Committee

FTA Organizing Committee Program Committee

HATRA Organizing Committee Program Committee

IWACO Organizing Committee

LMPL Keynote Speaker Organizing Committee Program Committee

NSAD Organizing Committee Program Committee Steering Committee

PLSS PL Standardization and SpecificationOrganizers

SpecOps Specification-Driven Development Life CycleProgram Committee

SSNL N/A - check homepage

VMIL Program Committee

Co-hosted Symposia SAS Static Analysis SymposiumSAS 2026 Program Committee SAS 2026 Steering Committee SAS Artifact

Search Series Series

SPLASH 2027 SPLASH 2026 SPLASH 2025 SPLASH 2024 SPLASH 2023 SPLASH 2022 SPLASH 2021 SPLASH 2020 SPLASH 2019 SPLASH 2018 SPLASH 2017 SPLASH 2016 SPLASH 2015 SPLASH 2014 SPLASH 2013 SPLASH 2012 SPLASH 2011

SPLASH 2010

OOPSLA 2009 OOPSLA 2008 OOPSLA 2007 OOPSLA 2006 OOPSLA 2005 OOPSLA 2004 OOPSLA 2003 OOPSLA 2002 OOPSLA 2001 OOPSLA 2000

SPLASH/ISSTA 2026 (series) / SPLASH 2026 (series) / OOPSLA / Equivalence Checking of ML GPU Kernels

WhoKshitij Dubey, Benjamin Driscoll, Anjiang Wei, Neeraj Kayal, Rahul Sharma, Alex Aiken

TrackSPLASH 2026 OOPSLA

AbstractWith the rapid progress of deep learning and large language models (LLMs), companies spend enormous sums executing GPU kernels. These kernels have become prime targets for aggressive optimization. Recent efforts increasingly leverage LLMs to generate GPU kernels, but make no formal guarantees about the generated kernels. We present the first equivalence checker for GPU kernels and use it to formally verify the correctness of machine learning (ML) kernels optimized by hand, by LLM, and by compiler. We show that our equivalence checker is sound and, for a well-defined class of GPU kernels which includes many programs of interest, complete. Our implementation, Volta, can verify ML computations such as convolutions, matrix multiplications, and various attention mechanisms.

Kshitij Dubey Microsoft Research

Benjamin Driscoll Stanford University

Anjiang Wei Stanford University United States

Neeraj Kayal Microsoft Research

Rahul Sharma Google Deepmind

Alex Aiken Stanford University United States

xWed 19 Aug 01:23

Stanford's deterministic CUDA kernel verifier

Related Articles

Incident with Github.com

(no title)

Scientists reverse brain aging, with a nasal spray

NHS apologises and admits Palantir have access to identifiable patient data

Cursor Origin