Alastair F. Donaldson

PhD opportunity: Automated Testing and Verification of Machine Learning Compilers and Runtimes

I am looking to recruit a PhD student to start in October 2025 to work on an exciting project on automated testing and verification for ML compilers and runtime systems. See here for details. The studentship is fully-funded but only covers UK home rate tuition fees; please check here to see whether you are eligible for home rate fees.

Candidates would need to have (or to be shortly awarded) a Distinction in a Masters (or equivalent) in Computer Science (or a related discipline).

Email me before 30th April if you are interested in applying!

Research group

My FastPL research group is interested in all things related to formal analysis, software testing and programming languages. For information about the group members and activities, see our group webpage.

Biography

Bio for advertising talks

Alastair Donaldson is a Professor in the Department of Computing at Imperial College London where he is Director of Research and leads the FastPL Group, investigating novel techniques and tool support for programming, testing and reasoning about high performance systems and their programming languages. He was Founder and Director of GraphicsFuzz Ltd., a start-up company specialising in metamorphic testing of graphics drivers, which was acquired by Google in 2018, after which he spent time working with Google as a software engineering and then as a Visiting Researcher. He was the recipient of the 2017 BCS Roger Needham Award and an EPSRC Early Career Fellowship, and has published more than 100 articles in the fields of programming languages, formal verification, software testing and parallel programming. Alastair was previously a Visiting Researcher at Microsoft Research Redmond, an EPSRC Postdoctoral Research Fellow at the University of Oxford and a Research Engineer at Codeplay Software Ltd. He holds a PhD from the University of Glasgow, and is a Fellow of the British Computer Society.

Career overview

2011-present: Faculty member in the Department of Computing, Imperial College London, Professor since 2020, Reader 2017-2020, Senior Lecturer 2014-2017, Lecturer 2011-2014
2022-2024: Testifying Expert Witness in UK Technology & Construction Court case, IBM UK Ltd v LzLabs GmbH & Ors, engaged by Clifford Chance LLP via Imperial Consultants
2021-2022: Visiting Researcher, Google
2018-2021: Senior Software Engineer, Google
2017-2018: Founder and Director, GraphicsFuzz Ltd. (acquired by Google in 2018)
2011-2012: Visiting Researcher then Consulting Researcher, Microsoft Research Redmond
2010-2011: Research Fellow, Wolfson College Oxford
2009-2011: EPSRC Postdoctoral Research Fellow, Department of Computer Science, University of Oxford
2007-2009: Research Engineer, Codeplay Software Ltd., Edinburgh
2005: Internship at Graham Technology, Renfrewshire
2003-2007: PhD in Computing Science, Department (now School) of Computing Science, University of Glasgow, supervised by Alice Miller
2002: Internship at Reuters Plc., London
1999-2003: BSc (hons, First Class) in Computing Science and Mathematics (combined), University of Glasgow

I am married to Chris, who runs Little Wild Things. We have three children, Poppy, Felix and Kitty, two cats, Jekyll and Minty, and a dog, Caspar.

Teaching

I currently teach:

The Theory and Practice of Concurrent Programming, a third year BEng/MEng module, co-taught with Azalea Raad
Object-oriented Programming in Kotlin and Java, as part of Computing Practical 1, our first year BEng/MEng "mega module"

Previous courses I have developed and taught include Symbolic Reasoning and Software Reliability.

Current Service

Director of Research: Department of Computing, Imperial College London
PLDI Steering Committee: Steering Committee Chair, ACM SIGPLAN Conference on Programming Language Design and Implementation, 2022-2025 (SC member since 2018)
PACM-PL: Advisory Board member for Proceedings of the ACM on Programming Languages journal, since 2022
SIGPLAN Awards 2025: Committee Member for ACM SIGPLAN Programming Languages Software Award, 2025
ICSE 2025: PC member, 47th International Conference on Software Engineering
ICST 2025: PC member, 18th IEEE International Conference on Software Testing, Verification and Validation
Dafny 2025: PC member, Dafny Workshop co-locaed with POPL 2025
VSS 2025: PC member, International Workshop on Verification of Scientific Software, part of ETAPS 2025
SBFT 2025: PC member, 18th International Workshop on Search-Based and Fuzz Testing

Publications

