Alastair F. Donaldson

Old News

CARP project press release (May 2012)

New postdoc Peter Collingbourne (May 2012) Peter Collinbourne recently submitted his PhD thesis at Imperial, and will be moving to industry in September; in the meantime he has joined the Multicore Programming group for a short postdoc stint. Peter has worked extensively with the KLEE system, including building KLEE-FP, a dynamic symbolic execution tool which supports analysis of OpenCL kernels.

New postdoc Jeroen Ketema (April 2012) Jeroen Ketema has joined the Multicore Programming Group as a postdoctoral researcher for our EU-funded project, CARP. Jeroen joins us from the University of Twente. Welcome, Jeroen!

VSSE workshop (March 2012) I recently gave a talk at the First Workshop on Validation Strategies for Software Evolution, organised by Hana Chockler who leads the PINCETTE EU project. The workshop had a great mix of talks from the verification and testing communities, concentrating on how to provide meaningful validation of software systems that are under constant revision (i.e., most systems).

Visit to Intel (March 2012) I have been visiting the Operating Systems group at Intel, Portland Oregon, to speak at a workshop on Device Driver Synthesis and Reliability.

Welcoming Project Administrator, Afra Asim (February 2012) I'm pleased to welcome Afra Asim, who has joined the Multicore Programming Group to act as Project Administrator for CARP.

CARP poster at HiPEAC EU Projects Meeting (January 2012) I am about to go to Paris for the HiPEAC 2012 conference, to present a poster on the CARP project. Check out the poster, designed together with Adam Betts (with help from the CARP consortium).

New postdoc Adam Betts (December 2011) I'm delighted that Adam Betts has joined the Multicore Programming Group to work on the CARP project.

CARP project kickoff (December 2011) December sees the kickoff of CARP, Correct and Efficient Accelerator Programming, a three year collaborative project funded by the European Commission's Seventh Framework Programme. I am coordinating the project at Imperial, and the work is in collaboration with seven other European partners from academia and industry. See the project web page for more details!

New PhD student Paul Thomson (October 2011) I'm very pleased that Paul Thomson has started a PhD with me at Imperial. Paul recently completed his MSc in the Department of Computer Science at Oxford, with a project on race detection for concurrent programs using dynamic symbolic execution.

Visiting Researcher at Microsoft Research, Redmond (August 2011) At the end of August I am joining the RiSE group at Microsoft Research in Redmond as a Visiting Researcher, to work for six weeks with Shaz Qadeer and Tom Ball on analysis of concurrent software.

Paper at ASE (August 2011) For a while I've been working with Matko Botincan and Mike Dodds at the Cambridge Computer Laboratory, and Matthew Parkinson at Microsoft Research Cambridge, on using separation logic-based techniques to prove safety of multicore programs which use asynchronous memory operations. A full paper on this work has just been accepted to the 26th IEEE/ACM International Conference On Automated Software Engineering (ASE 2011). Check it out here.

Paper at SAS (May 2011) Philipp Ruemmer, Leopold Haller, Daniel Kroening and I have had a paper accepted to the 18th International Static Analysis Symposium. The paper is on the use of k-induction for verification of imperative software. Among other things, we implemented k-induction in the Boogie verifier, and found it enabled us to verify programs with weaker invariants than standard Boogie requires. Check it out!

Lectureship at Imperial College London (May 2011) In November 2011 I will be joining the faculty at the Department of Computing at Imperial College London as a Lecturer. I am very excited!

Paper at CAV (March 2011) Thomas Wahl, Alexander Kaiser, Daniel Kroening and I have had a paper accepted to the 23rd International Conference on Computer Aided Verification, on Symmetry-Aware Predicate Abstraction for Shared Variable Concurrent Programs. Check it out here.

Royal Society International Travel Grant funded (January 2011) The Royal Society will provide funding for Dragan Bosnacki of Eindhoven University of Technology to visit me at Oxford this summer, to work on the acceleration of formal verification algorithms using multicore systems. This is through the Society's International Travel Grants scheme.

Short papers accepted at PPoPP (October 2010) I have had two short papers accepted to the 2011 ACM SIGPLAN Conference on Principles and Practice of Parallel Programming. They are both on analysing multicore programs that use asynchronous memory operations. One gives preliminary details on an approach using separation logic, and is with Matko Botincan and Mike Dodds at the Cambridge Computer Laboratory, and Matthew Parkinson at Microsoft Research Cambridge. The other is a tool demonstration paper on SCRATCH, the DMA race analysis tool I have designed in collaboration with Daniel Kroening and Philipp Ruemmer at Oxford.

VMCAI paper on k-induction with static analysis (October 2010) Leopold Haller, Daniel Kroening and I have had a paper accepted at the 2011 conference on Verification, Model Checking and Abstract Interpretation. The paper explores the use of static analysis to aid k-induction as a technique for analysing races in multicore programs that use DMA. Check it out.

Offloading Threading Building Blocks (August 2010) George Russell from Codeplay just presented joint work with me, others at Codeplay, and Paul Keir at Glasgow, at the HPPC 2010 workshop, on using the Offload C++ system to get a subset of Intel's TBB running across the SPE cores of the Cell processor. Check it out.

Intel SCC Research Project (June 2010) Intel have accepted a proposal on Programming Tools for the Intel Single-chip Cloud Computer, which I put together with Paul Kelly at Imperial College London, and colleagues at Codeplay Software Ltd. The result is that Intel will grant us access to their 48-core research platform, to investigate formal verification and performance optimization techniques.

Symmetry Survey (April 2010) Thomas Wahl and I have published an up-to-date survey of symmetry reduction techniques for model checking. Check it out here. This survey complements and extends a previous ACM Computing Surveys article on the topic, which I published with Alice Miller and Muffy Calder.