Alastair F. Donaldson
where else to find them
what they talk about
all 8 in the filters
where they keep going back
- PLDI Workshop Honoring Andreas Podelski3 editions2022–2026
- POPL3 editions2021–2024
- OOPSLA2 editions2021–2024
all 4 in the filters
on a stage with
all 24 in the filters
who talks about the same things
- John Wickerson14 talks
- Tyler Sorensen12 talks
- Vasileios Klimis4 talks
- Margaret Martonosi4 talks
- Guido Martínez10 talks
- Julien Lange5 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… | ||
| Randomised Testing of the Dafny Compiler: Into the CI | Dafny 2025 | 2025-01-19 |
Integrates the fuzzer fuzz-d into Dafny’s CI as CompFuzzCI, running a brief per‑PR fuzzing campaign in containers, auto‑reducing and attempting bisection, and… | ||
| 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… | ||
| Program Reconditioning: Avoiding Undefined Behaviour When Finding and(…) | PLDI 2024 | 2024-06-24 |
Introduces reconditioning: generate potentially unsafe GPU programs, then apply a source-to-source reconditioner just before compilation so reduction never… | ||
| Randomised Testing of the Dafny Compiler | Dafny 2024 | 2024-01-14 |
Built two generators, fuzz-d (differential testing) and DafnyFuzz (metamorphic testing), plus comparison with XDsmith, and apply reconditioning and… | ||
| 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… | ||
| Sequential Reasoning for Optimizing Compilers Under Weak Memory Concurrency | PLDI 2022 | 2022-06-13 |
Claim: a new sequential semantics seq suffices to prove compiler optimizations sound even when linked into arbitrary weak‑memory contexts modeled by the… | ||
| 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… | ||
| The Lean Researcher | POPL 2021 | 2021-01-17 |
Argument links Lean Startup rules to research and gives concrete, checkable examples: GPUVerify starts as manual two‑thread translations into Boogie and Z3 to… | ||
| nothing matches | ||