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

Group Publications

  • Grammar Mutation for Testing Input Parsers (Registered Report)

    Bachir Bendrissou, Cristian Cadar, Alastair F. Donaldson

    Proceedings of the 2nd International Fuzzing Workshop (FUZZING'23)

  • GrayC: Greybox Fuzzing of Compilers and Analysers for C

    Karine Even-Mendoza, Arindam Sharma, Alastair F. Donaldson, Cristian Cadar

    Proceedings of the 32nd ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA'23)

  • RustSmith: Random Differential Compiler Testing for Rust

    Mayank Sharma, Pingshi Yu, Alastair F. Donaldson

    Proceedings of the 32nd ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA'23)

  • Industrial Deployment of Compiler Fuzzing Techniques for Two GPU Shading Languages

    Alastair F. Donaldson, Ben Clayton, Ryan Harrison, Hasan Mohsin, David Neto, Vasyl Teliman, Hana Watson

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

  • Model Checking Futexes

    Hugues Evrard, Alastair F. Donaldson

    29th International Symposium on Model Checking of Software (SPIN'23)

  • MOD2IR: High-Performance Code Generation for a Biophysically Detailed Neuronal Simulation DSL

    George Mitenkov, Ioannis Magkanaris, Omar Awile, Pramod Kumbhar, Felix Schürmann, Alastair F. Donaldson

    International Conference on Compiler Construction (CC'23)

  • Program Reconditioning: Avoiding Undefined Behaviour When Finding and Reducing Compiler Bugs

    Bastien Lecoeur, Hasan Mohsin, Alastair F. Donaldson

    Proceedings of the ACM Programming Languages

  • Taking Back Control in an Intermediate Representation for GPU Computing

    Vasileios Klimis, Jack Clark, Alan Baker, David Neto, John Wickerson, Alastair F. Donaldson

    Proceedings of the ACM Programming Languages

  • Simulating Operational Memory Models Using Off-the-Shelf Program Analysis Tools

    Dan Iorga, John Wickerson, Alastair F. Donaldson

    IEEE Transactions on Software Engineering

  • Combining Static Analysis Error Traces with Dynamic Symbolic Execution (Experience Paper)

    Frank Busse, Pritam Gharat, Cristian Cadar, Alastair F. Donaldson

    Proceedings of the 31st ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA'22)

  • Metamorphic Fuzzing of C++ Libraries

    Andrei Lascu, Alastair F. Donaldson, Tobias Grosser, Torsten Hoefler

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

  • High-coverage Metamorphic Testing of Concurrency Support in C Compilers

    Matt Windsor, Alastair F. Donaldson, John Wickerson

    Software: Testing, Verification and Reliability

  • C4: The C Compiler Concurrency Checker

    Matt Windsor, Alastair F. Donaldson, John Wickerson

    Proceedings of the 30th ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA'21)

  • Test-Case Reduction and Deduplication Almost for Free with Transformation-Based Compiler Testing

    Alastair F. Donaldson, Paul Thomson, Vasyl Teliman, Stefano Milizia, André Perez Maselco, Antoni Karpiński

    42nd Annual ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'21)

  • Dreaming up Metamorphic Relations: Experiences from Three Fuzzer Tools

    Andrei Lascu, Matt Windsor, Alastair F. Donaldson, Tobias Grosser, John Wickerson

    6th International Workshop on Metamorphic Testing, in concunction with the 43rd International Conference on Software Engineering

  • The Semantics of Shared Memory in Intel CPU/FPGA Systems

    Dan Iorga, Alastair F. Donaldson, Tyler Sorensen, John Wickerson

    Proceedings of the ACM Programming Languages

  • Specifying and Testing GPU Workgroup Progress Models

    Tyler Sorensen, Lucas F. Salvador, Harmit Raval, Hugues Evrard, Margaret Martonosi, Alastair F. Donaldson

    Proceedings of the ACM Programming Languages

  • Closer to the Edge: Testing Compilers More Thoroughly by Being Less Conservative About Undefined Behaviour

    Karine Even-Mendoza, Cristian Cadar, Alastair F. Donaldson

    IEEE/ACM International Conference on Automated Software Engineering, New Ideas and Emerging Results Track (ASE-NIER 2020)

  • Putting Randomized Compiler Testing into Production

    Alastair F. Donaldson, Hugues Evrard, Paul Thomson

    34th European Conference on Object-Oriented Programming (ECOOP'20)

  • Test-Case Reduction via Test-Case Generation: Insights From the Hypothesis Reducer

    David R. MacIver, Alastair F. Donaldson

    34th European Conference on Object-Oriented Programming (ECOOP'20)

  • Slow and Steady: Measuring and Tuning Multicore Interference

    Dan Iorga, Tyler Sorensen, John Wickerson, Alastair F. Donaldson

    26th IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS'20)

  • A Report on the First Virtual PLDI Conference

    Alastair F. Donaldson

    CoRR

  • One Size Doesn’t Fit All: Quantifying Performance Portability of Graph Applications on GPUs

    Tyler Sorensen, Sreepathi Pai, Alastair F. Donaldson

    2019 IEEE International Symposium on Workload Characterization (IISWC'19)

  • Just Fuzz It: Solving Floating-Point Constraints Using Coverage-Guided Fuzzing

    Daniel Liew, Cristian Cadar, Alastair F. Donaldson, J. Ryan Stinnett

    ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE'19)

  • Sparse Record and Replay with Controlled Scheduling

    Christopher Lidbury, Alastair F. Donaldson

    40th Annual ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'19)

  • Performance Evaluation of OpenCL Standard Support (and Beyond)

    Tyler Sorensen, Sreepathi Pai, Alastair F. Donaldson

    International Workshop on OpenCL (IWOCL'19)

  • Metamorphic Testing of Android Graphics Drivers

    Alastair F. Donaldson

    4th International Workshop on Metamorphic Testing, in concunction with the 41st International Conference on Software Engineering

  • Compiler Fuzzing: How Much Does It Matter?

    Michael Marcozzi, Qiyi Tang, Alastair F. Donaldson, Cristian Cadar

    Proceedings of the ACM Programming Languages

  • GPU Schedulers: How Fair Is Fair Enough?

    Tyler Sorensen, Hugues Evrard, Alastair F. Donaldson

    29th International Conference on Concurrency Theory (CONCUR'17)

  • Implementing and Evaluating Candidate-Based Invariant Generation

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

    IEEE Transactions on Software Engineering

  • Floating-Point Symbolic Execution: A Case Study in N-version Programming

    Daniel Liew, Daniel Schemmel, Cristian Cadar, Alastair F. Donaldson, Rafael Zähl, Klaus Wehrle

    IEEE/ACM International conference on Automated Software Engineering (ASE 2017)

  • Forward Progress on GPU Concurrency

    Alastair F. Donaldson, Jeroen Ketema, Tyler Sorensen, John Wickerson

    28th International Conference on Concurrency Theory (CONCUR'17)

  • Cooperative Kernels: GPU Multitasking for Blocking Algorithms

    Tyler Sorensen, Hugues Evrard, Alastair F. Donaldson

    11th Joint Meeting on Foundations of Software Engineering (ESEC/FSE'17)

  • Dynamic Race Detection for C++11

    Christopher Lidbury, Alastair F. Donaldson

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

  • Automated Testing of Graphics Shader Compilers

    Alastair F. Donaldson, Hugues Evrard, Andrei Lascu, Paul Thomson

    Proceedings of the ACM Programming Languages

  • Termination Analysis for GPU Kernels

    Jeroen Ketema, Alastair F. Donaldson

    Science of Computer Programming

  • Certified Roundoff Error Bounds Using Semidefinite Programming

    Victor Magron, George Constantinides, Alastair F. Donaldson

    ACM Transactions on Mathematical Software

  • 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