ASPLOS 2025: Pingshi Yu, Nicolas Wu, and Alastair F. Donaldson. Ratte: Fuzzing for miscompilations in multi-level compilers using composable semantics. In Proceedings of the 30th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS 2025, Rotterdam, The Netherlands, March 30-April 3, 2025. ACM, 2025. To appear.
[ pdf ]
ASPLOS 2025: Chengsong Tan, Alastair F. Donaldson, and John Wickerson. Formalising CXL cache coherence. In Proceedings of the 30th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS 2025, Rotterdam, The Netherlands, March 30-April 3, 2025. ACM, 2025. To appear.
[ pdf ]
FormaliSE 2025: Chengsong Tan, Alastair F. Donaldson, Jonathan Julián Huerta y Munive, and John Wickerson. The burden of proof: Automated tooling for rapid iteration on large mechanised proofs. In Proceedings of the 2025 IEEE/ACM 13th International Conference on Formal Methods in Software Engineering (FormaliSE), Ottowa, Canada, April 27-28, 2025. IEEE, 2025. To appear.
[ pdf ]
ICST 2025: Shahin Honarvar, Mark van der Wilk, and Alastair F. Donaldson. Turbulence: Systematically and automatically testing instruction-tuned large language models for code. In IEEE Conference on Software Testing, Verification and Validation, ICST 2025, Naples, Italy, March 31-April 4, 2025. IEEE, 2025. To appear.
[ pdf ]
ICST 2025: Manuel Carrasco, Cristian Cadar, and Alastair F. Donaldson. Scalable SMT sampling for floating-point formulas via coverage-guided fuzzing. In IEEE Conference on Software Testing, Verification and Validation, ICST 2025, Naples, Italy, March 31-April 4, 2025. IEEE, 2025. To appear.
[ pdf ]
ICST 2025: Karnbongkot Boonriong, Stefan Zetzsche, and Alastair F. Donaldson. Compiler fuzzing in continuous integration: A case study on Dafny. In IEEE Conference on Software Testing, Verification and Validation, ICST 2025, Naples, Italy, March 31-April 4, 2025. IEEE, 2025. To appear.
[ pdf ]
STTT 2025: Hugues Evrard and Alastair F. Donaldson. Analysing futex-based synchronisation primitives using model checking. Int. J. Softw. Tools Technol. Transf., 2025. To appear.
[ pdf ]
TOSEM 2024: Bachir Bendrissou, Cristian Cadar, and Alastair F. Donaldson. Grammar mutation for testing input parsers. ACM Trans. Softw. Eng. Methodol., December 2024. Just Accepted.
[ DOI | pdf ]
DVCon 2024: Michalis Pardalos, Alastair F. Donaldson, Emiliano Morini, Laura Pozzi, and John Wickerson. Who checks the checkers? Automatically finding bugs in C-to-RTL formal equivalence checkers. In Design and Verification Conference, 2024.
[ pdf ]
OOPSLA 2024: Luke Geeson, James Brotherston, Wilco Dijkstra, Alastair F. Donaldson, Lee Smith, Tyler Sorensen, and John Wickerson. Mix testing: Specifying and testing ABI compatibility of C/C++ atomics implementations. Proc. ACM Program. Lang., 8(OOPSLA2):442--467, 2024.
[ DOI | pdf ]
EuroSys 2024: Jack Clark, Alastair F. Donaldson, John Wickerson, and Manuel Rigger. Validating database system isolation level implementations with version certificate recovery. In Proceedings of the Nineteenth European Conference on Computer Systems, EuroSys 2024, Athens, Greece, April 22-25, 2024, pages 754--768. ACM, 2024. Best Paper award.
[ DOI | pdf ]
ICSE NIER 2024: Vasileios Klimis, Alastair F. Donaldson, Viktor Vafeiadis, John Wickerson, and Azalea Raad. Challenges in empirically testing memory persistency models. In Proceedings of the 2024 ACM/IEEE 44th International Conference on Software Engineering: New Ideas and Emerging Results, NIER@ICSE 2024, Lisbon, Portugal, April 14-20, 2024, pages 82--86. ACM, 2024.
[ DOI | pdf ]
ICST 2024: Alastair F. Donaldson, Dilan Sheth, Jean-Baptiste Tristan, and Alex Usher. Randomised testing of the compiler for a verification-aware programming language. In IEEE Conference on Software Testing, Verification and Validation, ICST 2024, Toronto, ON, Canada, May 27-31, 2024, pages 407--418. IEEE, 2024. Best Industry Paper award.
[ DOI | pdf ]
SPIN 2024: Ivaylo Valkov, Alastair F. Donaldson, and Alice Miller. Synchronisation in language-level symmetry reduction for probabilistic model checking. In Thomas Neele and Anton Wijs, editors, Model Checking Software - 30th International Symposium, SPIN 2024, Luxembourg City, Luxembourg, April 8-9, 2024, Proceedings, volume 14624 of Lecture Notes in Computer Science, pages 49--66. Springer, 2024.
[ DOI | pdf ]
PLDI 2023: Bastien Lecoeur, Hasan Mohsin, and Alastair F. Donaldson. Program reconditioning: Avoiding undefined behaviour when finding and reducing compiler bugs. Proc. ACM Program. Lang., 7(PLDI):1801--1825, 2023.
[ DOI | pdf ]
POPL 2023: Vasileios Klimis, Jack Clark, Alan Baker, David Neto, John Wickerson, and Alastair F. Donaldson. Taking back control in an intermediate representation for GPU computing. Proc. ACM Program. Lang., 7(POPL):1740--1769, 2023.
[ DOI | pdf ]
TSE 2023: Dan Iorga, John Wickerson, and Alastair F. Donaldson. Simulating operational memory models using off-the-shelf program analysis tools. IEEE Trans. Software Eng., 49(12):5084--5102, 2023.
[ DOI | pdf ]
CC 2023: George Mitenkov, Ioannis Magkanaris, Omar Awile, Pramod S. Kumbhar, Felix Schürmann, and Alastair F. Donaldson. MOD2IR: high-performance code generation for a biophysically detailed neuronal simulation DSL. In Clark Verbrugge, Ondrej Lhoták, and Xipeng Shen, editors, Proceedings of the 32nd ACM SIGPLAN International Conference on Compiler Construction, CC 2023, Montréal, QC, Canada, February 25-26, 2023, pages 203--215. ACM, 2023.
[ DOI | pdf ]
FUZZING 2023: Bachir Bendrissou, Cristian Cadar, and Alastair F. Donaldson. Grammar mutation for testing input parsers (registered report). In Marcel Böhme, Yannic Noller, Baishakhi Ray, and László Szekeres, editors, Proceedings of the 2nd International Fuzzing Workshop, FUZZING 2023, Seattle, WA, USA, 17 July 2023, pages 3--11. ACM, 2023.
[ DOI | pdf ]
ICST 2023: Alastair F. Donaldson, Ben Clayton, Ryan Harrison, Hasan Mohsin, David Neto, Vasyl Teliman, and Hana Watson. Industrial deployment of compiler fuzzing techniques for two GPU shading languages. In IEEE Conference on Software Testing, Verification and Validation, ICST 2023, Dublin, Ireland, April 16-20, 2023, pages 374--385. IEEE, 2023.
[ DOI | pdf ]
ISSTA 2023: Karine Even-Mendoza, Arindam Sharma, Alastair F. Donaldson, and Cristian Cadar. GrayC: Greybox fuzzing of compilers and analysers for C. In René Just and Gordon Fraser, editors, Proceedings of the 32nd ACM SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2023, Seattle, WA, USA, July 17-21, 2023, pages 1219--1231. ACM, 2023. ACM SIGSOFT Disginguished Paper award.
[ DOI | pdf ]
ISSTA 2023: Mayank Sharma, Pingshi Yu, and Alastair F. Donaldson. RustSmith: Random differential compiler testing for Rust. In René Just and Gordon Fraser, editors, Proceedings of the 32nd ACM SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2023, Seattle, WA, USA, July 17-21, 2023, pages 1483--1486. ACM, 2023.
[ DOI | pdf ]
SPIN 2023: Hugues Evrard and Alastair F. Donaldson. Model checking futexes. In Georgiana Caltais and Christian Schilling, editors, Model Checking Software - 29th International Symposium, SPIN 2023, Paris, France, April 26-27, 2023, Proceedings, volume 13872 of Lecture Notes in Computer Science, pages 41--58. Springer, 2023.
[ DOI | pdf ]
ESE 2022: Karine Even-Mendoza, Cristian Cadar, and Alastair F. Donaldson. CsmithEdge: more effective compiler testing by handling undefined behaviour less conservatively. Empir. Softw. Eng., 27(6):129, 2022.
[ DOI | pdf ]
STVR 2022: Matt Windsor, Alastair F. Donaldson, and John Wickerson. High-coverage metamorphic testing of concurrency support in C compilers. Softw. Test. Verification Reliab., 32(4), 2022.
[ DOI | pdf ]
ICST 2022: Andrei Lascu, Alastair F. Donaldson, Tobias Grosser, and Torsten Hoefler. Metamorphic fuzzing of C++ libraries. In 15th IEEE Conference on Software Testing, Verification and Validation, ICST 2022, Valencia, Spain, April 4-14, 2022, pages 35--46. IEEE, 2022.
[ DOI | pdf ]
ISSTA 2022: Frank Busse, Pritam M. Gharat, Cristian Cadar, and Alastair F. Donaldson. Combining static analysis error traces with dynamic symbolic execution (experience paper). In Sukyoung Ryu and Yannis Smaragdakis, editors, ISSTA '22: 31st ACM SIGSOFT International Symposium on Software Testing and Analysis, Virtual Event, South Korea, July 18 - 22, 2022, pages 568--579. ACM, 2022.
[ DOI | pdf ]
OOPSLA 2021: Dan Iorga, Alastair F. Donaldson, Tyler Sorensen, and John Wickerson. The semantics of shared memory in Intel CPU/FPGA systems. Proc. ACM Program. Lang., 5(OOPSLA):1--28, 2021.
[ DOI | pdf ]
OOPSLA 2021: Tyler Sorensen, Lucas F. Salvador, Harmit Raval, Hugues Evrard, John Wickerson, Margaret Martonosi, and Alastair F. Donaldson. Specifying and testing GPU workgroup progress models. Proc. ACM Program. Lang., 5(OOPSLA):1--30, 2021.
[ DOI | pdf ]
MET 2021: Andrei Lascu, Matt Windsor, Alastair F. Donaldson, Tobias Grosser, and John Wickerson. Dreaming up metamorphic relations: Experiences from three fuzzer tools. In 6th IEEE/ACM International Workshop on Metamorphic Testing, MET@ICSE 2021, Madrid, Spain, June 2, 2021, pages 61--68. IEEE, 2021. Best Paper award.
[ DOI | pdf ]
ISSTA 2021: Matt Windsor, Alastair F. Donaldson, and John Wickerson. C4: the C compiler concurrency checker. In Cristian Cadar and Xiangyu Zhang, editors, ISSTA '21: 30th ACM SIGSOFT International Symposium on Software Testing and Analysis, Virtual Event, Denmark, July 11-17, 2021, pages 670--673. ACM, 2021.
[ DOI | pdf ]
PLDI 2021: Alastair F. Donaldson, Paul Thomson, Vasyl Teliman, Stefano Milizia, André Perez Maselco, and Antoni Karpinski. Test-case reduction and deduplication almost for free with transformation-based compiler testing. In Stephen N. Freund and Eran Yahav, editors, PLDI '21: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, Virtual Event, Canada, June 20-25, 2021, pages 1017--1032. ACM, 2021.
[ DOI | pdf ]
ECOOP 2020: David Maciver and Alastair F. Donaldson. Test-case reduction via test-case generation: Insights from the hypothesis reducer (tool insights paper). In Robert Hirschfeld and Tobias Pape, editors, 34th European Conference on Object-Oriented Programming, ECOOP 2020, November 15-17, 2020, Berlin, Germany (Virtual Conference), volume 166 of LIPIcs, pages 13:1--13:27. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020.
[ DOI | pdf ]
ECOOP 2020: Alastair F. Donaldson, Hugues Evrard, and Paul Thomson. Putting randomized compiler testing into production (experience report). In Robert Hirschfeld and Tobias Pape, editors, 34th European Conference on Object-Oriented Programming, ECOOP 2020, November 15-17, 2020, Berlin, Germany (Virtual Conference), volume 166 of LIPIcs, pages 22:1--22:29. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020.
[ DOI | pdf ]
ASE 2020: Karine Even-Mendoza, Cristian Cadar, and Alastair F. Donaldson. Closer to the edge: Testing compilers more thoroughly by being less conservative about undefined behaviour. In 35th IEEE/ACM International Conference on Automated Software Engineering, ASE 2020, Melbourne, Australia, September 21-25, 2020, pages 1219--1223. IEEE, 2020.
[ DOI | pdf ]
RTAS 2020: Dan Iorga, Tyler Sorensen, John Wickerson, and Alastair F. Donaldson. Slow and steady: Measuring and tuning multicore interference. In IEEE Real-Time and Embedded Technology and Applications Symposium, RTAS 2020, Sydney, Australia, April 21-24, 2020, pages 200--212. IEEE, 2020.
[ DOI | pdf ]
OOPSLA 2019: Michaël Marcozzi, Qiyi Tang, Alastair F. Donaldson, and Cristian Cadar. Compiler fuzzing: how much does it matter? Proc. ACM Program. Lang., 3(OOPSLA):155:1--155:29, 2019.
[ DOI | pdf ]
MET 2019: Alastair F. Donaldson. Metamorphic testing of Android graphics drivers. In Xiaoyuan Xie, Pak-Lok Poon, and Laura L. Pullum, editors, Proceedings of the 4th International Workshop on Metamorphic Testing, MET@ICSE 2019, Montreal, QC, Canada, May 26, 2019, page 1. IEEE / ACM, 2019.
[ DOI | pdf ]
IISWC 2019: Tyler Sorensen, Sreepathi Pai, and Alastair F. Donaldson. One size doesn't fit all: Quantifying performance portability of graph applications on GPUs. In IEEE International Symposium on Workload Characterization, IISWC 2019, Orlando, FL, USA, November 3-5, 2019, pages 155--166. IEEE, 2019. Best Paper award.
[ DOI | pdf ]
IWOCL 2019: Tyler Sorensen, Sreepathi Pai, and Alastair F. Donaldson. Performance evaluation of OpenCL standard support (and beyond). In Proceedings of the International Workshop on OpenCL, IWOCL 2019, Boston, MA, USA, May 13-15, 2019, pages 8:1--8:2. ACM, 2019. Best Paper award.
[ DOI | pdf ]
PLDI 2019: Christopher Lidbury and Alastair F. Donaldson. Sparse record and replay with controlled scheduling. In Kathryn S. McKinley and Kathleen Fisher, editors, Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019, Phoenix, AZ, USA, June 22-26, 2019, pages 576--593. ACM, 2019.
[ DOI | pdf ]
FSE 2019: Daniel Liew, Cristian Cadar, Alastair F. Donaldson, and J. Ryan Stinnett. Just fuzz it: solving floating-point constraints using coverage-guided fuzzing. In Marlon Dumas, Dietmar Pfahl, Sven Apel, and Alessandra Russo, editors, Proceedings of the ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/SIGSOFT FSE 2019, Tallinn, Estonia, August 26-30, 2019, pages 521--532. ACM, 2019.
[ DOI | pdf ]
LNCS 2019: Robert Chatley, Alastair F. Donaldson, and Alan Mycroft. The next 7000 programming languages. In Bernhard Steffen and Gerhard J. Woeginger, editors, Computing and Software Science - State of the Art and Perspectives, volume 10000 of Lecture Notes in Computer Science, pages 250--282. Springer, 2019.
[ DOI | pdf ]
ACM TSE 2018: Adam Betts, Nathan Chong, Pantazis Deligiannis, Alastair F. Donaldson, and Jeroen Ketema. Implementing and evaluating candidate-based invariant generation. IEEE Trans. Software Eng., 44(7):631--650, 2018.
[ DOI | pdf ]
CONCUR 2018: Tyler Sorensen, Hugues Evrard, and Alastair F. Donaldson. GPU schedulers: How fair is fair enough? In Sven Schewe and Lijun Zhang, editors, 29th International Conference on Concurrency Theory, CONCUR 2018, September 4-7, 2018, Beijing, China, volume 118 of LIPIcs, pages 23:1--23:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018.
[ DOI | pdf ]
OOPSLA 2017: Alastair F. Donaldson, Hugues Evrard, Andrei Lascu, and Paul Thomson. Automated testing of graphics shader compilers. Proc. ACM Program. Lang., 1(OOPSLA):93:1--93:29, 2017.
[ DOI | pdf ]
SoCP 2017: Jeroen Ketema and Alastair F. Donaldson. Termination analysis for GPU kernels. Sci. Comput. Program., 148:107--122, 2017.
[ DOI | pdf ]
ACM TOMS 2017: Victor Magron, George A. Constantinides, and Alastair F. Donaldson. Certified roundoff error bounds using semidefinite programming. ACM Trans. Math. Softw., 43(4):34:1--34:31, 2017.
[ DOI | pdf ]
CONCUR 2017: Alastair F. Donaldson, Jeroen Ketema, Tyler Sorensen, and John Wickerson. Forward progress on GPU concurrency (invited talk). In Roland Meyer and Uwe Nestmann, editors, 28th International Conference on Concurrency Theory, CONCUR 2017, September 5-8, 2017, Berlin, Germany, volume 85 of LIPIcs, pages 1:1--1:13. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017.
[ DOI | pdf ]
ASE 2017: Daniel Liew, Daniel Schemmel, Cristian Cadar, Alastair F. Donaldson, Rafael Zähl, and Klaus Wehrle. Floating-point symbolic execution: a case study in n-version programming. In Grigore Rosu, Massimiliano Di Penta, and Tien N. Nguyen, editors, Proceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering, ASE 2017, Urbana, IL, USA, October 30 - November 03, 2017, pages 601--612. IEEE Computer Society, 2017. Best Experience Paper award.
[ DOI | pdf ]
POPL 2017: Christopher Lidbury and Alastair F. Donaldson. Dynamic race detection for C++11. In Giuseppe Castagna and Andrew D. Gordon, editors, Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, pages 443--457. ACM, 2017.
[ DOI | pdf ]
FSE 2017: Tyler Sorensen, Hugues Evrard, and Alastair F. Donaldson. Cooperative kernels: GPU multitasking for blocking algorithms. In Eric Bodden, Wilhelm Schäfer, Arie van Deursen, and Andrea Zisman, editors, Proceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering, ESEC/FSE 2017, Paderborn, Germany, September 4-8, 2017, pages 431--441. ACM, 2017. ACM SIGSOFT Disginguished Paper award.
[ DOI | pdf ]
ACM TOPC 2016: Paul Thomson, Alastair F. Donaldson, and Adam Betts. Concurrency testing using controlled schedulers: An empirical study. ACM Trans. Parallel Comput., 2(4):23:1--23:37, 2016.
[ DOI | pdf ]
FAST 2016: Pantazis Deligiannis, Matt McCutchen, Paul Thomson, Shuo Chen, Alastair F. Donaldson, John Erickson, Cheng Huang, Akash Lal, Rashmi Mudduluru, Shaz Qadeer, and Wolfram Schulte. Uncovering bugs in distributed storage systems during testing (not in production!). In Angela Demke Brown and Florentina I. Popovici, editors, 14th USENIX Conference on File and Storage Technologies, FAST 2016, Santa Clara, CA, USA, February 22-25, 2016, pages 249--262. USENIX Association, 2016.
[ pdf ]
MET 2016: Alastair F. Donaldson and Andrei Lascu. Metamorphic testing for (graphics) compilers. In Proceedings of the 1st International Workshop on Metamorphic Testing, MET@ICSE 2016, Austin, Texas, USA, May 16, 2016, pages 44--47. ACM, 2016.
[ DOI | pdf ]
ICSE V2025 2016: Cristian Cadar and Alastair F. Donaldson. Analysing the program analyser. In Laura K. Dillon, Willem Visser, and Laurie A. Williams, editors, Proceedings of the 38th International Conference on Software Engineering, ICSE 2016, Austin, TX, USA, May 14-22, 2016 - Companion Volume, pages 765--768. ACM, 2016.
[ DOI | pdf ]
ICST 2016: Daniel Liew, Cristian Cadar, and Alastair F. Donaldson. Symbooglix: A symbolic execution engine for Boogie programs. In 2016 IEEE International Conference on Software Testing, Verification and Validation, ICST 2016, Chicago, IL, USA, April 11-15, 2016, pages 45--56. IEEE Computer Society, 2016. Best Paper award.
[ DOI | pdf ]
IWOCL 2016: Moritz Pflanzer, Alastair F. Donaldson, and Andrei Lascu. Automatic test case reduction for OpenCL. In Proceedings of the 4th International Workshop on OpenCL, IWOCL 2016, Vienna, Austria, April 19-21, 2016, pages 1:1--1:12. ACM, 2016.
[ DOI | pdf ]
IWOCL 2016: Tyler Sorensen and Alastair F. Donaldson. The hitchhiker's guide to cross-platform OpenCL application development. In Proceedings of the 4th International Workshop on OpenCL, IWOCL 2016, Vienna, Austria, April 19-21, 2016, pages 2:1--2:12. ACM, 2016.
[ DOI | pdf ]
OOPSLA 2016: Tyler Sorensen, Alastair F. Donaldson, Mark Batty, Ganesh Gopalakrishnan, and Zvonimir Rakamaric. Portable inter-workgroup barrier synchronisation for GPUs. In Eelco Visser and Yannis Smaragdakis, editors, Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2016, part of SPLASH 2016, Amsterdam, The Netherlands, October 30 - November 4, 2016, pages 39--58. ACM, 2016.
[ DOI | pdf ]
PLDI 2016: Tyler Sorensen and Alastair F. Donaldson. Exposing errors related to weak memory in GPU applications. In Chandra Krintz and Emery D. Berger, editors, Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2016, Santa Barbara, CA, USA, June 13-17, 2016, pages 100--113. ACM, 2016.
[ DOI | pdf ]
POPL 2016: Mark Batty, Alastair F. Donaldson, and John Wickerson. Overhauling SC atomics in C11 and OpenCL. In Rastislav Bodík and Rupak Majumdar, editors, Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016, pages 634--648. ACM, 2016.
[ DOI | pdf ]
TOPLAS 2015: Adam Betts, Nathan Chong, Alastair F. Donaldson, Jeroen Ketema, Shaz Qadeer, Paul Thomson, and John Wickerson. The design and implementation of a verification technique for GPU kernels. ACM Trans. Program. Lang. Syst., 37(3):10:1--10:49, 2015.
[ DOI | pdf ]
PACT 2015: 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, and Elnar Hajiyev. PENCIL: A platform-neutral compute intermediate language for accelerator programming. In 2015 International Conference on Parallel Architectures and Compilation, PACT 2015, San Francisco, CA, USA, October 18-21, 2015, pages 138--149. IEEE Computer Society, 2015.
[ DOI | pdf ]
ASPLOS 2015: Jade Alglave, Mark Batty, Alastair F. Donaldson, Ganesh Gopalakrishnan, Jeroen Ketema, Daniel Poetzl, Tyler Sorensen, and John Wickerson. GPU concurrency: Weak behaviours and programming assumptions. In Özcan Özturk, Kemal Ebcioglu, and Sandhya Dwarkadas, editors, Proceedings of the Twentieth International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS 2015, Istanbul, Turkey, March 14-18, 2015, pages 577--591. ACM, 2015.
[ DOI | pdf ]
ASE 2015: Pantazis Deligiannis, Alastair F. Donaldson, and Zvonimir Rakamaric. Fast and precise symbolic analysis of concurrency bugs in device drivers. In Myra B. Cohen, Lars Grunske, and Michael Whalen, editors, 30th IEEE/ACM International Conference on Automated Software Engineering, ASE 2015, Lincoln, NE, USA, November 9-13, 2015, pages 166--177. IEEE Computer Society, 2015.
[ DOI | pdf ]
OOPSLA 2015: John Wickerson, Mark Batty, Bradford M. Beckmann, and Alastair F. Donaldson. Remote-scope promotion: clarified, rectified, and verified. In Jonathan Aldrich and Patrick Eugster, editors, Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2015, part of SPLASH 2015, Pittsburgh, PA, USA, October 25-30, 2015, pages 731--747. ACM, 2015.
[ DOI | pdf ]
PLDI 2015: Christopher Lidbury, Andrei Lascu, Nathan Chong, and Alastair F. Donaldson. Many-core compiler fuzzing. In David Grove and Stephen M. Blackburn, editors, Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, Portland, OR, USA, June 15-17, 2015, pages 65--76. ACM, 2015.
[ DOI | pdf ]
PLDI 2015: Pantazis Deligiannis, Alastair F. Donaldson, Jeroen Ketema, Akash Lal, and Paul Thomson. Asynchronous programming, analysis and testing with state machines. In David Grove and Stephen M. Blackburn, editors, Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, Portland, OR, USA, June 15-17, 2015, pages 154--164. ACM, 2015.
[ DOI | pdf ]
PPoPP 2015: Paul Thomson and Alastair F. Donaldson. The lazy happens-before relation: better partial-order reduction for systematic concurrency testing. In Albert Cohen and David Grove, editors, Proceedings of the 20th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPoPP 2015, San Francisco, CA, USA, February 7-11, 2015, pages 259--260. ACM, 2015.
[ DOI | pdf ]
AVoCS 2014: Alastair F. Donaldson. The GPUVerify method: a tutorial overview. Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 70, 2014.
[ DOI | pdf ]
OSR 2014: Sidney Amani, Peter Chubb, Alastair F. Donaldson, Alexander Legg, Keng Chai Ong, Leonid Ryzhyk, and Yanjin Zhu. Automatic verification of active device drivers. ACM SIGOPS Oper. Syst. Rev., 48(1):106--118, 2014.
[ DOI | pdf ]
CAV 2014: Ethel Bardsley, Adam Betts, Nathan Chong, Peter Collingbourne, Pantazis Deligiannis, Alastair F. Donaldson, Jeroen Ketema, Daniel Liew, and Shaz Qadeer. Engineering a static verification tool for GPU kernels. In Armin Biere and Roderick Bloem, editors, Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings, volume 8559 of Lecture Notes in Computer Science, pages 226--242. Springer, 2014.
[ DOI | pdf ]
IWOCL 2014: Ethel Bardsley, Alastair F. Donaldson, and John Wickerson. KernelInterceptor: automating GPU kernel verification by intercepting kernels and their parameters. In Simon McIntosh-Smith and Ben Bergen, editors, Proceedings of the International Workshop on OpenCL, IWOCL 2013 & 2014, May 13-14, 2013, Georgia Tech, Atlanta, GA, USA / Bristol, UK, May 12-13, 2014, pages 7:1--7:5. ACM, 2014.
[ DOI | pdf ]
NFM 2014: Ethel Bardsley and Alastair F. Donaldson. Warps and atomics: Beyond barrier synchronization in the verification of GPU kernels. In Julia M. Badger and Kristin Yvonne Rozier, editors, NASA Formal Methods - 6th International Symposium, NFM 2014, Houston, TX, USA, April 29 - May 1, 2014. Proceedings, volume 8430 of Lecture Notes in Computer Science, pages 230--245. Springer, 2014.
[ DOI | pdf ]
POPL 2014: Nathan Chong, Alastair F. Donaldson, and Jeroen Ketema. A sound and complete abstraction for reasoning about parallel prefix sums. In Suresh Jagannathan and Peter Sewell, editors, The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, San Diego, CA, USA, January 20-21, 2014, pages 397--410. ACM, 2014.
[ DOI | pdf ]
PPoPP 2014: Paul Thomson, Alastair F. Donaldson, and Adam Betts. Concurrency testing using schedule bounding: an empirical study. In José E. Moreira and James R. Larus, editors, ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPoPP '14, Orlando, FL, USA, February 15-19, 2014, pages 15--28. ACM, 2014. Best Student Paper award.
[ DOI | pdf ]
ECRTS 2013: Adam Betts and Alastair F. Donaldson. Estimating the WCET of GPU-accelerated applications using hybrid analysis. In 25th Euromicro Conference on Real-Time Systems, ECRTS 2013, Paris, France, July 9-12, 2013, pages 193--202. IEEE Computer Society, 2013.
[ DOI | pdf ]
ESOP 2013: Peter Collingbourne, Alastair F. Donaldson, Jeroen Ketema, and Shaz Qadeer. Interleaving and lock-step semantics for analysis and verification of GPU kernels. In Matthias Felleisen and Philippa Gardner, editors, Programming Languages and Systems - 22nd European Symposium on Programming, ESOP 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings, volume 7792 of Lecture Notes in Computer Science, pages 270--289. Springer, 2013. Nominated for Best Paper award.
[ DOI | pdf ]
OOPSLA 2013: Nathan Chong, Alastair F. Donaldson, Paul H. J. Kelly, Jeroen Ketema, and Shaz Qadeer. Barrier invariants: a shared state abstraction for the analysis of data-dependent GPU kernels. In Antony L. Hosking, Patrick Th. Eugster, and Cristina V. Lopes, editors, Proceedings of the 2013 ACM SIGPLAN International Conference on Object Oriented Programming Systems Languages & Applications, OOPSLA 2013, part of SPLASH 2013, Indianapolis, IN, USA, October 26-31, 2013, pages 605--622. ACM, 2013.
[ DOI | pdf ]
FMSD 2012: Alastair F. Donaldson, Alexander Kaiser, Daniel Kroening, Michael Tautschnig, and Thomas Wahl. Counterexample-guided abstraction refinement for symmetric concurrent programs. Formal Methods Syst. Des., 41(1):25--44, 2012.
[ DOI | pdf ]
OOPSLA 2012: Adam Betts, Nathan Chong, Alastair F. Donaldson, Shaz Qadeer, and Paul Thomson. GPUVerify: a verifier for GPU kernels. In Gary T. Leavens and Matthew B. Dwyer, editors, Proceedings of the 27th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2012, part of SPLASH 2012, Tucson, AZ, USA, October 21-25, 2012, pages 113--132. ACM, 2012. ACM SIGPLAN Most Influntial OOPSLA Paper Award, 2022.
[ DOI | pdf ]
TACAS 2012: Gérard Basler, Alastair F. Donaldson, Alexander Kaiser, Daniel Kroening, Michael Tautschnig, and Thomas Wahl. satabs: A bit-precise verifier for C programs - (competition contribution). In Cormac Flanagan and Barbara König, editors, Tools and Algorithms for the Construction and Analysis of Systems - 18th International Conference, TACAS 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 - April 1, 2012. Proceedings, volume 7214 of Lecture Notes in Computer Science, pages 552--555. Springer, 2012.
[ DOI | pdf ]
SSV 2012: Sidney Amani, Peter Chubb, Alastair F. Donaldson, Alexander Legg, Leonid Ryzhyk, and Yanjin Zhu. Automatic verification of message-based device drivers. In Franck Cassez, Ralf Huuck, Gerwin Klein, and Bastian Schlich, editors, Proceedings Seventh Conference on Systems Software Verification, SSV 2012, Sydney, Australia, 28-30 November 2012, volume 102 of EPTCS, pages 4--17, 2012.
[ DOI | pdf ]
FMSD 2011: Alastair F. Donaldson, Daniel Kroening, and Philipp Rümmer. Automatic analysis of DMA races using model checking and k-induction. Formal Methods Syst. Des., 39(1):83--113, 2011.
[ DOI | pdf ]
APSys 2011: Sidney Amani, Leonid Ryzhyk, Alastair F. Donaldson, Gernot Heiser, Alexander Legg, and Yanjin Zhu. Static analysis of device drivers: we can do better! In Haibo Chen, Zheng Zhang, Sue Moon, and Yuanyuan Zhou, editors, APSys '11 Asia Pacific Workshop on Systems, Shanghai, China, July 11-12, 2011, page 8. ACM, 2011.
[ DOI | pdf ]
ATVA 2011: Jade Alglave, Alastair F. Donaldson, Daniel Kroening, and Michael Tautschnig. Making software verification tools really work. In Tevfik Bultan and Pao-Ann Hsiung, editors, Automated Technology for Verification and Analysis, 9th International Symposium, ATVA 2011, Taipei, Taiwan, October 11-14, 2011. Proceedings, volume 6996 of Lecture Notes in Computer Science, pages 28--42. Springer, 2011.
[ DOI | pdf ]
CAV 2011: Alastair F. Donaldson, Alexander Kaiser, Daniel Kroening, and Thomas Wahl. Symmetry-aware predicate abstraction for shared-variable concurrent programs. In Ganesh Gopalakrishnan and Shaz Qadeer, editors, Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings, volume 6806 of Lecture Notes in Computer Science, pages 356--371. Springer, 2011.
[ DOI | pdf ]
ASE 2011: Matko Botincan, Mike Dodds, Alastair F. Donaldson, and Matthew J. Parkinson. Safe asynchronous multicore memory operations. In Perry Alexander, Corina S. Pasareanu, and John G. Hosking, editors, 26th IEEE/ACM International Conference on Automated Software Engineering (ASE 2011), Lawrence, KS, USA, November 6-10, 2011, pages 153--162. IEEE Computer Society, 2011.
[ DOI | pdf ]
MSPC 2011: George Russell, Colin Riley, Neil Henning, Uwe Dolinsky, Andrew Richards, Alastair F. Donaldson, and Alexander S. van Amesfoort. The impact of diverse memory architectures on multicore consumer software: an industrial perspective from the video games domain. In Jeffrey S. Vetter, Madanlal Musuvathi, and Xipeng Shen, editors, Proceedings of the 2011 ACM SIGPLAN workshop on Memory Systems Performance and Correctness: held in conjunction with PLDI '11, San Jose, CA, USA, June 5, 2011, pages 37--42. ACM, 2011.
[ DOI | pdf ]
PPoPP 2011: Alastair F. Donaldson, Daniel Kroening, and Philipp Rümmer. SCRATCH: a tool for automatic analysis of dma races. In Calin Cascaval and Pen-Chung Yew, editors, Proceedings of the 16th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPOPP 2011, San Antonio, TX, USA, February 12-16, 2011, pages 311--312. ACM, 2011.
[ DOI | pdf ]
PPoPP 2011: Matko Botincan, Mike Dodds, Alastair F. Donaldson, and Matthew J. Parkinson. Automatic safety proofs for asynchronous memory operations. In Calin Cascaval and Pen-Chung Yew, editors, Proceedings of the 16th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPOPP 2011, San Antonio, TX, USA, February 12-16, 2011, pages 313--314. ACM, 2011.
[ DOI | pdf ]
SAS 2011: Alastair F. Donaldson, Leopold Haller, Daniel Kroening, and Philipp Rümmer. Software verification using k-induction. In Eran Yahav, editor, Static Analysis - 18th International Symposium, SAS 2011, Venice, Italy, September 14-16, 2011. Proceedings, volume 6887 of Lecture Notes in Computer Science, pages 351--368. Springer, 2011.
[ DOI | pdf ]
VMCAI 2011: Alastair F. Donaldson, Leopold Haller, and Daniel Kroening. Strengthening induction-based race checking with lightweight static analysis. In Ranjit Jhala and David A. Schmidt, editors, Verification, Model Checking, and Abstract Interpretation - 12th International Conference, VMCAI 2011, Austin, TX, USA, January 23-25, 2011. Proceedings, volume 6538 of Lecture Notes in Computer Science, pages 169--183. Springer, 2011.
[ DOI | pdf ]
SoCP 2010: Alastair F. Donaldson and Simon J. Gay. Type inference and strong static type checking for Promela. Sci. Comput. Program., 75(11):1165--1191, 2010.
[ DOI | pdf ]
Symmetry 2010: Thomas Wahl and Alastair F. Donaldson. Replication and abstraction: Symmetry in automated formal verification. Symmetry, 2(2):799--847, 2010.
[ DOI | pdf ]
MuCoCoS 2010: Alastair F. Donaldson, Uwe Dolinsky, Andrew Richards, and George Russell. Automatic offloading of C++ for the Cell BE processor: A case study using offload. In Leonard Barolli, Fatos Xhafa, Salvatore Vitabile, and Hui-Huang Hsu, editors, 3rd International Workshop on Multi-/Many-core Computing Systems (MuCoCoS), co-located with CISIS 2010, The Fourth International Conference on Complex, Intelligent and Software Intensive Systems, Krakow, Poland, 15-18 February 2010, pages 901--906. IEEE Computer Society, 2010.
[ DOI | pdf ]
HPPC 2010: George Russell, Paul Keir, Alastair F. Donaldson, Uwe Dolinsky, Andrew Richards, and Colin Riley. Programming heterogeneous multicore systems using threading building blocks. In Mario R. Guarracino, Frédéric Vivien, Jesper Larsson Träff, Mario Cannataro, Marco Danelutto, Anders Hast, Francesca Perla, Andreas Knüpfer, Beniamino Di Martino, and Michael Alexander, editors, Euro-Par 2010 Parallel Processing Workshops - HeteroPar, HPCC, HiBB, CoreGrid, UCHPC, HPCF, PROPER, CCPI, VHPC, Ischia, Italy, August 31-September 3, 2010, Revised Selected Papers, volume 6586 of Lecture Notes in Computer Science, pages 117--125. Springer, 2010.
[ DOI | pdf ]
FMCO 2010: Alastair F. Donaldson, Nannan He, Daniel Kroening, and Philipp Rümmer. Tightening test coverage metrics: A case study in equivalence checking using k-induction. In Bernhard K. Aichernig, Frank S. de Boer, and Marcello M. Bonsangue, editors, Formal Methods for Components and Objects - 9th International Symposium, FMCO 2010, Graz, Austria, November 29 - December 1, 2010. Revised Papers, volume 6957 of Lecture Notes in Computer Science, pages 297--315. Springer, 2010.
[ DOI | pdf ]
HiPEAC 2010: Pete Cooper, Uwe Dolinsky, Alastair F. Donaldson, Andrew Richards, Colin Riley, and George Russell. Offload - automating code migration to heterogeneous multicore systems. In Yale N. Patt, Pierfrancesco Foglia, Evelyn Duesterwald, Paolo Faraboschi, and Xavier Martorell, editors, High Performance Embedded Architectures and Compilers, 5th International Conference, HiPEAC 2010, Pisa, Italy, January 25-27, 2010. Proceedings, volume 5952 of Lecture Notes in Computer Science, pages 337--352. Springer, 2010.
[ DOI | pdf ]
TACAS 2010: Alastair F. Donaldson, Daniel Kroening, and Philipp Rümmer. Automatic analysis of scratch-pad memory code for heterogeneous multicore processors. In Javier Esparza and Rupak Majumdar, editors, Tools and Algorithms for the Construction and Analysis of Systems, 16th International Conference, TACAS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings, volume 6015 of Lecture Notes in Computer Science, pages 280--295. Springer, 2010.
[ DOI | pdf ]
AMAI 2009: Alastair F. Donaldson and Alice Miller. On the constructive orbit problem. Ann. Math. Artif. Intell., 57(1):1--35, 2009.
[ DOI | pdf ]
HPPC 2009: Lee W. Howes, Anton Lokhmotov, Alastair F. Donaldson, and Paul H. J. Kelly. Towards metaprogramming for parallel systems on a chip. In Hai-Xiang Lin, Michael Alexander, Martti Forsell, Andreas Knüpfer, Radu Prodan, Leonel Sousa, and Achim Streit, editors, Euro-Par 2009 - Parallel Processing Workshops, HPPC, HeteroPar, PROPER, ROIA, UNICORE, VHPC, Delft, The Netherlands, August 25-28, 2009, Revised Selected Papers, volume 6043 of Lecture Notes in Computer Science, pages 36--45. Springer, 2009.
[ DOI | pdf ]
HiPEAC 2009: Lee W. Howes, Anton Lokhmotov, Alastair F. Donaldson, and Paul H. J. Kelly. Deriving efficient data movement from decoupled access/execute specifications. In André Seznec, Joel S. Emer, Michael F. P. O'Boyle, Margaret Martonosi, and Theo Ungerer, editors, High Performance Embedded Architectures and Compilers, Fourth International Conference, HiPEAC 2009, Paphos, Cyprus, January 25-28, 2009. Proceedings, volume 5409 of Lecture Notes in Computer Science, pages 168--182. Springer, 2009.
[ DOI | pdf ]
QEST 2009: Alastair F. Donaldson, Alice Miller, and David Parker. Language-level symmetry reduction for probabilistic model checking. In QEST 2009, Sixth International Conference on the Quantitative Evaluation of Systems, Budapest, Hungary, 13-16 September 2009, pages 289--298. IEEE Computer Society, 2009.
[ DOI | pdf ]
JAR 2008: Alastair F. Donaldson and Alice Miller. Automatic symmetry detection for promela. J. Autom. Reason., 41(3-4):251--293, 2008.
[ DOI | pdf ]
HPPC 2008: Alastair F. Donaldson, Paul Keir, and Anton Lokhmotov. Compile-time and run-time issues in an auto-parallelisation system for the Cell BE processor. In Eduardo César, Michael Alexander, Achim Streit, Jesper Larsson Träff, Christophe Cérin, Andreas Knüpfer, Dieter Kranzlmüller, and Shantenu Jha, editors, Euro-Par 2008 Workshops - Parallel Processing, VHPC 2008, UNICORE 2008, HPPC 2008, SGS 2008, PROPER 2008, ROIA 2008, and DPA 2008, Las Palmas de Gran Canaria, Spain, August 25-26, 2008, Revised Selected Papers, volume 5415 of Lecture Notes in Computer Science, pages 163--173. Springer, 2008.
[ DOI | pdf ]
NETGAMES 2008: George Russell, Alastair F. Donaldson, and Paul Sheppard. Tackling online game development problems with a novel network scripting language. In Mark Claypool, editor, Proceedings of the 7th ACM SIGCOMM Workshop on Network and System Support for Games, NETGAMES 2008, Worcester, Massachusetts, USA, October 21-22, 2008, pages 85--90. ACM, 2008.
[ DOI | pdf ]
AVoCS 2008: Alastair F. Donaldson. Vector symmetry reduction. In Alice Miller and Muffy Calder, editors, Proceedings of the Eighth International Workshop on Automated Verification of Critical Systems, AVoCS 2008, Glasgow, UK, September 30 - October 1, 2008, volume 250 of Electronic Notes in Theoretical Computer Science, pages 3--18. Elsevier, 2008.
[ DOI | pdf ]
ComNet 2007: Alice Miller, Muffy Calder, and Alastair F. Donaldson. A template-based approach for the generation of abstractable and reducible models of featured networks. Comput. Networks, 51(2):439--455, 2007.
[ DOI | pdf ]
ATVA 2007: Dragan Bosnacki, Alastair F. Donaldson, Michael Leuschel, and Thierry Massart. Efficient approximate verification of promela models via symmetry markers. In Kedar S. Namjoshi, Tomohiro Yoneda, Teruo Higashino, and Yoshio Okamura, editors, Automated Technology for Verification and Analysis, 5th International Symposium, ATVA 2007, Tokyo, Japan, October 22-25, 2007, Proceedings, volume 4762 of Lecture Notes in Computer Science, pages 300--315. Springer, 2007.
[ DOI | pdf ]
HPPC 2007: Alastair F. Donaldson, Colin Riley, Anton Lokhmotov, and Andrew Cook. Auto-parallelisation of Sieve C++ programs. In Luc Bougé, Martti Forsell, Jesper Larsson Träff, Achim Streit, Wolfgang Ziegler, Michael Alexander, and Stephen Childs, editors, Euro-Par 2007 Workshops: Parallel Processing, HPPC 2007, UNICORE Summit 2007, and VHPC 2007, Rennes, France, August 28-31, 2007, Revised Selected Papers, volume 4854 of Lecture Notes in Computer Science, pages 18--27. Springer, 2007.
[ DOI | pdf ]
QEST 2007: Alastair F. Donaldson, Alice Miller, and David Parker. GRIP: generic representatives in PRISM. In Fourth International Conference on the Quantitative Evaluaiton of Systems (QEST 2007), 17-19 September 2007, Edinburgh, Scotland, UK, pages 115--116. IEEE Computer Society, 2007.
[ DOI | pdf ]
ACM Surv. 2006: Alice Miller, Alastair F. Donaldson, and Muffy Calder. Symmetry in temporal logic model checking. ACM Comput. Surv., 38(3):8, 2006.
[ DOI | pdf ]
AMAST 2006: Alastair F. Donaldson and Alice Miller. A computational group theoretic symmetry reduction package for the spin model checker. In Michael Johnson and Varmo Vene, editors, Algebraic Methodology and Software Technology, 11th International Conference, AMAST 2006, Kuressaare, Estonia, July 5-8, 2006, Proceedings, volume 4019 of Lecture Notes in Computer Science, pages 374--380. Springer, 2006.
[ DOI | pdf ]
ATVA 2006: Alastair F. Donaldson and Alice Miller. Symmetry reduction for probabilistic model checking using generic representatives. In Susanne Graf and Wenhui Zhang, editors, Automated Technology for Verification and Analysis, 4th International Symposium, ATVA 2006, Beijing, China, October 23-26, 2006, volume 4218 of Lecture Notes in Computer Science, pages 9--23. Springer, 2006.
[ DOI | pdf ]
FM 2006: Alastair F. Donaldson and Alice Miller. Exact and approximate strategies for symmetry reduction in model checking. In Jayadev Misra, Tobias Nipkow, and Emil Sekerinski, editors, FM 2006: Formal Methods, 14th International Symposium on Formal Methods, Hamilton, Canada, August 21-27, 2006, Proceedings, volume 4085 of Lecture Notes in Computer Science, pages 541--556. Springer, 2006.
[ DOI | pdf ]
AVoCS 2006: Alastair F. Donaldson and Alice Miller. Extending symmetry reduction techniques to a realistic model of computation. In Stephan Merz and Tobias Nipkow, editors, Proceedings of the 6th International Workshop on Automated Verification of Critical Systems, AVoCS 2006, Nancy, France, September 18-19, 2006, volume 185 of Electronic Notes in Theoretical Computer Science, pages 63--76. Elsevier, 2006.
[ DOI | pdf ]
FM 2005: Alastair F. Donaldson and Alice Miller. Automatic symmetry detection for model checking using computational group theory. In John S. Fitzgerald, Ian J. Hayes, and Andrzej Tarlecki, editors, FM 2005: Formal Methods, International Symposium of Formal Methods Europe, Newcastle, UK, July 18-22, 2005, Proceedings, volume 3582 of Lecture Notes in Computer Science, pages 481--496. Springer, 2005.
[ DOI | pdf ]
SPIN 2005: Alastair F. Donaldson and Simon J. Gay. Etch: An enhanced type checking tool for Promela. In Patrice Godefroid, editor, Model Checking Software, 12th International SPIN Workshop, San Francisco, CA, USA, August 22-24, 2005, Proceedings, volume 3639 of Lecture Notes in Computer Science, pages 266--271. Springer, 2005.
[ DOI | pdf ]
ARTS 2004: Alastair F. Donaldson, Alice Miller, and Muffy Calder. Spin-to-Grape: A tool for analysing symmetry in promela models. In Irek Ulidowski, editor, Proceedings of the 6th AMAST Workshop on Real-Time Systems, ARTS 2004, Stirling, UK, July 12, 2004, volume 139 of Electronic Notes in Theoretical Computer Science, pages 3--23. Elsevier, 2004.
[ DOI | pdf ]
AVoCS 2004: Alastair F. Donaldson, Alice Miller, and Muffy Calder. Finding symmetry in models of concurrent systems by static channel diagram analysis. In Michael Huth, editor, Proceedings of the Fouth International Workshop on Automated Verification of Critical Systems, AVoCS 2004, London, UK, September 4, 2004, volume 128 of Electronic Notes in Theoretical Computer Science, pages 161--177. Elsevier, 2004.
[ DOI | pdf ]

