Alastair (Ally) Donaldson is a Senior Lecturer at Imperial, and leads the Multicore Programming Group.

Group Publications

  • Dynamic Race Detection for C++11

    Christopher Lidbury, Alastair F. Donaldson

    44th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'17)

  • Portable Inter-workgroup Barrier Synchronisation for GPUs

    Tyler Sorensen, Alastair F. Donaldson, Mark Batty, Ganesh Gopalakrishnan, Zvonimir Rakamaric

    31st Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA'16)

  • Exposing Errors Related to Weak Memory in GPU Applications

    Tyler Sorensen, Alastair F. Donaldson

    37th Annual ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'16)

  • Metamorphic Testing for (Graphics) Compilers

    Alastair F. Donaldson, Andrei Lascu

    1st International Workshop on Metamorphic Testing, in concunction with the 38th International Conference on Software Engineering

  • Analysing the Program Analyser

    Cristian Cadar, Alastair F. Donaldson

    Visions of 2025 and Beyond Track, 38th International Conference on Software Engineering

  • Automatic Test Case Reduction for OpenCL

    Moritz Pflanzer, Alastair F. Donaldson, Andrei Lascu

    4th International Workshop on OpenCL (IWOCL'16)

  • Symbooglix: A Symbolic Execution Engine for Boogie Programs

    Daniel Liew, Cristian Cadar, Alastair F. Donaldson

    IEEE International Conference on Software Testing, Verification and Validation (ICST'16)

  • The Hitchhiker's Guide to Cross-Platform OpenCL Application Development

    Tyler Sorensen, Alastair F. Donaldson

    4th International Workshop on OpenCL (IWOCL'16)

  • Uncovering Bugs in Distributed Storage Systems during Testing (not in Production!)

    Pantazis Deligiannis, Matt McCutchen, Paul Thomson, Shuo Chen, Alastair F. Donaldson, John Erickson, Cheng Huang, Akash Lal, Rashmi Mudduluru, Shaz Qadeer, Wolfram Schulte

    14th USENIX Conference on File and Storage Technologies (FAST'16)

  • Integrating a large-scale testing campaign in the CK framework

    Andrei Lascu, Alastair F. Donaldson

    6th International Workshop on Adaptive Self-tuning Computing Systems (ADAPT'16)

  • Overhauling SC atomics in C11 and OpenCL

    Mark Batty, John Wickerson, Alastair F. Donaldson

    43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'16)

  • Implementing and Evaluating Candidate-Based Invariant Generation

    Adam Betts, Nathan Chong, Pantazis Deligiannis, Alastair F. Donaldson, Jeroen Ketema

    CoRR

  • Concurrency Testing Using Controlled Schedulers: An Empirical Study

    Paul Thomson, Alastair F. Donaldson, Adam Betts

    ACM Transactions on Parallel Computing

  • Fast and Precise Symbolic Analysis of Concurrency Bugs in Device Drivers

    Pantazis Deligiannis, Alastair F. Donaldson, Zvonimir Rakamaric

    30th IEEE/ACM International Conference on Automated Software Engineering (ASE'15)

  • Remote-Scope Promotion: Clarified, Rectified, and Verified

    John Wickerson, Mark Batty, Bradford M. Beckmann, Alastair F. Donaldson

    30th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA'15)

  • PENCIL: A Platform-Neutral Compute Intermediate Language for Accelerator Programming

    Riyadh Baghdadi, Ulysse Beaugnon, Albert Cohen, Tobias Grosser, Michael Kruse, Chandan Reddy, Sven Verdoolaege, Adam Betts, Alastair F. Donaldson, Jeroen Ketema, Javed Absar, Sven van Haastregt, Alexey Kravets, Anton Lokhmotov, Robert David, Elnar Hajiyev

    2015 International Conference on Parallel Architecture and Compilation (PACT'15)

  • Many-Core Compiler Fuzzing

    Christopher Lidbury, Andrei Lascu, Nathan Chong, Alastair F. Donaldson

    36th Annual ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'15)

  • Asynchronous Programming, Analysis and Testing with State Machines

    Pantazis Deligiannis, Alastair F. Donaldson, Jeroen Ketema, Akash Lal, Paul Thomson

    36th Annual ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'15)

  • GPU Concurrency: Weak Behaviours and Programming Assumptions

    Jade Alglave, Mark Batty, Alastair F. Donaldson, Ganesh Gopalakrishnan, Jeroen Ketema, Daniel Poetzl, Tyler Sorensen, John Wickerson

    20th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS'15)

  • The Lazy Happens-Before Relation: Better Partial-Order Reduction for Systematic Concurrency Testing

    Paul Thomson, Alastair F. Donaldson

    20th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (PPoPP'15)

  • The Design and Implementation of a Verification Technique for GPU Kernels

    Adam Betts, Nathan Chong, Alastair F. Donaldson, Jeroen Ketema, Shaz Qadeer, Paul Thomson, John Wickerson

    ACM Transactions on Programming Languages and Systems

  • Automatic Verification of Data Race Freedom in Device Drivers

    Pantazis Deligiannis, Alastair F. Donaldson

    2014 Imperial College Computing Student Workshop (ICCSW'14)

  • Engineering a Static Verification Tool for GPU Kernels

    Ethel Bardsley, Adam Betts, Nathan Chong, Peter Collingbourne, Pantazis Deligiannis, Alastair F. Donaldson, Jeroen Ketema, Daniel Liew, Shaz Qadeer

    26th International Conference on Computer Aided Verification (CAV'14)

  • KernelInterceptor: Automating GPU Kernel Verification by Intercepting Kernels and their Parameters

    Ethel Bardsley, Alastair F. Donaldson, John Wickerson

    International Workshop on OpenCL (IWOCL'14)

  • Warps and Atomics: Beyond Barrier Synchronization in the Verification of GPU Kernels

    Ethel Bardsley, Alastair F. Donaldson

    6th International NASA Formal Methods Symposium (NFM'14)

  • Proceedings 7th Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software (PLACES'14)

    Alastair F. Donaldson, Vasco T. Vasconcelos

  • Concurrency Testing Using Schedule Bounding: an Empirical Study

    Paul Thomson, Alastair F. Donaldson, Adam Betts

    19th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (PPoPP'14)

  • A Sound and Complete Abstraction for Reasoning About Parallel Prefix Sums

    Nathan Chong, Alastair F. Donaldson, Jeroen Ketema

    41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'14)

  • The GPUVerify Method: a Tutorial Overview

    Alastair F. Donaldson

    ECEASST

  • Software Model Checking

    Alastair F. Donaldson

    Computing Handbook, 3rd ed., vol. 1

  • Automatic Verification of Active Device Drivers

    Sidney Amani, Peter Chubb, Alastair F. Donaldson, Alexander Legg, Keng Chai Ong, Leonid Ryzhyk, Yanjin Zhu

    Operating Systems Review

  • Barrier Invariants: a Shared State Abstraction for the Analysis of Data-Dependent GPU Kernels

    Nathan Chong, Alastair F. Donaldson, Paul H. J. Kelly, Jeroen Ketema, Shaz Qadeer

    28th Annual {ACM} {SIGPLAN} Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA'13)

  • Estimating the WCET of GPU-Accelerated Applications Using Hybrid Analysis

    Adam Betts, Alastair F. Donaldson

    25th Euromicro Conference on Real-Time Systems (ECRTS'13)

  • Correct and Efficient Accelerator Programming (Dagstuhl Seminar 13142)

    Albert Cohen, Alastair F. Donaldson, Marieke Huisman, Joost-Pieter Katoen

    Dagstuhl Reports

  • Interleaving and Lock-Step Semantics for Analysis and Verification of GPU Kernels

    Peter Collingbourne, Alastair F. Donaldson, Jeroen Ketema, Shaz Qadeer

    22nd European Symposium on Programming (ESOP'13)

  • Automatic Verification of Message-Based Device Drivers

    Sidney Amani, Peter Chubb, Alastair F. Donaldson, Alexander Legg, Leonid Ryzhyk, Yanjin Zhu

    Seventh Conference on Systems Software Verification (SSV'12)

  • GPUVerify: a Verifier for GPU Kernels

    Adam Betts, Nathan Chong, Alastair F. Donaldson, Shaz Qadeer, Paul Thomson

    27th Annual {ACM} {SIGPLAN} Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA'12)

  • Model Checking Software - 19th International Workshop, SPIN 2012

    Alastair F. Donaldson, David Parker

  • SatAbs: A Bit-Precise Verifier for C Programs - (Competition Contribution)

    Gérard Basler, Alastair F. Donaldson, Alexander Kaiser, Daniel Kroening, Michael Tautschnig, Thomas Wahl

    18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'12)

  • Counterexample-Guided Abstraction Refinement for Symmetric Concurrent Programs

    Alastair F. Donaldson, Alexander Kaiser, Daniel Kroening, Michael Tautschnig, Thomas Wahl

    Formal Methods in System Design

  • Safe Asynchronous Multicore Memory Operations

    Matko Botincan, Mike Dodds, Alastair F. Donaldson, Matthew J. Parkinson

    26th IEEE/ACM International Conference on Automated Software Engineering (ASE'11)

  • Software Verification Using k-Induction

    Alastair F. Donaldson, Leopold Haller, Daniel Kroening, Philipp Rümmer},

    18th International Static Analysis Symposium (SAS'11)

  • Making Software Verification Tools Really Work

    Jade Alglave, Alastair F. Donaldson, Daniel Kroening, Michael Tautschnig

    9th International Symposium on Automated Technology for Verification and Analysis (ATVA'11)

  • Static Analysis of Device Drivers: We Can Do Better!

    Sidney Amani, Leonid Ryzhyk, Alastair F. Donaldson, Gernot Heiser, Alexander Legg, Yanjin Zhu

    Asia Pacific Workshop on Systems (APSys'11)

  • Symmetry-Aware Predicate Abstraction for Shared-Variable Concurrent Programs

    Alastair F. Donaldson, Alexander Kaiser, Daniel Kroening, Thomas Wahl

    23rd International Conference on Computer Aided Verification (CAV'11)

  • The Impact of Diverse Memory Architectures on Multicore Consumer Software: an Industrial Perspective from the Video Games Domain

    George Russell, Colin Riley, Neil Henning, Uwe Dolinsky, Andrew Richards, Alastair F. Donaldson, Alexander S. van Amesfoort

    ACM SIGPLAN Workshop on Memory Systems Performance and Correctness (MSPC'11)

  • SCRATCH: a Tool for Automatic Analysis of DMA Races

    Alastair F. Donaldson, Daniel Kroening, Philipp Rümmer}

    16th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (PPoPP'11)

  • Automatic Safety Proofs for Asynchronous Memory Operations

    Matko Botincan, Mike Dodds, Alastair F. Donaldson, Matthew J. Parkinson

    16th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (PPoPP'11)

  • Strengthening Induction-Based Race Checking with Lightweight Static Analysis

    Alastair F. Donaldson, Leopold Haller, Daniel Kroening

    12th International on Verification, Model Checking, and Abstract Interpretation (VMCAI'11)

  • Automatic Analysis of DMA Races Using Model Checking and k-Induction

    Alastair F. Donaldson, Daniel Kroening, Philipp Rümmer

    Formal Methods in System Design

  • Tightening Test Coverage Metrics: A Case Study in Equivalence Checking Using k-Induction

    Alastair F. Donaldson, Nannan He, Daniel Kroening, Philipp Rümmer

    9th International Symposium on Formal Methods for Components and Objects (FMCO'10)

  • Programming Heterogeneous Multicore Systems Using Threading Building Blocks

    George Russell, Paul Keir, Alastair F. Donaldson, Uwe Dolinsky, Andrew Richards, Colin Riley

    Euro-Par 2010 Parallel Processing Workshops - Revised Selected Papers

  • Automatic Analysis of Scratch-Pad Memory Code for Heterogeneous Multicore Processors

    Alastair F. Donaldson, Daniel Kroening, Philipp Rümmer

    16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'10)

  • Offload - Automating Code Migration to Heterogeneous Multicore Systems

    Pete Cooper, Uwe Dolinsky, Alastair F. Donaldson, Andrew Richards, Colin Riley, George Russell

    5th International Conference on High Performance Embedded Architectures and Compilers (HiPEAC'10)

  • Type inference and strong static type checking for Promela

    Alastair F. Donaldson, Simon J. Gay

    Science of Computer Programming

  • Replication and Abstraction: Symmetry in Automated Formal Verification

    Thomas Wahl and, Alastair F. Donaldson

    Symmetry

  • Language-Level Symmetry Reduction for Probabilistic Model Checking

    Alastair F. Donaldson, Alice Miller, David Parker

    6th International Conference on the Quantitative Evaluation of Systems (QEST'09)

  • Towards Metaprogramming for Parallel Systems on a Chip

    Lee W. Howes, Anton Lokhmotov, Alastair F. Donaldson, Paul H. J. Kelly

    Euro-Par 2009 Parallel Processing Workshops - Revised Selected Papers

  • On the constructive orbit problem

    Alastair F. Donaldson, Alice Miller

    Annals of Mathematics and Artificial Intelligence

  • Vector Symmetry Reduction

    Alastair F. Donaldson

    Electronic Notes in Theoretical Computer Science

  • Tackling Online Game Development Problems With a Novel Network Scripting Language

    George Russell, Alastair F. Donaldson, Paul Sheppard

    Proceedings of the 7th ACM SIGCOMM Workshop on Networks and System Support for Games (NETGAMES'08)

  • Compile-Time and Run-Time Issues in an Auto-Parallelisation System for the Cell BE Processor

    Alastair F. Donaldson, Paul Keir, Anton Lokhmotov

    Euro-Par 2008 Parallel Processing Workshops - Revised Selected Papers

  • Automatic Symmetry Detection for Promela

    Alastair F. Donaldson, Alice Miller

    Journal of Automated Reasoning