Travelled to:1 × Austria
1 × Canada
1 × Cyprus
1 × Estonia
1 × Turkey
1 × United Kingdom
11 × USA
2 × Italy
Collaborated with:D.Kröning P.Thomson C.Lidbury J.Ketema N.Chong T.S.0001 A.Miller P.Rümmer M.Batty S.Qadeer J.Wickerson C.Cadar P.Deligiannis A.Betts L.Haller H.Evrard Z.Rakamaric D.Liew A.Lascu M.Botincan M.Dodds M.J.Parkinson A.Kaiser T.Wahl P.Collingbourne G.Gopalakrishnan B.M.Beckmann J.R.Stinnett M.Marcozzi Q.T.0001 A.Lal P.H.J.Kelly G.Basler M.Tautschnig D.Schemmel R.Zähl K.Wehrle J.Alglave D.Pötzl T.Sorensen E.Bardsley
Talks about:gpu (8) analysi (7) program (5) concurr (5) kernel (5) automat (4) verifi (4) memori (4) test (4) fuzz (4)
Person: Alastair F. Donaldson
DBLP: Donaldson:Alastair_F=
Facilitated 1 volumes:
EdContributed to:
2015
2015
2015
2015
2014
20142014
201320132012
2012
201120112011
2011
20112010
2006200520152017
201720192016201720192016201620172019Wrote 32 papers:
- ASPLOS-2015-AlglaveBDGKPSW #behaviour #concurrent #gpu #programming
- GPU Concurrency: Weak Behaviours and Programming Assumptions (JA, MB, AFD, GG, JK, DP, TS, JW), pp. 577–591.
- OOPSLA-2015-WickersonBBD
- Remote-scope promotion: clarified, rectified, and verified (JW, MB, BMB, AFD), pp. 731–747.
- PLDI-2015-DeligiannisDKLT #analysis #programming #state machine #testing
- Asynchronous programming, analysis and testing with state machines (PD, AFD, JK, AL, PT), pp. 154–164.
- PLDI-2015-LidburyLCD #compilation #fuzzing #manycore
- Many-core compiler fuzzing (CL, AL, NC, AFD), pp. 65–76.
- PPoPP-2015-ThomsonD #concurrent #lazy evaluation #partial order #reduction #testing
- The lazy happens-before relation: better partial-order reduction for systematic concurrency testing (PT, AFD), pp. 259–260.
- CAV-2014-BardsleyBCCDDKLQ #gpu #kernel #verification
- Engineering a Static Verification Tool for GPU Kernels (EB, AB, NC, PC, PD, AFD, JK, DL, SQ), pp. 226–242.
- POPL-2014-ChongDK #abstraction #parallel #reasoning
- A sound and complete abstraction for reasoning about parallel prefix sums (NC, AFD, JK), pp. 397–410.
- PPoPP-2014-ThomsonDB #bound #concurrent #empirical #testing #using
- Concurrency testing using schedule bounding: an empirical study (PT, AFD, AB), pp. 15–28.
- ESOP-2013-CollingbourneDKQ #analysis #gpu #kernel #semantics #verification
- Interleaving and Lock-Step Semantics for Analysis and Verification of GPU Kernels (PC, AFD, JK, SQ), pp. 270–289.
- OOPSLA-2013-ChongDKKQ #abstraction #analysis #gpu #invariant #kernel
- Barrier invariants: a shared state abstraction for the analysis of data-dependent GPU kernels (NC, AFD, PHJK, JK, SQ), pp. 605–622.
- OOPSLA-2012-BettsCDQT #gpu #kernel #named #verification
- GPUVerify: a verifier for GPU kernels (AB, NC, AFD, SQ, PT), pp. 113–132.
- TACAS-2012-BaslerDKKTW #c #contest #named #source code #verification
- satabs: A Bit-Precise Verifier for C Programs — (Competition Contribution) (GB, AFD, AK, DK, MT, TW), pp. 552–555.
- ASE-2011-BotincanDDP #manycore #memory management
- Safe asynchronous multicore memory operations (MB, MD, AFD, MJP), pp. 153–162.
- CAV-2011-DonaldsonKKW #abstraction #concurrent #source code #symmetry
- Symmetry-Aware Predicate Abstraction for Shared-Variable Concurrent Programs (AFD, AK, DK, TW), pp. 356–371.
- PPoPP-2011-BotincanDDP #automation #memory management #proving #safety
- Automatic safety proofs for asynchronous memory operations (MB, MD, AFD, MJP), pp. 313–314.
- PPoPP-2011-DonaldsonKR #analysis #automation #named
- SCRATCH: a tool for automatic analysis of dma races (AFD, DK, PR), pp. 311–312.
- SAS-2011-DonaldsonHKR #using #verification
- Software Verification Using k-Induction (AFD, LH, DK, PR), pp. 351–368.
- VMCAI-2011-DonaldsonHK #lightweight #static analysis
- Strengthening Induction-Based Race Checking with Lightweight Static Analysis (AFD, LH, DK), pp. 169–183.
- TACAS-2010-DonaldsonKR #analysis #automation #manycore #memory management
- Automatic Analysis of Scratch-Pad Memory Code for Heterogeneous Multicore Processors (AFD, DK, PR), pp. 280–295.
- FM-2006-DonaldsonM #approximate #model checking #reduction #symmetry
- Exact and Approximate Strategies for Symmetry Reduction in Model Checking (AFD, AM), pp. 541–556.
- FM-2005-DonaldsonM #automation #detection #model checking #symmetry #using
- Automatic Symmetry Detection for Model Checking Using Computational Group Theory (AFD, AM), pp. 481–496.
- ASE-2015-DeligiannisDR #analysis #concurrent #debugging #performance #precise
- Fast and Precise Symbolic Analysis of Concurrency Bugs in Device Drivers (T) (PD, AFD, ZR), pp. 166–177.
- ASE-2017-LiewSCDZW #case study #execution #float #programming #symbolic computation
- Floating-point symbolic execution: a case study in n-version programming (DL, DS, CC, AFD, RZ, KW), pp. 601–612.
- ESEC-FSE-2017-SorensenED #algorithm #gpu #kernel #multi
- Cooperative kernels: GPU multitasking for blocking algorithms (TS0, HE, AFD), pp. 431–441.
- ESEC-FSE-2019-LiewCDS #constraints #float #fuzzing #using
- Just fuzz it: solving floating-point constraints using coverage-guided fuzzing (DL, CC, AFD, JRS), pp. 521–532.
- OOPSLA-2016-SorensenDBGR
- Portable inter-workgroup barrier synchronisation for GPUs (TS0, AFD, MB, GG, ZR), pp. 39–58.
- OOPSLA-2017-DonaldsonELT #automation #compilation #testing
- Automated testing of graphics shader compilers (AFD, HE, AL, PT), p. 29.
- OOPSLA-2019-MarcozziTDC #compilation #fuzzing #how #matter #question
- Compiler fuzzing: how much does it matter? (MM, QT0, AFD, CC), p. 29.
- PLDI-2016-SorensenD #fault #gpu #memory management
- Exposing errors related to weak memory in GPU applications (TS0, AFD), pp. 100–113.
- POPL-2016-BattyDW
- Overhauling SC atomics in C11 and OpenCL (MB, AFD, JW), pp. 634–648.
- POPL-2017-LidburyD #concurrent #detection
- Dynamic race detection for C++11 (CL, AFD), pp. 443–457.
- PLDI-2019-LidburyD #scheduling
- Sparse record and replay with controlled scheduling (CL, AFD), pp. 576–593.