Tyler Sorensen
where else to find them
no profile links on file
what they talk about
all 9 in the filters
where they keep going back
- OOPSLA4 editions2020–2025
all 6 in the filters
on a stage with
all 34 in the filters
who talks about the same things
- Alastair F. Donaldson14 talks
- John Wickerson14 talks
- Margaret Martonosi4 talks
- Guido Martínez10 talks
- Jonathan Ragan-Kelley12 talks
- Julien Lange5 talks
| title | conference | date |
|---|---|---|
| Consistency and Coherence of the NVIDIA Grace-Hopper Superchip | ISMM 2026 | 2026-06-16 |
Empirical study validates the Grace‑Hopper enforces the Compound Memory Consistency Model using 1,960 litmus variants spanning ARM and PTX, showing independent… | ||
| The Next Frontier for AI-Generated Kernels: Correctness | PAgE 2026 | 2026-06-15 |
KernelBench’s fixed test suites let buggy kernels pass tests and even reject correct implementations; mutation testing finds racey softmaxes and trivial… | ||
| From Workarounds to Root Causes: Experience Using Agentic Workflows to Debug Complex(…) | PAgE 2026 | 2026-06-15 |
Porting llama.cpp to the browser via WebGPU exposes a bug chain across WGSL, browser runtimes, compiler rewrites, and Metal; a context-managed, re-steerable… | ||
| SIMT-Step Execution: A Flexible Operational Semantics For GPU Subgroup Behavior | PLDI 2026 | 2026-06-15 |
Formal operational semantics defines subgroup behavior using dynamic basic blocks and a spectrum classifying instructions as independent, synchronous, or… | ||
| Kuiper: Correct and Efficient GPU Programming with Dependent Types and Separation Logic | PLDI 2026 | 2026-06-15 |
Kuiper is an F library that uses Pulse-based separation logic to verify GPU kernels, extending the logic with forall+ connective and located resources to model… | ||
| SafeRace: Assessing and Addressing WebGPU Memory Safety in the Presence of Data Races | OOPSLA 2025 | 2025-10-16 |
Identifies a WGSL specification gap where data races let downstream GPU compilers legally remove bounds clamps, enabling out‑of‑bounds accesses; implements a… | ||
| Kuiper: verified and efficient GPU programming | ARRAY 2025 | 2025-06-17 |
Kuiper is a verified GPU language that uses dependent types and concurrent separation logic (built on F★/Pulse) to guarantee memory safety and race freedom for… | ||
| Mix Testing: Specifying and Testing ABI Compatibility of C/C++ Atomics Implementations | OOPSLA 2024 | 2024-10-20 |
Tooling and results: a new testing technique compiles individual C/C++ atomic operations with multiple mappings, links the permutations, and checks whether… | ||
| Specifying and Testing GPU Workgroup Progress Models | OOPSLA 2021 | 2021-10-17 |
A toolbox formalizes a tiny concurrent language, implements executable semantics in the CDP model checker, synthesizes 483 litmus tests, compiles them to… | ||
| The Semantics of Shared Memory in Intel CPU/FPGA Systems | OOPSLA 2021 | 2021-10-17 |
Defines precise weak‑memory behaviors for Intel Xeon + Arria FPGA systems, encoding them as an operational model in CBMC and an axiomatic model in Alloy and… | ||
| Foundations of Empirical Memory Consistency Testing | OOPSLA 2020 | 2020-11-15 |
Claims a reproducible, efficient GPU litmus-testing workflow that finds weak-memory behaviors by combining a new OpenCL tool, randomized 737000 parameter sets… | ||
| The Semantics of Transactions and Weak Memory in x86, Power, ARM, and C++ | USENIX ATC '19 | 2019-07-10 |
Extends existing axiomatic models for x86, Power, ARMv8 and C++ with concrete TM rules and proves sanity properties (transactions never enable previously… | ||
| nothing matches | ||