Past Service

Organisation and Chairing

2025: Dagstuhl Seminar on Testing Program Analyzers and Verifiers (Co-Organiser)
S-REPLS 16 (Organiser)
2024: POPL (Associate Chair)
POPL (Publicity Co-Chair)
2023: TAROT Summer School (Co-Organiser)
2022: ECOOP 2022 (Area Chair for Pearls/Brave New Ideas)
MET (PC Co-Chair)
2020: PLDI (General Chair)
2019: ECOOP (PC Chair)
2017: Dagstuhl Seminar on Analysis and Synthesis of Floating-point Programs (Co-Organiser)
Dagstuhl Seminar on Testing and Verification of Compilers (Co-Organiser)
2016: S-REPLS 4 (Co-Organiser)
Getting Started with Vulkan, UK Khronos Group Chapter meetup at Imperial College London (Organizer)
2015: Imperial Concurrency Workshop, Imperial College London (Co-Organizer)
2014: PLACES (PC Co-Chair)
2013: Dagstuhl Seminar on Correct and Efficient Accelerator Programming (Co-Organiser)
2012: SPIN (PC Co-Chair)
2007: International Symmetry Conference 2007 (Area Chair for Model Checking track)
2006: 6th International Workshop on Symmetry and Constraint Satisfaction Problems (PC Co-Chair)
27th Scottish Theorem Proving Seminar (Organiser)
2005: SymNet Workshop on "Almost Symmetry" in Search, New Lanark, UK, funded by the SymNet EPSRC Network of Excellence (Co-Organiser)

