John Wickerson
where else to find them
bluesky:wicko3.bsky.social
linkedin:john-wickerson-34a737167
what they talk about
all 7 in the filters
where they keep going back
- PLDI Workshop Honoring Andreas Podelski3 editions2020–2026
- OOPSLA2 editions2021–2024
- POPL2 editions2023–2024
all 6 in the filters
on a stage with
all 27 in the filters
who talks about the same things
- Alastair F. Donaldson14 talks
- Tyler Sorensen12 talks
- Azalea Raad27 talks
- Viktor Vafeiadis23 talks
- Vasileios Klimis4 talks
- Peter Sewell14 talks
| title | conference | date |
|---|---|---|
| Uniformity Analysis in the WebGPU Shading Language | PLDI 2026 | 2026-06-15 |
Provides a rigorous operational semantics for TinyWGSL that defines barrier divergence, formalizes the WGSL uniformity rules, and proves soundness sketches… | ||
| QuteFuzz: Fuzzing quantum compilers using randomly generated circuits with control(…) | PLanQC 2025 | 2025-01-25 |
QuteFuzz generates fully random quantum programs with nested subroutines and control flow, runs them through Qiskit, Pytket and Cirq stacks, and does… | ||
| 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… | ||
| Hyperblock Scheduling for Verified High-Level Synthesis | PLDI 2024 | 2024-06-24 |
A verified HLS backend implements a hyperblock scheduler with operation chaining and a system-of-difference-constraints LP scheduler, emits schedules checked… | ||
| Welcome | The Future of Weak Memory 2024 | 2024-01-15 |
Program opens by defining weak versus strong memory and lists concrete agenda items: empirical validation of memory persistency models, tooling for checking… | ||
| Extraordinary Meeting: The Publicity Chairs Reflect on the Peer-Review Process | POPL 2024 | 2024-01-14 |
A reflective, often comic diagnosis of peer review that names concrete pain points and behavior not just ideals It highlights workload pressures with numbers… | ||
| Taking Back Control in an Intermediate Representation for GPU Computing | POPL 2023 | 2023-01-15 |
Formal modeling of SPIR-V control flow encodes the rules in an Alloy model, replaces brittle dominance rules with structural dominance that counts control… | ||
| 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… | ||
| Formal Verification of High-Level Synthesis | OOPSLA 2021 | 2021-10-17 |
Presents a mechanically verified HLS tool called Vericert that extends CompCert and is proved correct in Coq, translating CompCert 3AC into an HTL FSM and then… | ||
| Ask Me Anything with Peter O'Hearn | PLDI 2020 | 2020-06-15 |
Answers claim a shift from heavy upfront specs to a pay-as-you-go model where small specs give incremental value, and point to concrete tools: Infer team work… | ||
| 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 | ||