Alastair (Ally) Donaldson is a Senior Lecturer at Imperial, and leads the Multicore Programming Group.
Group Publications
-
Who checks the checkers? Automatically finding bugs in C-to-RTL formal equivalence checkers
Michalis Pardalos, Alastair F. Donaldson, Emiliano Morini, Laura Pozzi, John Wickerson
Proceedings of Design and Verification Conference Europe (DVCon Europe 2024)
-
Randomised Testing of the Compiler for a Verification-Aware Programming Language
Alastair F. Donaldson, Dilan Sheth, Jean-Baptiste Tristan, Alex Usher
IEEE International Conference on Software Testing, Verification and Validation (ICST'24)
-
Validating Database System Isolation Level Implementations with Version Certificate Recovery
Jack Clark, Alastair F. Donaldson, John Wickerson, Manuel Rigger
Proceedings of the 19th European Conference on Computer Systems (EuroSys'24)
-
Challenges in Empirically Testing Memory Persistency Models
Vasileios Klimis, Alastair F. Donaldson, Viktor Vafeiadis, John Wickerson, Azalea Raad
Proceedings of the 2024 ACM/IEEE 44th International Conference on Software Engineering: New Ideas and Emerging Results
-
Synchronisation in Language-level Symmetry Reduction for Probabilistic Model Checking
Ivaylo Valkov, Alastair F. Donaldson, Alice Miller
30th International Symposium on Model Checking of Software (SPIN'23)
-
Mix Testing: Specifying and Testing ABI Compatibility of C/C++ Atomics Implementations
Luke Geeson, James Brotherston, Wilco Dijkstra, Alastair F. Donaldson, Lee Smith, Tyler Sorensen, John Wickerson
Proceedings of the ACM Programming Languages
-
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
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
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
ECEASST
-
Software Model Checking
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
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