Membership of Program and Review Committees

2025: ICSE 2025 (PC)
ASE 2025 (PC)
ICST 2025 (PC)
FUZZING 2025 (PC)
SBFT 2025 (PC)
VSS 2025 (PC)
Dafny 2025 (PC)
2024: FUZZING 2024 (PC)
ASPLOS 2024 (PC)
2023: STAI 2023 (PC)
ASE 2023 (PC)
IWOCL/SYCLcon 2023 (PC)
ISSTA 2023 (PC)
ECOOP 2023 (PC)
POPL 2023 (PC)
MET 2023 (PC)
2022: IWOCL/SYCLcon 2022 (PC)
ASE 2022 (PC)
CAV 2022 (PC)
PLDI 2022 Student Research Competition (Review Committee)
FUZZING 2022 (PC)
2021: CAV 2021 (PC)
OOPSLA 2021 (ERC)
MET 2021 (PC)
2020: POPL 2020 (PC)
IWOCL 2020 (PC)
2019: OOPSLA 2019 (Review Committee)
PLDI 2019 (PC)
IWOCL 2019 (PC)
2018: OOPSLA 2018 (PC)
ICST 2018 (PC)
2017: CORRECTNESS 2017 (PC)
PLOS 2017 (PC)
SPLASH Workshops 2017 (PC)
PLDI 2017 (ERC)
MET 2017 (PC)
IWOCL 2017 (PC)
DAC 2017, Designer track (PC)
ICSE-NIER 2017 (PC)
PPoPP 2017 (ERC)
2016: POPL 2016 (PC)
PPoPP 2016 (ERC)
FSTTCS 2016 (PC)
DAC 2016, Design/IP track (PC)
SYCL 2016 (PC)
IWOCL 2016 (PC)
2015: CAV 2015 (PC)
ESOP 2015 (PC)
IWOCL 2015 (PC)
PPoPP 2015 (PC)
RV 2015 (PC)
POPL 2015 (ERC)
2014: PLDI 2014 (ERC)
RV 2014 (PC and tool demonstration committee)
SPIN 2014 (PC)
HIPS 2014 (PC)
2013: EuroPar 2013 (PC) SPIN 2013 (PC)
PLACES 2013 (PC)
GRAPHITE 2013 (PC)
VSSE 2013 (PC)
2012: DAC 2012 (Expert Reviewer for subcommittee on Embedded System Specification and Software Engineering)
PLACES 2012 (PC)
GRAPHITE 2012 (PC)
2011: PLACES 2011 (PC)
CISIS 2011 (PC)
2010: HPCC 2010 (PC)
3PGCIC 2010 (PC)
HIPS 2010 (PC) MuCoCoS 2010 (PC)